SuperposedFluxLowerLtTwo #
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 below two #
This file normalizes the pointwise sharp representative by its deterministic
depth amplitude and supplies the conditional finite-q < 2 pre-split A. The
output-constant inequalities remain caller-supplied obligations; these Provider
helpers assert no source-node status.
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.exists_superposedFluxFiniteQPresplit_lt_two
{d : ℕ}
[NeZero d]
(hd : 2 ≤ d)
{Clow : ℝ}
(hClow : 0 < Clow)
(haux : profileAuxiliaryConst d ≤ Clow)
(hbudgetChoice : superposedFluxLtTwoBudgetConst d + 6 ≤ superposedFluxBfaRate d / 2 * 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 : ↑r < 2)
(s : ℝ)
(hsWindow : s ∈ Set.Icc (M.gamma / 2 + Real.exp (-(Clow⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))) 1)
:
∃ (V : ℕ → Cutoff.CutoffSample d → ℝ) (a : ℕ → ℝ),
(∀ (n : ℕ) (omega : Cutoff.CutoffSample d), 0 ≤ V n omega) ∧ (∀ (n : ℕ), Measurable (V n)) ∧ (∀ (n : ℕ), 0 < a n) ∧ (Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a n ^ (↑r / 2)) ∧ (∀ (omega : Cutoff.CutoffSample d),
Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a n ^ (↑r / 2) * V n omega) ∧ (∀ (n : ℕ),
HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M))
(HCPolySupport.IndependentSums.gammaSigma ((1 - sigma) / 2)) (V n) 1) ∧ 2 * (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s (↑r) n * a n ^ (↑r / 2)) ^ (2 / ↑r) * HCPolySupport.IndependentSums.gammaTriangleConst ((1 - sigma) / 2) ≤ 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 + a n * V n omega
The model-facing normalized finite-q < 2 producer consumed by
coarse_ellipticity_lower_branchPayload_lt_two_of_finiteQPresplit.
theorem
Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFlux_lower_branchPayload_lt_two
{d : ℕ}
[NeZero d]
(hd : 2 ≤ d)
{Clow : ℝ}
(hClow : 0 < Clow)
(haux : profileAuxiliaryConst d ≤ Clow)
(hdet : 16 * superposedFluxSharpDetConst d ≤ Clow)
(hbudgetChoice : superposedFluxLtTwoBudgetConst d + 6 ≤ superposedFluxBfaRate d / 2 * 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 }),
↑r < 2 →
∀ (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)) ^ (2 / ↑r)) ∧ 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 1 ≤ q < 2 A.