StepSevenLambdaChain

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

t.regularity Step 7b: the Step-7 chain with hlambda discharged

What this file does

StepSevenMean.exists_stepSevenEnd_chain_of_lambda_hmeanFree is the Step-7 end chain with hmean and hoscTrunc discharged inside; its remaining conditional inputs are exactly two — hlambda and the Step-7c gradient display hgrad.

exists_stepSevenEnd_chain_of_caps below replaces hlambda by the clause-(B) record StepSevenLambdaCaps on the parent cube □_{k+1}, at Clam := (32/7)·CB and shomMp := σ^{-1} — the row-1 entry of the derived-slot table (StepSevenLambdaSlots.stepSevenCgLamInv_le_of_caps). The chain's conditional set is thereby narrowed to

   clause (B)  +  the Step-7c hgrad

and clause (B) is itself produced unconditionally, a.e. on the §4.4 good event, by StepSevenLambdaGoodEvent.ae_stepSevenLambdaCaps.

Every other binder of the parent chain is carried verbatim; only Clam and shomMp are substituted, and the two positivity binders that referred to them (0 ≤ Clam, 0 ≤ shomMp) are replaced by 0 ≤ CB and 0 < sigma, from which they are derived here.

References

• ABK26, t.regularity Step 7.

1. Row 1 at the chain's own indexing

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCgLamInv_le_of_caps_succ {d : ℕ} [NeZero d] {k : ℤ} (a : HCPolySupport.Book.Ch03.CoeffFamily d) {sigma CB : ℝ} (hcaps : StepSevenLambdaCaps (HCPolySupport.originCube d (k + 1)) a sigma CB) : stepSevenCgLamInv (HCPolySupport.originCube d k) a stepSevenCgS ≤ 32 / 7 * CB * sigma⁻¹

Row 1 of the derived-slot table at the chain's indexing. Clause (B) on the parent cube □_{k+1} caps the chain's hlambda slot on □_k:

  λ_{1/8,2}^{-1}(□_k; a) ≤ (32/7)·CB · σ^{-1} .

2. The Step-7 chain with hlambda discharged

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenEnd_chain_of_caps (d : ℕ) [NeZero d] : ∃ (C : ℝ), 0 < C ∧ ∀ {alpha : ℝ} {n m k : ℤ} {a : HCPolySupport.Book.Ch03.CoeffFamily d} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} {z c : HCPolySupport.Vec d} {w : HCPolySupport.Vec d → ℝ} (u : HCPolySupport.Book.Ch03.ForcedCubeSolution (HCPolySupport.originCube d k) a g) {Cg Ccmp Kg Kd Ks Ctr CB sigma shomNp shomM gradLoc gradM dataG dataM W G H : ℝ}, (∀ (y : HCPolySupport.Vec d), u.toH1.toFun y = w (y + c)) → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → k ≤ m → ExcessDecay.truncatedWindow z m k ⊆ (fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k) → MeasureTheory.IntegrableOn w (ExcessDecay.truncatedWindow z m k) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => w x ^ 2) (ExcessDecay.truncatedWindow z m k) MeasureTheory.volume → MeasureTheory.IntegrableOn w ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => w x ^ 2) ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume → MeasureTheory.IntegrableOn (fun (x : HCPolySupport.Vec d) => (w x - HCPolySupport.volumeAverage ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) w) ^ 2) ((fun (y : HCPolySupport.Vec d) => c + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k)) MeasureTheory.volume → 0 ≤ Cg → 0 ≤ CB → 0 ≤ Ks → 0 ≤ Ccmp → 0 < sigma → 0 < shomM → 0 ≤ gradM → 0 ≤ dataG → 0 ≤ W → 0 ≤ G → 0 ≤ H → HCPolySupport.Book.Ch03.ForceBesovRegularity (HCPolySupport.originCube d k) stepSevenCgS g → StepSevenLambdaCaps (HCPolySupport.originCube d (k + 1)) a sigma CB → HCPolySupport.Book.Ch03.forcedSolutionEnergyNorm (HCPolySupport.originCube d k) a u ≤ Kg * gradM → HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d k) stepSevenCgS g ≤ Kd * dataG → sigma⁻¹ ≤ Ks * shomM⁻¹ → √Ks * Kg ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → Ks * Kd ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → shomNp ≤ Ccmp * shomM → gradLoc ≤ Cg * √shomNp * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * ((HCPolySupport.cubeScaleFactor (HCPolySupport.originCube d k))⁻¹ * Support.normalizedL2On (ExcessDecay.truncatedWindow z m k) fun (x : HCPolySupport.Vec d) => w x - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m k) w) + Cg * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√shomNp * (W * (shomM⁻¹ * G + H)) + dataM) → gradLoc ≤ Cg * √Ccmp * (√(3 ^ d) * stepSevenEmbeddingConst d * stepSevenBridgeConst stepSevenCgS * (C * 64 * (√(32 / 7 * CB) + 32 / 7 * CB)) * Ctr) * Real.rpow 3 (stepSixExponent alpha n m) * (gradM + √shomM⁻¹ * dataG) + Cg * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√Ccmp * (W * ((√shomM)⁻¹ * G + √shomM * H)) + dataM)

The Step-7 end chain, conditional only on clause (B)'s hgrad.

This is StepSevenMean.exists_stepSevenEnd_chain_of_lambda_hmeanFree verbatim, with the hlambda hypothesis stepSevenCgLamInv (□_k) a stepSevenCgS ≤ Clam * shomMp replaced by the clause-(B) record on the parent cube and the two constants substituted: Clam := (32/7)·CB, shomMp := σ^{-1}.