HomSeamFluxLevelChain #

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

The level pairing with the `Ccg` slot FREED, and its `ã` instance #

Why the `Ccg` slot has to be freed #

HomSeamSqrtTwoChain's pairing chain is stated at the pinned coarse-graining constant of the a_L lane, which is the Classical.choose of that lane's existential. The print-accurate lane produces its own constant HomSeamFluxLane.cgDualBoundConstFlux d p, and Classical.choose does not reduce, so the two names are different reals even though they arise from the SAME source constant C(p,d) of HomCGDischargeInstantiation.exists_printedCoarseGraining_of_dirichletPair.

Section 1 therefore restates the pairing constants and the two pairing theorems with Ccg a bare nonnegative real. Nothing in the mathematics changes: the proofs use the pinned constant only through its nonnegativity. At the a_L lane's pinned constant these are exactly HomSeamSqrtTwoChain's level leg and budget split.

Section 2 instantiates at Ccg:= recutPinnedCcgFlux d p and at the print-accurate error slots recutPinnedE1Flux/recutPinnedE2Flux, producing the two level conditions of the re-cut bundle at

  the coefficient  ã_{L,m},   the EthmB base  s' = s/8,   C_w = 2·pairCwOf.

Scope #

Nothing here is a source-facing claim. The two level conditions are conditional APIs whose remaining hypotheses are exactly hSbound (the Theorem-C Step-2 datum), the two ã dominations of HomSeamFluxCoefficient, and the a.e. finiteness of the [0,∞] carrier.

1. The pairing constants and the two legs at a FREE `Ccg` #

source

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.pairCwLegOf (d : ℕ) (Ccg : ℝ) (p : HCPolySupport.FiniteLpExponent) (s2 : ↑HCPolySupport.FractionalOrder) (Cgap Cen0 sbase kappa theta : ℝ) :

ℝ

The a_L lane's pairing-leg constant with the coarse-graining constant freed. At that lane's pinned constant this is that definition.

Equations

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

Instances For

source

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.pairCwOf (d : ℕ) (Ccg : ℝ) (p : HCPolySupport.FiniteLpExponent) (s2 : ↑HCPolySupport.FractionalOrder) (Cgap Cen0 sbase Ktest : ℝ) :

ℝ

The a_L lane's pairing constant with the coarse-graining constant freed.

Equations

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

Instances For

source

theorem Algsuperdiff.Section4.Provider.Homogenization.pairCwLegOf_nonneg (d : ℕ) {Ccg : ℝ} (p : HCPolySupport.FiniteLpExponent) (s2 : ↑HCPolySupport.FractionalOrder) {Cgap Cen0 sbase kappa theta : ℝ} (hCcg0 : 0 ≤ Ccg) (hCgap : 0 < Cgap) (hCen0 : 0 ≤ Cen0) (hsbase : 0 < sbase) (hkappa : 0 ≤ kappa) (htheta : 0 < theta) (hwin : theta * sbase < ↑s2) (hCdata0 : 0 ≤ cgOverlapDataConst d s2 p) (hs2gap : 5 < 10 * ↑s2 * Real.log 3) :

0 ≤ pairCwLegOf d Ccg p s2 Cgap Cen0 sbase kappa theta

source

theorem Algsuperdiff.Section4.Provider.Homogenization.seamLegOf_ofReal_le {d : ℕ} (M : Section3.ABKModel d) {Cgap : ℝ} (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) (p : HCPolySupport.FiniteLpExponent) (s2 : ↑HCPolySupport.FractionalOrder) {Ccg sbase kappa theta Cen0 E1 E2 : ℝ} (hCcg0 : 0 ≤ Ccg) (hs : 0 < homS M) (hsbase : sbase = homS M) (hlog : 4 ≤ |Real.log M.gamma|) (hgamma1 : M.gamma < 1) (hCgap : 0 < Cgap) (hkappa : 0 ≤ kappa) (htheta : 0 < theta) (hCen0 : 0 ≤ Cen0) (hE1 : 0 ≤ E1) (hE2 : 0 ≤ E2) (hCdata0 : 0 ≤ cgOverlapDataConst d s2 p) (hwin : theta * sbase < ↑s2) (hs2gap : 5 < 10 * ↑s2 * Real.log 3) (hdom1 : ENNReal.ofReal E1 ≤ Support.fluxCorrectedTwoScaleErrorObservableSup M m (homN M m) (homHalf (homSeamBase M hs)) omega) (hdom2 : ENNReal.ofReal E2 ≤ ENNReal.ofReal √2 * Support.fluxCorrectedTwoScaleErrorObservableSup M m (homN M m) (homQuarterOf (homSeamBase M hs)) omega) :

ENNReal.ofReal (kappa * (Ccg * (theta * sbase)⁻¹ * E1 * (Cen0 * recutEnergyFactor M Y m omega)) + kappa * (Ccg * (theta * sbase) ^ (-(9 / 2)) * (↑s2 - theta * sbase)⁻¹ * (1 + E2 ^ 2) * cgOverlapDataConst d s2 p * 3 ^ (↑s2 * ↑(homN M m) - ↑s2 * ↑m))) ≤ ENNReal.ofReal (2 * pairCwLegOf d Ccg p s2 Cgap Cen0 sbase kappa theta) * ethmB M Cgap Y m (homN M m) (homSeamBase M hs) omega

THE PAIRING OF ONE LEVEL CONDITION, AT A FREE Ccg AND THE RE-PINNED BASE.

HomSeamSqrtTwoChain's level leg with the coarse-graining constant freed; the proof is unchanged; it uses the pinned constant only through its nonnegativity.

source