LocalEnergy

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

Local block energy (Prop 3.4)

The two consumer theorems, assembled from the test identity (energyIntegral_eq_bulk_add_cutoff) and the pointwise bulk/cutoff estimates (bulkIntegrand_le, cutoffIntegrand_le).

• centered_local_block_energy (T1): the 𝓔-level bound 𝓔 ≤ C_d (M²·|supp η ∩ U| + Θ·K∞²·∫_U Σᵢ(∂ᵢη)²).
• local_block_energy (T2): the consumer shape ∫_C Z·𝐁Z ≤ C_d (M²·|supp η ∩ U| + Θ·K∞²·∫_U Σᵢ(∂ᵢη)²).

M² = Θ|p|² + |q|². No EuclideanSpace.

Integrability of the two elementary weights

theorem HCPolySupport.integrableOn_sqCutoff {d : ℕ} {m : ℤ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) : MeasureTheory.IntegrableOn (sqCutoff η) (openCubeSet (originCube d m)) MeasureTheory.volume

theorem HCPolySupport.integrableOn_gradEtaSq {d : ℕ} {m : ℤ} {η : Vec d → ℝ} {Gη : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq fun (i : Fin d) => (fderiv ℝ η x) (basisVec i)) (openCubeSet (originCube d m)) MeasureTheory.volume

The squared-gradient norm is integrable on the cube.

∫ η² ≤ |supp η ∩ U|

theorem HCPolySupport.setIntegral_sqCutoff_le {d : ℕ} {m : ℤ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) : ∫ (x : Vec d) in openCubeSet (originCube d m), sqCutoff η x ≤ (MeasureTheory.volume (Function.support η ∩ openCubeSet (originCube d m))).toReal

The two integral estimates

theorem HCPolySupport.setIntegral_bulkIntegrand_le {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) : ∫ (x : Vec d) in openCubeSet (originCube d m), bulkIntegrand a v vstar P η x ≤ (5 * (Θ * vecNormSq P.1 + vecNormSq P.2) * ∫ (x : Vec d) in openCubeSet (originCube d m), sqCutoff η x) + 1 / 8 * ∫ (x : Vec d) in openCubeSet (originCube d m), energyIntegrand a v vstar P η x

theorem HCPolySupport.setIntegral_cutoffIntegrand_le {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} {Gη c Kinf : ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (hKv : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m v P.1 c).toFun x| ≤ Kinf) (hKvs : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m vstar P.1 (-c)).toFun x| ≤ Kinf) : ∫ (x : Vec d) in openCubeSet (originCube d m), cutoffIntegrand a v vstar P c η x ≤ ((1 / 16 * ∫ (x : Vec d) in openCubeSet (originCube d m), energyIntegrand a v vstar P η x) + 2 * (Θ * vecNormSq P.1 + vecNormSq P.2) * ∫ (x : Vec d) in openCubeSet (originCube d m), sqCutoff η x) + 67 * Θ * Kinf ^ 2 * ∫ (x : Vec d) in openCubeSet (originCube d m), vecNormSq fun (i : Fin d) => (fderiv ℝ η x) (basisVec i)

∑ᵢ(∂ᵢη)² = |∇η|² bridge

theorem HCPolySupport.gradEtaSq_eq_vecNormSq {d : ℕ} {η : Vec d → ℝ} (x : Vec d) : ∑ i : Fin d, (fderiv ℝ η x) (basisVec i) ^ 2 = vecNormSq fun (i : Fin d) => (fderiv ℝ η x) (basisVec i)

The coordinate expression of |∇η|² equals its vector norm.

Θ ≥ 0 from ellipticity on the (nonempty) cube

theorem HCPolySupport.theta_nonneg_of_isEllipticFieldOn {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) : 0 ≤ Θ

The ellipticity parameter is nonnegative on the nonempty cube.

T1 — the centered energy bound

theorem HCPolySupport.centered_local_block_energy_num {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} {Gη c Kinf : ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hWeak : CoupledWeakForm a (openCubeSet (originCube d m)) P.2 v vstar) (hTrace : MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot P.1 x) (hKv : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m v P.1 c).toFun x| ≤ Kinf) (hKvs : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m vstar P.1 (-c)).toFun x| ≤ Kinf) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) : ∫ (x : Vec d) in openCubeSet (originCube d m), η x ^ 2 * (vecDot ((centeredPotential m v P.1 c).grad x) (matVecMul (symmPart (a x)) ((centeredPotential m v P.1 c).grad x)) + vecDot ((centeredPotential m vstar P.1 (-c)).grad x) (matVecMul (symmPart (a x)) ((centeredPotential m vstar P.1 (-c)).grad x))) ≤ 128 * ((Θ * vecNormSq P.1 + vecNormSq P.2) * (MeasureTheory.volume (Function.support η ∩ openCubeSet (originCube d m))).toReal + Θ * Kinf ^ 2 * ∫ (x : Vec d) in openCubeSet (originCube d m), ∑ i : Fin d, (fderiv ℝ η x) (basisVec i) ^ 2)

T1 with the explicit numeral 128. The witness of centered_local_block_energy is the fixed dimensional constant 128; this is the same bound stated with that literal so the consumer can see a field-independent constant.

