RootClauseBClosePayload

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

1. The re-cut payload

structure Algsuperdiff.Section4.Provider.Regularity.RootClauseBTopPayload {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L : ℤ) (Khol Kd CB CBc Cdel Cosc CdM alpha : ℝ) (n m kc n' : ℤ) (x : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) (uglob : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d) : Prop

The Step-7 payload of the clause-(B) display at a free coarse scale, at the lattice centre z = offGridCentre n x the root's display is stated at.

• caps : StepSevenLambdaCaps (HCPolySupport.originCube d (kc + 1)) (Support.fluxCorrectedCoeffFamily M L (kc + 1) (HCPolySupport.originCube d (kc + 1)) (Section3.Cutoff.translateCutoffSample (offGridCentre n x) omega)) (↑(Section3.Annealed.sigmaBar M (kc + 1))) CB

  The A6 clause-(B) record on the re-cut coarse cube □_{k_c+1}.

• capsCacc : StepSevenLambdaCaps (HCPolySupport.originCube d (n' + 1)) (Support.fluxCorrectedCoeffFamily M L (n' + 1) (HCPolySupport.originCube d (n' + 1)) (Section3.Cutoff.translateCutoffSample (offGridCentre n x) omega)) (↑(Section3.Annealed.sigmaBar M (n' + 1))) CBc

  The A6 clause-(B) record on the Caccioppoli's cube □_{n'+1}.

• dataB : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d kc) stepSevenCgS fun (y : HCPolySupport.Vec d) => -gsrc (y + offGridCentre n x)) ≤ Kd * edFinalDataOscG Khol m

  The Step-7d data transport at the re-cut coarse cube.

• dataM : (stepSevenCaccDataM (HCPolySupport.originCube d n') (Support.fluxCorrectedCoeffFamily M L (n' + 1) (HCPolySupport.originCube d (n' + 1)) (Section3.Cutoff.translateCutoffSample (offGridCentre n x) omega)) fun (y : HCPolySupport.Vec d) => -gsrc (y + offGridCentre n x)) ≤ CdM * (√(↑(Section3.Annealed.sigmaBar M m))⁻¹ * edFinalDataOscG Khol m)

  The Caccioppoli's data leg against the printed K_g-leg.

• osc : (3 ^ (-n') * Support.normalizedL2On (ExcessDecay.truncatedWindow (offGridCentre n x) m n') fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow (offGridCentre n x) m n') uglob.toFun) ≤ Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * (3 ^ (-kc) * Support.normalizedL2On (ExcessDecay.truncatedWindow (offGridCentre n x) m kc) fun (y : HCPolySupport.Vec d) => uglob.toFun y - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow (offGridCentre n x) m kc) uglob.toFun) + Cosc * Real.rpow 3 (1 / 2 * stepSixExponent alpha n m) * (edFinalDataG M Cdel (Khol * stepFourGagliardoConst d stepOneS) m + 0)

  e.oscillation.Holder.bound at (n', k_c).

2. The endpoint: clause (B) of RootLatticeDisplay

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseB_display_offGrid_freeUniform (d : ℕ) [NeZero d] : ∃ (Cch : ℝ) (Cc : ℝ), 0 < Cch ∧ 0 < Cc ∧ ∀ (M : Section3.ABKModel d) (m0 : ℤ) (Ecap : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M m0 Ecap → M.gamma < 1 / 2 → ∀ (L : ℤ) {alpha : ℝ} {n m kc n' : ℤ} {x : HCPolySupport.Vec d} (omega : Section3.Cutoff.CutoffSample d) (uglob hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) {gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} {Khol Kd CB CBc Cdel Cosc CdM C1 delta Cest : ℝ} {B : ℕ}, m ≤ m0 → n' ≤ m - 1 → n + 1 ≤ n' - 2 → n ≤ m → n' ≤ kc → kc ≤ m - 1 → m - (kc + 1) ≤ ↑B + 1 → Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) uglob hdat gsrc → MeasureTheory.MemLp gsrc 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 gsrc) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → 0 ≤ Khol → 0 ≤ Kd → 0 ≤ CB → 0 ≤ CBc → 0 ≤ Cdel → 0 ≤ Cosc → 0 ≤ CdM → 2 * ↑d + 2 ≤ C1 → 0 ≤ alpha → alpha ≤ 1 → delta ≤ C1⁻¹ * (1 - alpha) → n' - n ≤ ↑B + 6 → ↑B ≤ delta * (↑(m - n).toNat + 1) → RootClauseBTopPayload M L Khol Kd CB CBc Cdel Cosc CdM alpha n m kc n' x omega uglob gsrc → rootClauseBPrefactor d Cch (rootClauseBCaccUniform Cc CBc) Cosc CBc CB (rootClauseBTopCtr d Kd) (edFinalDataOscW M Cdel * stepFourGagliardoConst d stepOneS) CdM ≤ Cest → offGridCentre n x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1)) → (√M.nu * Support.normalizedL2On (ExcessDecay.truncatedWindow (offGridCentre n x) m (n + 1)) fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (uglob.grad y))) ≤ Cest * Real.rpow 3 ((1 - alpha) * (↑m - ↑n)) * ((√M.nu * Support.normalizedL2On (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) fun (y : HCPolySupport.Vec d) => √(HCPolySupport.vecNormSq (uglob.grad y))) + √(↑(Section3.Annealed.sigmaBar M m))⁻¹ * Real.rpow 3 (↑m / 2) * Khol)

Clause (B) of RootAssemblyConditional.RootLatticeDisplay, at the re-cut coarse scale.

The S conjunct of the root's lattice-centre display — the interior-guarded, boundary-leg-free half — produced for every datum satisfying RootClauseBTopPayload, with the funding line stated at the ω- Caccioppoli constant unit 1.

3. The three produced fields

theorem Algsuperdiff.Section4.Provider.Regularity.rootClauseB_dataB_free {d : ℕ} [NeZero d] {m kc : ℤ} {z : HCPolySupport.Vec d} {gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} {Khol : ℝ} (hz : z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d (m - 1))) (hkc : kc ≤ m - 1) (hKhol : 0 ≤ Khol) (hgHol : Support.HolderSeminormBoundOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (1 / 2) Khol gsrc) (hgL2 : MeasureTheory.MemLp gsrc 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) (hgW : MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 gsrc) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)))) : (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d kc) stepSevenCgS fun (y : HCPolySupport.Vec d) => -gsrc (y + z)) ≤ rootClauseBDataBConst d * edFinalDataOscG Khol m

dataB at the re-cut coarse cube, produced.

RootPayloadDataB.besovTranslated_neg_le_holder at j = k_c followed by 3^{k_c/2} ≤ 3^{m/2} — the same single inequality used at j = m-1.