Coarse-graining support: Support.PDE.HarmonicCube

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

Harmonic functions on triadic subcubes

This file packages the general restriction theorem for AHarmonicFunction as a cube-facing API. The half-open cubeSet transport layer is intentionally kept separate; on open cubes the restriction follows directly from descendant containment and monotonicity of ellipticity.

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

Transport a harmonic function along an equality of domains.

Equations

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

noncomputable def HCPolySupport.AHarmonicFunction.castCoeff {d : ℕ} {a b : CoeffField d} {U : Set (Vec d)} (hab : a = b) (u : AHarmonicFunction a U) : AHarmonicFunction b U

Transport a harmonic function along an equality of coefficient fields.

Equations

• HCPolySupport.AHarmonicFunction.castCoeff hab u = hab ▸ u

@[simp]

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

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_castCoeff {d : ℕ} {a b : CoeffField d} {U : Set (Vec d)} (hab : a = b) (u : AHarmonicFunction a U) : (castCoeff hab u).toH1.grad = u.toH1.grad

theorem HCPolySupport.AHarmonicFunction.isAHarmonicGradient_cubeSet_originCube_iff_openCubeSet {d : ℕ} [NeZero d] {n : ℤ} {a : CoeffField d} {f : Vec d → Vec d} : IsAHarmonicGradient a (cubeSet (originCube d n)) f ↔ IsAHarmonicGradient a (openCubeSet (originCube d n)) f

noncomputable def HCPolySupport.AHarmonicFunction.toCubeSetOriginCube {d : ℕ} [NeZero d] {n : ℤ} {a : CoeffField d} (u : AHarmonicFunction a (openCubeSet (originCube d n))) : AHarmonicFunction a (cubeSet (originCube d n))

Regard a harmonic function on an open origin cube as one on its half-open cube.

Equations

