CaccioppoliInteriorDatum

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

The interior regime of the coarse-grained Caccioppoli inequality with

CoarseGraining proves ABK26's l.coarse.grained.Caccioppoli.RHS in its boundary form: the datum BoundaryForcedCaccioppoliDatum Q a x g bundles a forced H¹(Q) solution together with the localized zero-trace condition

  LocalizedZeroTraceFunctionOn (□_Q) (x + □_{Q.scale-1}) u ,

i.e. "u vanishes on the part of ∂Q seen through the Dirichlet patch". This module observes that in the interior regime — the regime the frozen theorem's frontier-empty clause selects, where the patch is a compact subset of Q and the Dirichlet locus ∂Q ∩ (x + □_{Q.scale-1}) is empty — that condition is automatic: multiplying by a smooth cutoff supported inside Q proves in H¹₀(Q) for every H¹(Q) function. So the boundary theorem's interior specialization is unconditional in the boundary data, which is exactly the statement needs ("the h-term vanishes").

Two further steps are performed here:

• the geometric hypothesis is reduced to one inclusion. CoarseGraining asks for both x ∈ □_Q and the patch condition; the patch inclusion implies the former (the patch contains its own centre).

What is not done here

Nothing in this module identifies the coefficient field of the frozen theorem's Dirichlet problem on □_m with a CoeffFamily at the parent cube, and nothing restricts an equation from □_m to the parent: both are inputs, supplied by the caller. The module is purely the interior specialization of CoarseGraining's theorem plus the constant shift.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS.
• ABK26, e.energy.bound.interior.

1. The interior regime makes the localized zero trace automatic

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedZeroTraceFunctionOn_of_memH1 {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) (hVU : V ⊆ U) {u : HCPolySupport.Vec d → ℝ} (hu : HCPolySupport.MemH1 U u) : HCPolySupport.LocalizedZeroTraceFunctionOn U V u

The interior localization. If the localization window sits inside a bounded open convex domain, then every H¹ function of that domain satisfies the localized zero-trace condition: a smooth cutoff supported in the window has compact support inside the domain, so the product is an admissible H¹₀ test function. This is the Lean content of "in the interior regime the Dirichlet locus is empty".

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_openCubeAtScale_self {d : ℕ} (x : HCPolySupport.Vec d) (m : ℤ) : x ∈ HCPolySupport.Book.Ch03.openCubeAtScale x m

A cube window contains its own centre.

2. The interior forced datum, with a constant subtracted

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.constH1 {d : ℕ} (Q : HCPolySupport.TriadicCube d) (c : ℝ) : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier

The constant function as an H¹ function of a cube.

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.constH1 Q c = Algsuperdiff.Section4.Provider.ExcessDecay.constantDatumH1 Q c

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sub_constH1_grad {d : ℕ} (Q : HCPolySupport.TriadicCube d) (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) (c : ℝ) : (u - constH1 Q c).grad = u.grad

The gradient of a constant-shifted H¹ function.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.interiorForcedCaccioppoliDatumSubConst {d : ℕ} {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} (x : HCPolySupport.Vec d) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) (c : ℝ) (hu : HCPolySupport.Book.Ch03.IsForcedEquation Q a u g) (hpatch : HCPolySupport.Book.Ch03.openCubeAtScale x (Q.scale - 1) ⊆ HCPolySupport.openCubeSet Q) : HCPolySupport.Book.Ch03.BoundaryForcedCaccioppoliDatum Q a x g

The interior forced Caccioppoli datum with a constant subtracted.

The equation is unchanged (it only sees ∇u), and the localized zero-trace condition is discharged by the interior localization. This is the object the interior regime feeds to CoarseGraining's boundary theorem.

Equations

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

3. The interior energy estimate

theorem Algsuperdiff.Section4.Provider.ExcessDecay.localizedCoeffEnergyValue_congr_grad {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (V : Set (HCPolySupport.Vec d)) (a : HCPolySupport.Book.Ch02.CoeffOn U) {u v : HCPolySupport.H1Function U.carrier} (hgrad : v.grad = u.grad) : HCPolySupport.Book.Ch03.localizedCoeffEnergyValue V a v = HCPolySupport.Book.Ch03.localizedCoeffEnergyValue V a u

The local coefficient energy sees only the gradient.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_interiorCaccioppoliEnergy_subConst (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {s t : ℝ} {x : HCPolySupport.Vec d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (u : HCPolySupport.H1Function (HCPolySupport.Book.Ch02.cubeDomain Q).carrier) (c : ℝ), HCPolySupport.Book.Ch03.IsForcedEquation Q a u g → 0 < s → s < 1 → 0 < t → t < 1 / 2 → s + t < 1 → 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 ≤ HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor C Q a s 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 (-8) / (1 - 2 * t) * (HCPolySupport.Book.Ch02.lambdaS Q t a).rpow (-1) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q (2 * t) g ^ 2)

The interior coarse-grained Caccioppoli inequality with right-hand side, mean-subtracted.

For every forced H¹(Q) solution whose Dirichlet patch x + □_{Q.scale-1} sits inside Q (the interior regime) and every real c,

  ⨍_{□_Q ∩ (x+□_{Q.scale-2})} ∇u · ã ∇u
      ≤  prefactor(C,Q,a,s,t)
         ( λ_{t,1} 3^{-2·scale} ‖u - c‖²_{L²(Q)}
           + t^{-8}(1-2t)^{-1} λ_{t,1}^{-1} [g]²_{B^{2t}(Q)} ) ,

with prefactor CoarseGraining's caccioppoliWithRHSPrefactor, i.e. the printed (C/σ)^{2+4s/σ} s^{-2s/σ} Θ_{s,t}^{(1-t)/σ} at σ = 1-s-t.

Only the boundary data has been specialized (to the interior regime); the ∇h-term of the printed lemma is absent because CoarseGraining's datum carries the homogeneous localized trace.