StepSevenCaccMatching

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

t.regularity Step 7c: matching l.coarse.grained.Caccioppoli.RHS to the §4.4 data

The target, and the gap this module closes

Step 7c says only

Since n' is a good scale, we may apply the coarse-grained Caccioppoli inequality and the oscillation bound e.oscillation.Holder.bound at scale n' to obtain a gradient bound.

The exponent pin (the one real choice, and it is forced)

The Caccioppoli's forcing slot is 𝐠 ∈ H^{2t}. So the §4.4 datum determines t completely:

      2 t  =  s_{§4.4}  =  1/4       ⟹      t = 1/8 = stepSevenCaccT

and the Caccioppoli's own first exponent is taken to be s_{§4.4} = 1/4 as well, giving

      σ  =  1 - 1/4 - 1/8  =  5/8  >  0 .

Nothing else is available: any other t would measure the forcing at an exponent §4.4 never produces.

The binder-by-binder match

Each binder of l.coarse.grained.Caccioppoli.RHS, against the §4.4 datum that discharges it.

• s ∈ (0,1) ⇝ stepOneS = 1/4. Discharged, stepSevenCaccS_lt_one.
• t ∈ (0,1/2], σ = 1-s-t > 0 ⇝ stepSevenCaccT = 1/8, σ = 5/8. Discharged, stepSevenCaccT_lt_half and the positivity of σ.
• x ∈ □_0 (the Dirichlet-patch centre) ⇝ the good-scale centre: the patch contains its own centre, so the patch inclusion implies it.
• 𝐚 ∈ L^∞(□_0; ℝ_+^{d×d}) ⇝ the truncated field 𝐚_{L,n'} (e.infrared.cutoff.def). Discharged as a CoeffFamily binder.
• u ∈ H^1(□_0) with -∇·𝐚∇u = ∇·𝐠 ⇝ the §4.4 solution on □_m, restricted to the good-scale cube. Discharged by IsForcedEquation together with S4.3's EquationRestriction.
• 𝐠 ∈ H^{2t}(□_0;ℝ^d) ⇝ [𝐠]_{H^{1/4}(U_{n'})}, itself coming from [𝐠]_{W^{1/2,∞}(□_m)}. Discharged at the exponent (2t = 1/4, the pin); the W^{1/2,∞} → H^{1/4} embedding is normalizedGagliardoESeminormOn_stepThreeWindow_quarter_le. What remains: the Gagliardo H^s ↔ CoarseGraining ForceBesovRegularity / scaleNormalizedPositiveBesovVectorSeminormTwo carrier bridge is not performed here.
• h ∈ H^{1+2t}(□_0) with (h)_{□_0} = 0 ⇝ ‖∇h‖_{W^{1/2,∞}(□_m)}. Not dischargeable from any proved source — see the residues below. The mean-zero normalization is itself free: only ∇h and the trace class of u - h are used, and both are invariant under h ↦ h - c.
• the unit-cube normalization □_0 ⇝ the good-scale cube at scale n'. Discharged, and at zero cost: CoarseGraining does not state the lemma at the unit cube. This is the largest single item the manuscript's silence hides.
• the boundary condition u = h on (∂□_0) ∩ (x + □_{-1}) ⇝ §4.4's u = h on ∂□_m.

The two residues, stated exactly

(R1) the ∇h leg is not formalized anywhere. CoarseGraining proves l.coarse.grained.Caccioppoli.RHS only at zero localized boundary data: its datum BoundaryForcedCaccioppoliDatum carries LocalizedZeroTraceFunctionOn, and its right-hand side boundaryCaccioppoliWithRHSRHS has exactly two summands (the parent L² mass and the 𝐠-Besov mass). The printed third summand t^{-3} Λ_t(□_0;𝐚) ‖∇h‖²_{H^{2t}(□_0)} comes from move 3 of the printed proof, which is not formalized here (it needs the mean-zero-boundary fractional Sobolev embedding e.fractional.Sobolev.embedding.zero.bndr applied to h itself). The boundary cubes of Theorem C consume the estimate with the h-term switched on but never need it in the ‖∇h‖-only normal form, so the boundary-data defect is carried as data — it vanishes identically on interior cubes. The Step-7c display therefore carries the ∇h leg as an opaque scalar (dataH, guarded by the indicator 1_{z ∉ □_{m-1}}), and this module makes no claim about it.

(R2) the truncated window is not a cube. Every proved form of the lemma lives on a triadic cube (caccioppoliCoreSet Q x ⊆ openCubeSet Q), while §4.4's window is the truncation U_j = (z + □_j) ∩ □_m.

References

• ABK26, l.coarse.grained.Caccioppoli.RHS.
• ABK26, t.regularity Step 7c; Step 1.
• CoarseGraining, Homogenization/Book/Ch03/Theorems/CoarseCaccioppoliRHS.lean (coarseCaccioppoliRHSTheory).

1. The exponent pin

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccS : ℝ

The Caccioppoli's first exponent at the §4.4 pin. It is §4.4's own s = 1/4 (e.parameter.choices.regularity).

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccS = Algsuperdiff.Section4.Provider.Regularity.stepOneS

noncomputable def Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccT : ℝ

The Caccioppoli's second exponent at the §4.4 pin. Determined by the forcing slot: l.coarse.grained.Caccioppoli.RHS measures 𝐠 in H^{2t}, and §4.4 measures it in H^{1/4}, so 2t = 1/4.

Equations

• Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccT = Algsuperdiff.Section4.Provider.Regularity.stepOneS / 2

@[simp]

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccS_eq : stepSevenCaccS = 1 / 4

@[simp]

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccT_eq : stepSevenCaccT = 1 / 8

theorem Algsuperdiff.Section4.Provider.Regularity.two_mul_stepSevenCaccT : 2 * stepSevenCaccT = stepOneS

The pin, in the form that states WHY it is forced: twice the Caccioppoli's second exponent is §4.4's own exponent, so the forcing slot H^{2t} IS the H^{1/4} slot of Steps 4--7.

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccS_pos : 0 < stepSevenCaccS

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccS_lt_one : stepSevenCaccS < 1

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccT_pos : 0 < stepSevenCaccT

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccT_lt_half : stepSevenCaccT < 1 / 2

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccS_add_T_lt_one : stepSevenCaccS + stepSevenCaccT < 1

2. The prefactor and the forcing factor at the pin

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccPrefactor_le {d : ℕ} [NeZero d] {Q : HCPolySupport.TriadicCube d} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {C Theta0 : ℝ} (hC : 0 < C) (hTheta : HCPolySupport.Book.Ch02.ThetaRatio Q stepSevenCaccS stepSevenCaccT a ≤ Theta0) : HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor C Q a stepSevenCaccS stepSevenCaccT ≤ (2 * max 1 C) ^ 4 * 4 * Theta0 ^ 2

3. The coarse-grained Caccioppoli, at the §4.4 pin

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenCaccioppoliEnergy (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ {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 : ℝ), HCPolySupport.Book.Ch03.IsForcedEquation Q a u g → HCPolySupport.Book.Ch03.openCubeAtScale x (Q.scale - 1) ⊆ HCPolySupport.openCubeSet Q → HCPolySupport.Book.Ch03.ForceBesovRegularity Q stepOneS g → HCPolySupport.Book.Ch03.localizedCoeffEnergyValue (HCPolySupport.Book.Ch03.caccioppoliCoreSet Q x) (a.coeffOn Q) u ≤ HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor C Q a stepSevenCaccS stepSevenCaccT * ((HCPolySupport.Book.Ch02.lambdaS Q stepSevenCaccT a * Real.rpow 3 (-2 * ↑Q.scale) * HCPolySupport.Book.Ch03.normalizedL2SqOnSet (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => u.toFun y - c) + stepSevenCaccT.rpow (-8) / (1 - 2 * stepSevenCaccT) * (HCPolySupport.Book.Ch02.lambdaS Q stepSevenCaccT a).rpow (-1) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q stepOneS g ^ 2)

l.coarse.grained.Caccioppoli.RHS, instantiated at the §4.4 exponent pin.

For every triadic cube Q, every coefficient family a, every forced H¹(Q) solution u whose Dirichlet patch x + □_{Q.scale-1} sits inside Q, and every real c,

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

with the forcing seminorm displayed at §4.4's own exponent stepOneS = 1/4 (this is the pin 2t = s_{§4.4}, two_mul_stepSevenCaccT).

Unconditional in d; the surviving hypotheses are exactly the pinned lemma's own equation, patch and forcing-regularity binders. The ∇h leg of the printed display is absent — see residue (R1) of the module docstring.