LevelEnergy

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

The coupled level-energy estimate

Derivation of the generic De Giorgi core's level-energy hypothesis from the coupled weak form. Given the representation package (v, v*) solving CoupledWeakForm on a cube U, the measurable representatives w₁ ≈ v − ½p·x, w₂ ≈ −v* + ½p·x share a trace and satisfy, for every median level m₀ and every k ≥ 0, ∑ᵢ‖1_{A_k¹}∂ᵢw₁‖₂ + ∑ᵢ‖1_{A_k²}∂ᵢw₂‖₂ ≤ E₀·√(|A_k¹|+|A_k²|), with E₀ = 2√d·M, M = √(Θ|p|²+|q|²).

The core mechanism: testing CoupledWeakForm at the truncation pair (f_k, −g_k) (D1/D4) produces the level energy identity E_k = ∫_{A¹}(q−½ap)·∇w₁ + ∫_{A²}(½aᵗp)·∇w₂, which the s-metric Young inequality (symmForm_young, t = 1) and the coefficient bounds (symmPartInv_bulkV_le, symmPartInv_bulkVstar_le) drive to E_k ≤ 2M²|A_k|; then s ≥ 1 and a Cauchy–Schwarz on the 2d coordinate norms give the √-shaped conclusion.

Measurable representative of an H¹ function

