GammaTenCloserGauge

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

The Step-2 cell bound at the closure's own corrector families

ABK26, Step 2 of l.approximate.recurrence.formula, target e.lower.bound.localization.terms.

The gap this module fills

Closure.GammaTenAssemblyCell.meshFluctuationCellIntegrand_le_ancestor_fold_shape bounds the Step-2 cell integrand by c1 H + c2 H at a free Besov exponent s, a free gauge sigma_0, and with the load leg read as blockVecNormSum (blockGaugeUp sigma_0 P_z). The two proved moment producers read their legs at fixed data:

• LocalizationFluctuationSplitFoldArithmetic.exists_regime_gaugedEllipticitySum_pow_four_le gauges the ellipticity sum by shom_{n+h-1};
• Closure.GammaTenLoad.exists_gammaTenLoadConst_root reads the load as sqrt (annealedSqrtNormSq shom_n (meshCellLoad ...)).

What is proved

• gammaTenBesovExponent, gammaTenCellFactor, gammaTenDualityConst, gammaTenGaugeConst, gammaTenCrossConst, gammaTenQuadConst --- the absolute constants of the fold at the fixed exponent, with their signs. The duality constant is cube-independent by Closure.GammaTenAssemblyCell.besovDualityConst_eq, so c1 and c2 depend only on the dimension.
• blockVecNormSum_blockGaugeUp_le_gaugeRatio --- the load-leg identification:

    | bfA_0^{1/2} P |_1 + | bfA_0^{1/2} P |_2
      <=  sqrt ( 2 gaugeRatio(shom_low, shom_top) ) * sqrt ( annealedSqrtNormSq shom_low P ) .
  

  Both sides are gauge readings of the same load; the two constants are the sqrt 2 of (a + b)^2 <= 2 (a^2 + b^2) and the gauge ratio of PrincipalResponseMomentsFourth.gaugeRatio.
• blockVecNormSum_blockGaugeUp_le_gammaTenGaugeConst --- the same at the closure's own pair of scales, where PrincipalResponseComposeDisplayTwo.gaugeRatio_sigmaBar_le_readingConst caps the ratio by the absolute 4 . 3^9.
• meshFluctuationCellIntegrand_le_closureFold --- the Step-2 cell bound at the closure's own corrector families, in the exact c1 H + c2 H shape the grid fold consumes, with F the gauged ellipticity sum at the cell's scale-(n+h) ancestor, G the load in the producer's own spelling and H the pathwise Besov envelope.

Binders

The large-cube gate, the depth/scale identity of the closure mesh, the two e.recurrence.params facts hcover, hshell, the gauge-ratio cap hgauge, the cell membership and the envelope. No measurability, no moment and no smallness proposition occurs.

Scope

There is no sorry, no admit, no custom axiom and no set_option maxHeartbeats.

References

• ABK26, l.approximate.recurrence.formula Step 2, e.Pz.def, e.Fz.def, the load display.

The absolute constants of the fold at the fixed exponent

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenBesovExponent : ℝ

The Besov exponent the closure fixes, s = 1/2. The ancestor route of Closure.GammaTenAssemblyCell.meshFluctuationCellIntegrand_le_ancestor_fold_shape forces cgamma < s, the annealed depth fold of LocalizationFluctuationAnnealedFold asks for s <= 1/2, and the per-cube bound asks for 0 < s < 1; 1/2 is the unique value meeting all three uniformly in the model.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenBesovExponent = 1 / 2

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenCellFactor : ℝ

The absolute Poincare/ancestor factor 32 c_{s,2}^{-2} 3^{22} of the cell bound at the fixed exponent.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenCellFactor_nonneg : 0 ≤ gammaTenCellFactor

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenDualityConst (d : ℕ) : ℝ

The cube-independent duality constant 2 d 3^{d+s} at the fixed exponent (Closure.GammaTenAssemblyCell.besovDualityConst_eq).

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenDualityConst_nonneg (d : ℕ) : 0 ≤ gammaTenDualityConst d

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenGaugeConst : ℝ

The gauge-transport factor between the load's own gauge shom_n and the ellipticity leg's gauge shom_{n+h-1}: the sqrt 2 of (a + b)^2 <= 2 (a^2 + b^2) times the absolute cap 4 . 3^9 of PrincipalResponseComposeDisplayTwo.gaugeRatio_sigmaBar_le_readingConst.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenGaugeConst = √(2 * (4 * 3 ^ 9))

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenGaugeConst_nonneg : 0 ≤ gammaTenGaugeConst

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenCrossConst (d : ℕ) : ℝ

c1, the coefficient of the cross term F G H of the Step-2 fold.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenQuadConst (d : ℕ) : ℝ

c2, the coefficient of the quadratic term F H H of the Step-2 fold.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenCrossConst_nonneg (d : ℕ) : 0 ≤ gammaTenCrossConst d

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.gammaTenQuadConst_nonneg (d : ℕ) : 0 ≤ gammaTenQuadConst d