theorem HCPolySupport.centered_local_block_energy {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} {Gη c Kinf : ℝ} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hWeak : CoupledWeakForm a (openCubeSet (originCube d m)) P.2 v vstar) (hTrace : MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot P.1 x) (hKv : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m v P.1 c).toFun x| ≤ Kinf) (hKvs : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m vstar P.1 (-c)).toFun x| ≤ Kinf) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∫ (x : Vec d) in openCubeSet (originCube d m), η x ^ 2 * (vecDot ((centeredPotential m v P.1 c).grad x) (matVecMul (symmPart (a x)) ((centeredPotential m v P.1 c).grad x)) + vecDot ((centeredPotential m vstar P.1 (-c)).grad x) (matVecMul (symmPart (a x)) ((centeredPotential m vstar P.1 (-c)).grad x))) ≤ Cd * ((Θ * vecNormSq P.1 + vecNormSq P.2) * (MeasureTheory.volume (Function.support η ∩ openCubeSet (originCube d m))).toReal + Θ * Kinf ^ 2 * ∫ (x : Vec d) in openCubeSet (originCube d m), ∑ i : Fin d, (fderiv ℝ η x) (basisVec i) ^ 2)

T1 — centered_local_block_energy. The 𝓔-level bound of p.local.block.energy.

T2 — the consumer shape

theorem HCPolySupport.two_symmPart_grad_le {d : ℕ} {Θ : ℝ} {A : Mat d} (hA : IsThetaElliptic Θ A) (gv p : Vec d) : 2 * vecDot gv (matVecMul (symmPart A) gv) ≤ 4 * vecDot (gv - (1 / 2) • p) (matVecMul (symmPart A) (gv - (1 / 2) • p)) + Θ * vecNormSq p

Adding back the affine part: 2∇v·s∇v ≤ 4V·sV + Θ|p|² with V = ∇v − ½p.

theorem HCPolySupport.local_block_energy_uniform {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} {Gη c Kinf : ℝ} {Z : BlockState d} {C : Set (Vec d)} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hWeak : CoupledWeakForm a (openCubeSet (originCube d m)) P.2 v vstar) (hTrace : MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot P.1 x) (hKv : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m v P.1 c).toFun x| ≤ Kinf) (hKvs : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m vstar P.1 (-c)).toFun x| ≤ Kinf) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (hEnergyId : (fun (x : Vec d) => blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField a x) (Z.eval x))) =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] fun (x : Vec d) => 2 * vecDot (v.grad x) (matVecMul (symmPart (a x)) (v.grad x)) + 2 * vecDot (vstar.grad x) (matVecMul (symmPart (a x)) (vstar.grad x))) (hCmeas : MeasurableSet C) (hCU : C ⊆ openCubeSet (originCube d m)) (hηC : ∀ᵐ (x : Vec d) ∂volumeMeasureOn C, η x = 1) : ∫ (x : Vec d) in C, blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField a x) (Z.eval x)) ≤ 514 * ((Θ * vecNormSq P.1 + vecNormSq P.2) * (MeasureTheory.volume (Function.support η ∩ openCubeSet (originCube d m))).toReal + Θ * Kinf ^ 2 * ∫ (x : Vec d) in openCubeSet (originCube d m), ∑ i : Fin d, (fderiv ℝ η x) (basisVec i) ^ 2)

T2 with the explicit numeral 514 = 4·128 + 2. The uniform-constant restatement of local_block_energy: its witness is the field-independent dimensional constant 514, exposed here as a literal so the per-core energy bound can be made uniform over realizations.

theorem HCPolySupport.local_block_energy {d : ℕ} {m : ℤ} {a : CoeffField d} {Θ : ℝ} {v vstar : H1Function (openCubeSet (originCube d m))} {P : BlockVec d} {η : Vec d → ℝ} {Gη c Kinf : ℝ} {Z : BlockState d} {C : Set (Vec d)} (hEllO : IsEllipticFieldOn 1 Θ (openCubeSet (originCube d m)) a) (hWeak : CoupledWeakForm a (openCubeSet (originCube d m)) P.2 v vstar) (hTrace : MemH10 (openCubeSet (originCube d m)) fun (x : Vec d) => v.toFun x + vstar.toFun x - vecDot P.1 x) (hKv : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m v P.1 c).toFun x| ≤ Kinf) (hKvs : ∀ᵐ (x : Vec d) ∂volumeMeasureOn (openCubeSet (originCube d m)), |(centeredPotential m vstar P.1 (-c)).toFun x| ≤ Kinf) (hη : ContDiff ℝ (↑⊤) η) (hIcc : ∀ (x : Vec d), η x ∈ Set.Icc 0 1) (hGη : ∀ (x : Vec d) (i : Fin d), |(fderiv ℝ η x) (basisVec i)| ≤ Gη) (hEnergyId : (fun (x : Vec d) => blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField a x) (Z.eval x))) =ᵐ[volumeMeasureOn (openCubeSet (originCube d m))] fun (x : Vec d) => 2 * vecDot (v.grad x) (matVecMul (symmPart (a x)) (v.grad x)) + 2 * vecDot (vstar.grad x) (matVecMul (symmPart (a x)) (vstar.grad x))) (hCmeas : MeasurableSet C) (hCU : C ⊆ openCubeSet (originCube d m)) (hηC : ∀ᵐ (x : Vec d) ∂volumeMeasureOn C, η x = 1) : ∃ (Cd : ℝ), 0 ≤ Cd ∧ ∫ (x : Vec d) in C, blockVecDot (Z.eval x) (blockMatVecMul (blockCoeffField a x) (Z.eval x)) ≤ Cd * ((Θ * vecNormSq P.1 + vecNormSq P.2) * (MeasureTheory.volume (Function.support η ∩ openCubeSet (originCube d m))).toReal + Θ * Kinf ^ 2 * ∫ (x : Vec d) in openCubeSet (originCube d m), ∑ i : Fin d, (fderiv ℝ η x) (basisVec i) ^ 2)

T2 — local_block_energy. The consumer shape of p.local.block.energy: the block energy on C is controlled by M²·|supp η ∩ U| + Θ·K∞²·∫_U Σᵢ(∂ᵢη)².