StepSevenCaccFinalCore

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

1. The square-root conversion on abstract reals

theorem Algsuperdiff.Section4.Provider.Regularity.sqrt_le_of_le_mul_add {E P A B : ℝ} (hP : 0 ≤ P) (hA : 0 ≤ A) (hB : 0 ≤ B) (h : E ≤ P * (A + B)) : √E ≤ √P * √A + √P * √B

The form conversion. A squared two-term bound becomes an energy-norm two-term bound with the SAME single constant √P:

  E ≤ P·(A + B)   ⟹   √E ≤ √P·√A + √P·√B .

This is the whole's residue at the level of reals; everything else in the residue is carrier identification.

2. The three exact square roots

theorem Algsuperdiff.Section4.Provider.Regularity.sqrt_normalizedL2SqOnSet {d : ℕ} (V : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → ℝ) : √(HCPolySupport.Book.Ch03.normalizedL2SqOnSet V f) = Support.normalizedL2On V f

The L² square root is definitional. √(⨍_V f²) = ‖f‖_{L²(V)}: CoarseGraining's normalizedL2SqOnSet and §4.3's normalizedL2On are the same object under one square root, with no constant and no hypothesis.

theorem Algsuperdiff.Section4.Provider.Regularity.sqrt_rpow_three_neg_two_mul (j : ℤ) : √(Real.rpow 3 (-2 * ↑j)) = 3 ^ (-j)

The scale weight's square root. √(3^{-2j}) = 3^{-j}, in the two spellings the two sides use: the Caccioppoli carries the Real.rpow form, the §4.4 windows the zpow form.

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccLambda_pos {d : ℕ} [NeZero d] (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch03.CoeffFamily d) {t : ℝ} (ht : 0 < t) : 0 < HCPolySupport.Book.Ch02.lambdaS Q t a

The Caccioppoli's own ellipticity coefficient is positive. λ_{t,1} at a positive index is positive, so its square root and its inverse are honest objects.

3. The forcing factor at the pin

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

The Caccioppoli's forcing factor at the §4.4 pin, t^{-8}(1-2t)^{-1} at t = 1/8.

Equations

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

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccForcingFactor_nonneg : 0 ≤ stepSevenCaccForcingFactor

4. l.coarse.grained.Caccioppoli.RHS in the hcacc slot shape

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenCaccioppoliEnergyNorm (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) * (3 ^ (-Q.scale) * Support.normalizedL2On (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => u.toFun y - c)) + √(HCPolySupport.Book.Ch03.caccioppoliWithRHSPrefactor C Q a stepSevenCaccS stepSevenCaccT) * (√(stepSevenCaccForcingFactor * (HCPolySupport.Book.Ch02.lambdaS Q stepSevenCaccT a)⁻¹) * HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo Q stepOneS g)

** residue, first half: the Caccioppoli in hcacc shape.**

StepSevenCaccMatching.exists_stepSevenCaccioppoliEnergy converted to the energy-norm (square-root) two-term form that StepSevenCaccGradient.stepSevenGradientWithShom consumes:

  √(⨍_{core} ∇u·𝐚∇u)
    ≤ √P · ( √λ_{1/8,1} · ( 3^{-scale} ‖u-c‖_{L²(□_Q)} ) )
      + √P · ( √(F·λ_{1/8,1}^{-1}) · [𝐠]_{B^{1/4}(□_Q)} ) ,

with P = caccioppoliWith 𝐚 (1/4) (1/8) and F = stepSevenCaccForcingFactor. The binder list is exists_stepSevenCaccioppoliEnergy's V; the ∇h leg is still absent (residue), which is exactly why the display's indicator 1_{z ∉ □_{m-1}} marks the boundary of this module's regime.