The load-leg identification

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.vecNorm_smul_of_nonneg {d : ℕ} {c : ℝ} (hc : 0 ≤ c) (v : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.vecNorm (c • v) = c * HCPolySupport.Book.Ch02.vecNorm v

The Euclidean vector norm of a nonnegative scalar multiple.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.blockVecNormSum_blockGaugeUp_le_gaugeRatio {d : ℕ} (sigmaLow sigmaTop : Observable.PositiveScalar) (P : HCPolySupport.BlockVec d) : CoarseEllipticity.blockVecNormSum (CoarseEllipticity.blockGaugeUp (↑sigmaTop) P) ≤ √(2 * gaugeRatio sigmaLow sigmaTop) * √(annealedSqrtNormSq sigmaLow P)

The two gauge readings of one load.

  | bfA_0^{1/2} P |_1 + | bfA_0^{1/2} P |_2
    <=  sqrt ( 2 rho ) * sqrt ( shom |P_1|^2 + shom^{-1} |P_2|^2 ) ,

with rho = gaugeRatio shom_low shom_top and bfA_0 the gauge at shom_top. The 2 is (a + b)^2 <= 2 (a^2 + b^2), the rho is the change of gauge. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.blockVecNormSum_blockGaugeUp_le_gammaTenGaugeConst {d : ℕ} (M : ABKModel d) (n : ℤ) (h : ℕ) (hgauge : gaugeRatio (Annealed.sigmaBar M n) (Annealed.sigmaBar M (n + ↑h - 1)) ≤ 4 * 3 ^ 9) (P : HCPolySupport.BlockVec d) : CoarseEllipticity.blockVecNormSum (CoarseEllipticity.blockGaugeUp (↑(Annealed.sigmaBar M (n + ↑h - 1))) P) ≤ gammaTenGaugeConst * √(annealedSqrtNormSq (Annealed.sigmaBar M n) P)

The load-leg identification at the closure's two gauges.

The cell bound at the closure's own families

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.meshFluctuationCellIntegrand_le_closureFold {d : ℕ} [NeZero d] (M : ABKModel d) (n : ℤ) (h K : ℕ) (hK10 : 10 ^ 10 * M.gamma⁻¹ ≤ ↑↑K - ↑(n + ↑h)) (hscale : (HCPolySupport.originCube d ↑K).scale - ↑(closureMeshDepth M n h K) = recurrenceMesoScale recurrenceGapMultiplier M.gamma (n + ↑h) ↑h) (hcover : (↑recurrenceGapMultiplier + 1) ^ 2 ≤ M.gamma⁻¹) (hshell : ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹) (hgauge : gaugeRatio (Annealed.sigmaBar M n) (Annealed.sigmaBar M (n + ↑h - 1)) ≤ 4 * 3 ^ 9) (e e' : HCPolySupport.Vec d) (omega : Cutoff.CutoffSample d) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d ↑K) (closureMeshDepth M n h K)) {Bg : ℝ} (hBg : 0 ≤ Bg) (hpos1 : ∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R gammaTenBesovExponent N fun (x : HCPolySupport.Vec d) => (CoarseEllipticity.blockGaugeUp (↑(Annealed.sigmaBar M (n + ↑h - 1))) ((localizationFz (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' R (closureDirichletAlong M n h K e ↑omega) (closureNeumannAlong M n h K e' ↑omega)).eval x)).1) ≤ Bg) (hpos2 : ∀ (N : ℕ), (HCPolySupport.cubeBesovPositiveVectorPartialSeminormTwo R gammaTenBesovExponent N fun (x : HCPolySupport.Vec d) => (CoarseEllipticity.blockGaugeUp (↑(Annealed.sigmaBar M (n + ↑h - 1))) ((localizationFz (Annealed.sigmaBar M n) (↑omega) n (n + ↑h) e' R (closureDirichletAlong M n h K e ↑omega) (closureNeumannAlong M n h K e' ↑omega)).eval x)).2) ≤ Bg) : meshFluctuationCellIntegrand M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega ≤ gammaTenCrossConst d * (gaugedEllipticitySum (↑(Annealed.sigmaBar M (n + ↑h - 1))) (ancestorAtScale R (n + ↑h)) M.gamma (Cutoff.coefficientCutoffTriadicCoeffFamily M (n + ↑h) omega) * √(annealedSqrtNormSq (Annealed.sigmaBar M n) (meshCellLoad M n h (↑K) e e' (closureDirichletAlong M n h K e) (closureNeumannAlong M n h K e') R omega)) * Bg) + gammaTenQuadConst d * (gaugedEllipticitySum (↑(Annealed.sigmaBar M (n + ↑h - 1))) (ancestorAtScale R (n + ↑h)) M.gamma (Cutoff.coefficientCutoffTriadicCoeffFamily M (n + ↑h) omega) * Bg * Bg)