• u.toCubeSetOriginCube = { toH1 := u.toH1.toCubeSetOriginCube, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_toCubeSetOriginCube {d : ℕ} [NeZero d] {n : ℤ} {a : CoeffField d} (u : AHarmonicFunction a (openCubeSet (originCube d n))) : u.toCubeSetOriginCube.toH1.grad = u.toH1.grad

noncomputable def HCPolySupport.AHarmonicFunction.toOpenCubeSetOriginCube {d : ℕ} [NeZero d] {n : ℤ} {a : CoeffField d} (u : AHarmonicFunction a (cubeSet (originCube d n))) : AHarmonicFunction a (openCubeSet (originCube d n))

Restrict a harmonic function on a half-open origin cube to its open cube.

Equations

• u.toOpenCubeSetOriginCube = { toH1 := u.toH1.restrict ⋯ ⋯, isHarmonic := ⋯ }

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_toOpenCubeSetOriginCube {d : ℕ} [NeZero d] {n : ℤ} {a : CoeffField d} (u : AHarmonicFunction a (cubeSet (originCube d n))) : u.toOpenCubeSetOriginCube.toH1.grad = u.toH1.grad

noncomputable def HCPolySupport.AHarmonicFunction.toCubeSetOrigin {d : ℕ} {a : CoeffField d} (Q : TriadicCube d) (u : AHarmonicFunction a (cubeSet Q)) : AHarmonicFunction (translateCoeffField (triadicCubeShift Q) a) (cubeSet (originCube d Q.scale))

Translate a harmonic function on a half-open cube to the origin cube of the same scale, with the correspondingly translated coefficient field.

Equations

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

noncomputable def HCPolySupport.AHarmonicFunction.toOpenCubeSetOrigin {d : ℕ} {a : CoeffField d} (Q : TriadicCube d) (u : AHarmonicFunction a (openCubeSet Q)) : AHarmonicFunction (translateCoeffField (triadicCubeShift Q) a) (openCubeSet (originCube d Q.scale))

Translate a harmonic function on an open cube to the open origin cube of the same scale, with the correspondingly translated coefficient field.

Equations

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

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

Restrict a harmonic function on a half-open cube to the corresponding open cube.

Equations

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

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

Regard a harmonic function on an open cube as one on the corresponding half-open cube.

Equations

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

noncomputable def HCPolySupport.AHarmonicFunction.restrictToOpenSubcube {d : ℕ} {a : CoeffField d} {lam Lam : ℝ} {Q R : TriadicCube d} {j : ℕ} (u : AHarmonicFunction a (openCubeSet Q)) (hEllQ : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) : AHarmonicFunction a (openCubeSet R)

Restrict an A-harmonic function on an open triadic cube to an open descendant cube.

Equations

• u.restrictToOpenSubcube hEllQ hR = u.restrictOfIsEllipticFieldOn ⋯ ⋯ ⋯ ⋯

@[simp]

theorem HCPolySupport.AHarmonicFunction.toH1_restrictToOpenSubcube {d : ℕ} {a : CoeffField d} {lam Lam : ℝ} {Q R : TriadicCube d} {j : ℕ} (u : AHarmonicFunction a (openCubeSet Q)) (hEllQ : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToOpenSubcube hEllQ hR).toH1 = u.toH1.restrict ⋯ ⋯

theorem HCPolySupport.AHarmonicFunction.grad_restrictToOpenSubcube {d : ℕ} {a : CoeffField d} {lam Lam : ℝ} {Q R : TriadicCube d} {j : ℕ} (u : AHarmonicFunction a (openCubeSet Q)) (hEllQ : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToOpenSubcube hEllQ hR).toH1.grad = u.toH1.grad

noncomputable def HCPolySupport.AHarmonicFunction.restrictToSubcube {d : ℕ} [NeZero d] {a : CoeffField d} {lam Lam : ℝ} {Q R : TriadicCube d} {j : ℕ} (u : AHarmonicFunction a (cubeSet Q)) (hEllQ : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) : AHarmonicFunction a (cubeSet R)

Restrict a harmonic function to a descendant half-open cube under parent-cube ellipticity.

Equations

• u.restrictToSubcube hEllQ hR = (u.toOpenCubeSet.restrictToOpenSubcube ⋯ hR).toCubeSet

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_toOpenCubeSet {d : ℕ} [NeZero d] {Q : TriadicCube d} {a : CoeffField d} (u : AHarmonicFunction a (cubeSet Q)) : u.toOpenCubeSet.toH1.grad = u.toH1.grad

@[simp]

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

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_restrictToSubcube {d : ℕ} [NeZero d] {a : CoeffField d} {lam Lam : ℝ} {Q R : TriadicCube d} {j : ℕ} (u : AHarmonicFunction a (cubeSet Q)) (hEllQ : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToSubcube hEllQ hR).toH1.grad = u.toH1.grad

noncomputable def HCPolySupport.AHarmonicFunction.restrictToSubcubeOfOpenElliptic {d : ℕ} [NeZero d] {a : CoeffField d} {lam Lam : ℝ} {Q R : TriadicCube d} {j : ℕ} (u : AHarmonicFunction a (cubeSet Q)) (hEllOpenQ : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) : AHarmonicFunction a (cubeSet R)

Restrict a cubeSet harmonic function to a descendant cubeSet when ellipticity is known on the parent open cube.

This is the a.e.-ellipticity-friendly variant used by Section 5.3: the restriction proof happens on open cubes, and the result is transported back to the half-open cubeSet.

Equations

• u.restrictToSubcubeOfOpenElliptic hEllOpenQ hR = (u.toOpenCubeSet.restrictToOpenSubcube hEllOpenQ hR).toCubeSet

@[simp]

theorem HCPolySupport.AHarmonicFunction.grad_restrictToSubcubeOfOpenElliptic {d : ℕ} [NeZero d] {a : CoeffField d} {lam Lam : ℝ} {Q R : TriadicCube d} {j : ℕ} (u : AHarmonicFunction a (cubeSet Q)) (hEllOpenQ : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToSubcubeOfOpenElliptic hEllOpenQ hR).toH1.grad = u.toH1.grad