theorem HCPolySupport.exists_measurableRep {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : ∃ (w : H1Function U), Measurable w.toFun ∧ w.toFun =ᵐ[MeasureTheory.volume.restrict U] u.toFun ∧ w.grad = u.grad

Every H¹ function has a measurable representative: an H¹ function with the same weak gradient and a measurable value function almost everywhere equal to the original. This is the swap needed to feed the De Giorgi core, whose truncation toolbox requires Measurable toFun.

H¹₀ membership transfers along a.e.-equality

theorem HCPolySupport.h1grad_ae_eq_of_toFun_ae_eq {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {u v : H1Function U} (huv : u.toFun =ᵐ[MeasureTheory.volume.restrict U] v.toFun) : u.grad =ᵐ[MeasureTheory.volume.restrict U] v.grad

Uniqueness of weak gradients under a.e.-equal values (open domain).

theorem HCPolySupport.memH10_of_ae_eq_h10 {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) (h : H1Function U) (W : H10Function U) (hae : h.toFun =ᵐ[MeasureTheory.volume.restrict U] W.toFun) : MemH10 U h.toFun

H¹₀ a.e.-transfer. If h : H¹(U) is a.e. equal to the value function of an H¹₀(U) witness W, then h.toFun ∈ H¹₀(U). (Constant-sequence application of the H¹₀-limit closure.)

Sign flip of the coupled weak form

theorem HCPolySupport.coupledWeakForm_neg {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {q : Vec d} {v vstar : H1Function U} (h : CoupledWeakForm a U q v vstar) : CoupledWeakForm a U (-q) (-v) (-vstar)

The coupled weak form is odd in (q, v, v*).

The affine H¹ function x ↦ ½ p·x on a bounded domain

noncomputable def HCPolySupport.affineHalfOn {d : ℕ} {U : Set (Vec d)} (hUm : MeasurableSet U) (hUb : IsBoundedDomain U) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (p : Vec d) : H1Function U

x ↦ ½ p·x as an H¹ function on a bounded measurable domain, assembled from the coordinate H¹ functions. Constant gradient ½ p.

Equations

• HCPolySupport.affineHalfOn hUm hUb p = ∑ i : Fin d, (1 / 2 * p i) • HCPolySupport.H1Function.coordOnIsBoundedDomain hUm hUb i

@[simp]

theorem HCPolySupport.affineHalfOn_grad {d : ℕ} {U : Set (Vec d)} (hUm : MeasurableSet U) (hUb : IsBoundedDomain U) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (p : Vec d) : (affineHalfOn hUm hUb p).grad = fun (x : Vec d) => (1 / 2) • p

@[simp]

theorem HCPolySupport.affineHalfOn_toFun {d : ℕ} {U : Set (Vec d)} (hUm : MeasurableSet U) (hUb : IsBoundedDomain U) [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (p : Vec d) : (affineHalfOn hUm hUb p).toFun = fun (x : Vec d) => 1 / 2 * vecDot p x

A subset-restricted indicator integral

theorem HCPolySupport.setIntegral_indicator_subset {d : ℕ} {U A : Set (Vec d)} (hAm : MeasurableSet A) (hAU : A ⊆ U) (f : Vec d → ℝ) : ∫ (x : Vec d) in U, A.indicator f x = ∫ (x : Vec d) in A, f x

For A ⊆ U measurable, integrating A.indicator f over U is the same as integrating f over A.

The level-energy identity

theorem HCPolySupport.levelEnergy_identity {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {Θ : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ U a) {p q : Vec d} {v vstar : H1Function U} (hCWF : CoupledWeakForm a U q v vstar) {w₁ w₂ : H1Function U} (hw1meas : Measurable w₁.toFun) (hw2meas : Measurable w₂.toFun) (hw1g : ∀ (x : Vec d), w₁.grad x = v.grad x - (1 / 2) • p) (hw2g : ∀ (x : Vec d), w₂.grad x = -vstar.grad x + (1 / 2) • p) (hmatch : MemH10 U fun (x : Vec d) => w₁.toFun x - w₂.toFun x) (m₀ k : ℝ) : (∫ (x : Vec d) in {x : Vec d | x ∈ U ∧ m₀ + k < w₁.toFun x}, vecDot (w₁.grad x) (matVecMul (symmPart (a x)) (w₁.grad x))) + ∫ (x : Vec d) in {x : Vec d | x ∈ U ∧ m₀ + k < w₂.toFun x}, vecDot (w₂.grad x) (matVecMul (symmPart (a x)) (w₂.grad x)) = (∫ (x : Vec d) in {x : Vec d | x ∈ U ∧ m₀ + k < w₁.toFun x}, vecDot (q - (1 / 2) • matVecMul (a x) p) (w₁.grad x)) + ∫ (x : Vec d) in {x : Vec d | x ∈ U ∧ m₀ + k < w₂.toFun x}, vecDot ((1 / 2) • matVecMul (matTranspose (a x)) p) (w₂.grad x)

Level-energy identity. Testing the coupled weak form at the truncation pair (f_k, −g_k) yields E_k = ∫_{A₁}(q−½ap)·∇w₁ + ∫_{A₂}(½aᵗp)·∇w₂, where E_k = ∫_{A₁}∇w₁·s∇w₁ + ∫_{A₂}∇w₂·s∇w₂ and Aᵢ = {wᵢ > m₀+k}.

The squared level-energy bound

theorem HCPolySupport.levelEnergy_sq_bound {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {Θ : ℝ} (hΘ : 0 ≤ Θ) {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ U a) {p q : Vec d} {v vstar : H1Function U} (hCWF : CoupledWeakForm a U q v vstar) {w₁ w₂ : H1Function U} (hw1meas : Measurable w₁.toFun) (hw2meas : Measurable w₂.toFun) (hw1g : ∀ (x : Vec d), w₁.grad x = v.grad x - (1 / 2) • p) (hw2g : ∀ (x : Vec d), w₂.grad x = -vstar.grad x + (1 / 2) • p) (hmatch : MemH10 U fun (x : Vec d) => w₁.toFun x - w₂.toFun x) (m₀ k : ℝ) : (∫ (x : Vec d) in {x : Vec d | x ∈ U ∧ m₀ + k < w₁.toFun x}, vecDot (w₁.grad x) (matVecMul (symmPart (a x)) (w₁.grad x))) + ∫ (x : Vec d) in {x : Vec d | x ∈ U ∧ m₀ + k < w₂.toFun x}, vecDot (w₂.grad x) (matVecMul (symmPart (a x)) (w₂.grad x)) ≤ 2 * (Θ * vecNormSq p + vecNormSq q) * ((MeasureTheory.volume {x : Vec d | x ∈ U ∧ m₀ + k < w₁.toFun x}).toReal + (MeasureTheory.volume {x : Vec d | x ∈ U ∧ m₀ + k < w₂.toFun x}).toReal)

Squared level-energy bound. E_k ≤ 2M²·|A_k|, obtained from the identity by the s-metric Young inequality (t = 1) and the coefficient bounds.

From the squared bound to the √-shaped level-energy estimate

theorem HCPolySupport.sumCoordNorm_le {d : ℕ} {U : Set (Vec d)} {Θ : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ U a) (w₁ w₂ : H1Function U) {A₁ A₂ : Set (Vec d)} (hA1m : MeasurableSet A₁) (hA2m : MeasurableSet A₂) (hA1U : A₁ ⊆ U) (hA2U : A₂ ⊆ U) {M2 : ℝ} (hM2 : 0 ≤ M2) (hEbound : (∫ (x : Vec d) in A₁, vecDot (w₁.grad x) (matVecMul (symmPart (a x)) (w₁.grad x))) + ∫ (x : Vec d) in A₂, vecDot (w₂.grad x) (matVecMul (symmPart (a x)) (w₂.grad x)) ≤ 2 * M2 * ((MeasureTheory.volume A₁).toReal + (MeasureTheory.volume A₂).toReal)) : ∑ i : Fin d, (MeasureTheory.eLpNorm (A₁.indicator fun (x : Vec d) => w₁.grad x i) 2 (volumeMeasureOn U)).toReal + ∑ i : Fin d, (MeasureTheory.eLpNorm (A₂.indicator fun (x : Vec d) => w₂.grad x i) 2 (volumeMeasureOn U)).toReal ≤ 2 * √↑d * √M2 * √((MeasureTheory.volume A₁).toReal + (MeasureTheory.volume A₂).toReal)

Coordinate-norm packaging. Given E_k ≤ 2M²·|A_k|, the sum of the coordinate L² norms of the truncated gradients is bounded by 2√d·M·√|A_k|, via s ≥ 1 and a Cauchy–Schwarz on the 2d coordinate norms.

Part C deliverable — the coupled level-energy estimate

theorem HCPolySupport.coupled_levelEnergy {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {Θ : ℝ} (hΘ : 0 ≤ Θ) {a : CoeffField d} (hEll : IsEllipticFieldOn 1 Θ U a) {p q : Vec d} {v vstar : H1Function U} (hCWF : CoupledWeakForm a U q v vstar) (htrace : MemH10 U fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot p x) : ∃ (w₁ : H1Function U) (w₂ : H1Function U), Measurable w₁.toFun ∧ Measurable w₂.toFun ∧ (w₁.toFun =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => v.toFun x - 1 / 2 * vecDot p x) ∧ (w₂.toFun =ᵐ[MeasureTheory.volume.restrict U] fun (x : Vec d) => -vstar.toFun x + 1 / 2 * vecDot p x) ∧ (MemH10 U fun (x : Vec d) => w₁.toFun x - w₂.toFun x) ∧ ∀ (m₀ k : ℝ), 0 ≤ k → ∑ i : Fin d, (MeasureTheory.eLpNorm ({x : Vec d | x ∈ U ∧ m₀ + k < w₁.toFun x}.indicator fun (x : Vec d) => w₁.grad x i) 2 (volumeMeasureOn U)).toReal + ∑ i : Fin d, (MeasureTheory.eLpNorm ({x : Vec d | x ∈ U ∧ m₀ + k < w₂.toFun x}.indicator fun (x : Vec d) => w₂.grad x i) 2 (volumeMeasureOn U)).toReal ≤ 2 * √↑d * √(Θ * vecNormSq p + vecNormSq q) * √((MeasureTheory.volume {x : Vec d | x ∈ U ∧ m₀ + k < w₁.toFun x}).toReal + (MeasureTheory.volume {x : Vec d | x ∈ U ∧ m₀ + k < w₂.toFun x}).toReal)

Coupled level-energy estimate. From the coupled weak form, the measurable representatives w₁ ≈ v − ½p·x, w₂ ≈ −v* + ½p·x share a trace and satisfy the De Giorgi core's level-energy hypothesis with E₀ = 2√d·√(Θ|p|²+|q|²).