ConstantDatumCoreEnergy

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The interior Caccioppoli energy through a constant-datum comparison

The interior specialization of l.coarse.grained.Caccioppoli.RHS used by the proved interior lane (CaccioppoliInteriorDatum.exists_interiorCaccioppoliEnergy_subConst) applies CoarseGraining's boundary theorem to u - c and pays CoarseGraining's own force leg t^{-8} λ_{t,1}^{-1} [g]². This module runs the comparison form instead:

  E_core(∇u) = E_core(∇(u-c))
      ≤ 2 E_core(∇((u-c) - ρ)) + 2 E_core(∇ρ)
      ≤ 2 P (λ_{t,1} 3^{-2m} ‖(u-c) - ρ‖²_{L²(Q)}) + 2 · 18^d · E_Q(∇ρ) ,

where ρ is the cube's own zero-trace corrector at the same force g. The difference (u-c) - ρ solves the homogeneous equation, so CoarseGraining's force leg disappears from the Caccioppoli application altogether; the force reappears only through the two corrector bounds of ConstantDatumCorrector, both of which carry λ_{t,2}^{-1} explicitly and only t^{-3}. Splitting the L² object and inserting them gives the display of exists_constantDatumCoreEnergy below:

  E_core(∇u) ≤ K ( P λ_{t,1} ( 3^{-2m} ‖u - c‖²_{L²(Q)}
                              + (t^{-3} λ_{t,2}^{-1} [g]_{B^{2t}(Q)})² )
                  + t^{-3} λ_{t,2}^{-1} [g]²_{B^{2t}(Q)} ) .

The comparison object is c + ρ, i.e. the Dirichlet solution with the constant datum c; the two ∇h legs of the printed boundary display vanish for it, which is why no boundary-gradient term appears. Nothing here uses the good event: the display is deterministic and keeps λ_{t,1}, λ_{t,2} separate.

What this buys (disclosed)

Against the proved interior display, the force envelope improves from t^{-8} to t^{-6} provided the caller can pay λ_{t,1} λ_{t,2}^{-2} ≲ σ^{-1} — which is exactly what the frozen theorem's good event gives. Nothing is gained deterministically: with only CoarseGraining's generic ellipticity comparison the two displays agree.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS; e.energy.bound.interior.
• CoarseGraining, Book/Ch03/Theorems/CoarseCaccioppoli/*, Book/Ch03/Theorems/CoarsePoincare.lean.

1. The L² split

theorem Algsuperdiff.Section4.Provider.ExcessDecay.normalizedL2SqOnSet_sub_le_two_add_two {d : ℕ} (Q : HCPolySupport.TriadicCube d) {f h : HCPolySupport.Vec d → ℝ} (hf : MeasureTheory.MemLp f 2 (HCPolySupport.normalizedCubeMeasure Q)) (hh : MeasureTheory.MemLp h 2 (HCPolySupport.normalizedCubeMeasure Q)) : (HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => f y - h y) ≤ 2 * HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) f + 2 * HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) h

The normalized L² triangle inequality on the open cube, in the squared form the Caccioppoli display consumes.

2. The composition, on abstract reals

3. The constant-datum core-energy display

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_constantDatumCoreEnergy (d : ℕ) [NeZero d] : ∃ (C₁ : ℝ) (K : ℝ), 0 < C₁ ∧ 0 < K ∧ ∀ {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {t c : ℝ} {x : HCPolySupport.Vec d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier), HCPolySupport.Book.Ch03.IsForcedEquation Q a u g → 0 < t → t ≤ 1 / 4 → HCPolySupport.Book.Ch03.openCubeAtScale x (Q.scale - 1) ⊆ HCPolySupport.openCubeSet Q → HCPolySupport.Book.Ch03.ForceBesovRegularity Q (2 * t) g → HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet Q x) (a.coeffOn Q) u ≤ K * (HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor C₁ Q a (1 / 4) t * HCPolySupport.Book.Ch02.lambdaS Q t a * ((Real.rpow 3 (-2 * ↑Q.scale) * HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => u.toFun y - c) + (t.rpow (-3) * (HCPolySupport.Book.Ch02.lambdaSq Q t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a).rpow (-1) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g) ^ 2) + t.rpow (-3) * (HCPolySupport.Book.Ch02.lambdaSq Q t (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a).rpow (-1) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g ^ 2)

The interior Caccioppoli energy through the constant-datum comparison.

See the module docstring for the display. The comparison solution is c + ρ with ρ the cube's own zero-trace corrector; the boundary-gradient legs of the printed display vanish because the datum is constant, and the Caccioppoli force leg vanishes because the difference solves the homogeneous equation.