SuperposedFluxLowerTwoLe

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

The sharp lower branch for finite exponents at least two

This file feeds the pointwise sharp representative into the finite-q pre-split theorem. Scale summability, amplitude absorption, and parameter gates are local proof steps. The output-constant inequalities on the main theorem remain caller-supplied conditional A obligations; this Provider module asserts no source-node status.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxTwoLeBudgetConst (d : ℕ) : ℝ

Fixed multiplicative budget prefactor for the 2 ≤ q < ∞ random lane.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxTwoLeBudgetConst_pos {d : ℕ} (hd : 2 ≤ d) : 0 < superposedFluxTwoLeBudgetConst d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.exists_superposedFluxFiniteQPresplit_two_le {d : ℕ} [NeZero d] (hd : 2 ≤ d) {Clow : ℝ} (hClow : 0 < Clow) (haux : profileAuxiliaryConst d ≤ Clow) (hbudgetChoice : superposedFluxTwoLeBudgetConst d + 6 ≤ superposedFluxBfaRate d * Clow) (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }) (hstate : Frozen.Section3.inductionState M (m - 1) E) (sigma : ℝ) (hsigma : sigma ∈ Set.Ioc 0 (1 / 2)) (hE1 : max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E) (hE2 : ↑E ≤ M.gamma ^ (-(1 / 5))) (r : { r : ℝ // 1 ≤ r }) (hr : 2 ≤ ↑r) (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1) : ∃ (U : ℕ → Cutoff.CutoffSample d → ℝ) (a : ℕ → ℝ), (∀ (n : ℕ) (omega : Cutoff.CutoffSample d), 0 ≤ U n omega) ∧ (∀ (n : ℕ), Measurable (U n)) ∧ (∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * U n omega ^ (↑r / 2)) ∧ (∀ (omega : Cutoff.CutoffSample d), Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n ^ (2 / ↑r) * U n omega) ∧ (∀ (n : ℕ), 0 < a n) ∧ (Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n ^ (2 / ↑r) * a n) ∧ (∀ (n : ℕ), HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (U n) (a n)) ∧ 2 * HCPolySupport.IndependentSums.gammaTriangleConst ((1 - sigma) / 2) * ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s (↑r) n ^ (2 / ↑r) * a n ≤ Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)) ∧ ∀ (omega : Cutoff.CutoffSample d) (L : ℤ), m - 1 ≤ L → ∀ (n : ℕ), ↑(Annealed.sigmaBar M (m - 1)) * HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - ↑n) (Cutoff.coefficientCutoff M.nu L omega) ≤ finiteQGeometricProfile (2 * superposedFluxSharpDetConst d) M.gamma n + U n omega

The model-facing finite-q producer consumed by coarse_ellipticity_lower_branchPayload_two_le_of_finiteQPresplit.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFlux_lower_branchPayload_two_le {d : ℕ} [NeZero d] (hd : 2 ≤ d) {Clow : ℝ} (hClow : 0 < Clow) (haux : profileAuxiliaryConst d ≤ Clow) (hdet : 8 * superposedFluxSharpDetConst d ≤ Clow) (hbudgetChoice : superposedFluxTwoLeBudgetConst d + 6 ≤ superposedFluxBfaRate d * Clow) (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }) : Frozen.Section3.inductionState M (m - 1) E → ∀ sigma ∈ Set.Ioc 0 (1 / 2), max (Real.exp (Clow / sigma)) (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → ∀ (r : { r : ℝ // 1 ≤ r }), 2 ≤ ↑r → ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1), ∃ (Ydet : Cutoff.CutoffSample d → ℝ) (Y : Cutoff.CutoffSample d → ℝ), (∀ (omega : Cutoff.CutoffSample d) (L : ℤ), m - 1 ≤ L → Observable.cutoffLowerEllipticityInv M m L s ⋯ (CoarseEllipticityExponent.finite r) omega * ↑(Annealed.sigmaBar M (m - 1)) ≤ Ydet omega + Y omega) ∧ (∀ (omega : Cutoff.CutoffSample d), Ydet omega ≤ Clow * s * (2 * s - M.gamma)⁻¹) ∧ Measurable Y ∧ HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) Y (Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)))

A payload-valued helper for the conditional 2 ≤ q < ∞ A.