Coarse-graining support: Support.Sobolev.PotentialSolenoidalCubeBridge

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Potential and solenoidal transport across triadic cube realizations

The deterministic multiscale layer mostly uses the half-open cubeSet Q, while the Sobolev layer often proves things first on the open cube openCubeSet Q. This file promotes the existing centered-cube bridge to arbitrary triadic cubes by translating to the centered cube, using the origin-cube bridge, and translating back.

@[simp]

theorem HCPolySupport.H1Function.toCubeSetOriginCube_grad {d : ℕ} [NeZero d] {n : ℤ} (u : H1Function (openCubeSet (originCube d n))) : u.toCubeSetOriginCube.grad = u.grad

@[simp]

theorem HCPolySupport.H1Function.toCubeSetOriginCube_toFun {d : ℕ} [NeZero d] {n : ℤ} (u : H1Function (openCubeSet (originCube d n))) : u.toCubeSetOriginCube.toFun = u.toFun

noncomputable def HCPolySupport.H1Function.castDomain {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1Function U) : H1Function V

Transport of an H¹ function along an equality of domains, retaining its value and weak gradient.

Equations

• HCPolySupport.H1Function.castDomain hUV u = hUV ▸ u

@[simp]

theorem HCPolySupport.H1Function.grad_castDomain {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1Function U) : (castDomain hUV u).grad = u.grad

@[simp]

theorem HCPolySupport.H1Function.toFun_castDomain {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H1Function U) : (castDomain hUV u).toFun = u.toFun

noncomputable def HCPolySupport.H1Function.toCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : H1Function (cubeSet Q)

Promote an H¹ witness on an open triadic cube to the corresponding half-open triadic cube.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.H1Function.grad_toCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : u.toCubeSet.grad = u.grad

@[simp]

theorem HCPolySupport.H1Function.toFun_toCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : u.toCubeSet.toFun = u.toFun

noncomputable def HCPolySupport.H1Function.toOpenCubeSet {d : ℕ} {Q : TriadicCube d} (u : H1Function (cubeSet Q)) : H1Function (openCubeSet Q)

Restrict an H¹ witness on a half-open triadic cube to its open realization.

Equations

• u.toOpenCubeSet = u.restrict ⋯ ⋯

@[simp]

theorem HCPolySupport.H1Function.grad_toOpenCubeSet {d : ℕ} {Q : TriadicCube d} (u : H1Function (cubeSet Q)) : u.toOpenCubeSet.grad = u.grad

@[simp]

theorem HCPolySupport.H1Function.toFun_toOpenCubeSet {d : ℕ} {Q : TriadicCube d} (u : H1Function (cubeSet Q)) : u.toOpenCubeSet.toFun = u.toFun

noncomputable def HCPolySupport.H10Function.castDomain {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H10Function U) : H10Function V

Transport of a zero-trace H¹ function along an equality of domains.

Equations

• HCPolySupport.H10Function.castDomain hUV u = hUV ▸ u

@[simp]

theorem HCPolySupport.H10Function.castDomain_toH1Function_grad {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H10Function U) : (castDomain hUV u).grad = u.grad

@[simp]

theorem HCPolySupport.H10Function.castDomain_toH1Function_toFun {d : ℕ} {U V : Set (Vec d)} (hUV : U = V) (u : H10Function U) : (castDomain hUV u).toFun = u.toFun

noncomputable def HCPolySupport.H10Function.toCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (openCubeSet Q)) : H10Function (cubeSet Q)

Promote an H¹₀ witness on an open triadic cube to the corresponding half-open triadic cube.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.H10Function.toCubeSet_toH1Function_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (openCubeSet Q)) : u.toCubeSet.grad = u.grad

@[simp]

theorem HCPolySupport.H10Function.toCubeSet_toH1Function_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (openCubeSet Q)) : u.toCubeSet.toFun = u.toFun

noncomputable def HCPolySupport.H10Function.toOpenCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (cubeSet Q)) : H10Function (openCubeSet Q)

Restrict an H¹₀ witness on a half-open triadic cube to the corresponding open triadic cube.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.H10Function.toOpenCubeSet_toH1Function_grad {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (cubeSet Q)) : u.toOpenCubeSet.grad = u.grad

@[simp]

theorem HCPolySupport.H10Function.toOpenCubeSet_toH1Function_toFun {d : ℕ} [NeZero d] {Q : TriadicCube d} (u : H10Function (cubeSet Q)) : u.toOpenCubeSet.toFun = u.toFun

theorem HCPolySupport.isPotentialOn_openCubeSet_triadicCube_of_cubeSet {d : ℕ} {Q : TriadicCube d} {f : Vec d → Vec d} (hf : IsPotentialOn (cubeSet Q) f) : IsPotentialOn (openCubeSet Q) f

theorem HCPolySupport.isPotentialOn_cubeSet_triadicCube_of_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {f : Vec d → Vec d} (hf : IsPotentialOn (openCubeSet Q) f) : IsPotentialOn (cubeSet Q) f

theorem HCPolySupport.isPotentialOn_cubeSet_triadicCube_iff_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {f : Vec d → Vec d} : IsPotentialOn (cubeSet Q) f ↔ IsPotentialOn (openCubeSet Q) f

theorem HCPolySupport.isPotentialZeroTraceOn_openCubeSet_triadicCube_of_cubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn (cubeSet Q) f) : IsPotentialZeroTraceOn (openCubeSet Q) f

theorem HCPolySupport.isPotentialZeroTraceOn_cubeSet_triadicCube_of_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn (openCubeSet Q) f) : IsPotentialZeroTraceOn (cubeSet Q) f

theorem HCPolySupport.isPotentialZeroTraceOn_cubeSet_triadicCube_iff_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {f : Vec d → Vec d} : IsPotentialZeroTraceOn (cubeSet Q) f ↔ IsPotentialZeroTraceOn (openCubeSet Q) f

theorem HCPolySupport.isSolenoidalOn_cubeSet_triadicCube_of_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {g : Vec d → Vec d} (hg : IsSolenoidalOn (openCubeSet Q) g) : IsSolenoidalOn (cubeSet Q) g

theorem HCPolySupport.isSolenoidalOn_openCubeSet_triadicCube_of_cubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {g : Vec d → Vec d} (hg : IsSolenoidalOn (cubeSet Q) g) : IsSolenoidalOn (openCubeSet Q) g

theorem HCPolySupport.isSolenoidalOn_cubeSet_triadicCube_iff_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {g : Vec d → Vec d} : IsSolenoidalOn (cubeSet Q) g ↔ IsSolenoidalOn (openCubeSet Q) g

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_cubeSet_triadicCube_of_openCubeSet {d : ℕ} {Q : TriadicCube d} {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn (openCubeSet Q) g) : IsSolenoidalZeroNormalTraceOn (cubeSet Q) g

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_openCubeSet_triadicCube_of_cubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {g : Vec d → Vec d} (hg : IsSolenoidalZeroNormalTraceOn (cubeSet Q) g) : IsSolenoidalZeroNormalTraceOn (openCubeSet Q) g

theorem HCPolySupport.isSolenoidalZeroNormalTraceOn_cubeSet_triadicCube_iff_openCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {g : Vec d → Vec d} : IsSolenoidalZeroNormalTraceOn (cubeSet Q) g ↔ IsSolenoidalZeroNormalTraceOn (openCubeSet Q) g

theorem HCPolySupport.IsPotentialOn.restrict_cubeSet_of_mem_descendantsAtDepth {d : ℕ} [NeZero d] {Q R : TriadicCube d} {n : ℕ} {u : Vec d → Vec d} (hu : IsPotentialOn (cubeSet Q) u) (hR : R ∈ descendantsAtDepth Q n) : IsPotentialOn (cubeSet R) u

Restrict a potential field on a half-open triadic cube to a descendant half-open triadic cube.

theorem HCPolySupport.IsSolenoidalOn.restrict_cubeSet_of_mem_descendantsAtDepth {d : ℕ} [NeZero d] {Q R : TriadicCube d} {n : ℕ} {F : Vec d → Vec d} (hF : IsSolenoidalOn (cubeSet Q) F) (hR : R ∈ descendantsAtDepth Q n) (hmemR : MemVectorL2 (cubeSet R) F) : IsSolenoidalOn (cubeSet R) F

Restrict a solenoidal field on a half-open triadic cube to a descendant half-open triadic cube.