SuperposedFluxLowerSeries

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

Scale-series estimates for the sharp lower lane

This file sums the uniform depth amplitude against the rooted finite-exponent weight and against the endpoint weight. The only pole used below is the rounded order-five pole already recorded for the lower lane.

def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLowerPoleConst : ℝ

Numerical cost of transporting the order-four polynomial from the positive-gap grid weight to the endpoint weight and then to the frozen window.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLowerPoleConst = 6912

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxLowerPoleConst_pos : 0 < superposedFluxLowerPoleConst

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_poly_mul_endpointWeight (rho : ℝ) (hrho : 0 < rho) : Summable fun (n : ℕ) => (↑n + 1) ^ 4 * endpointWeight rho n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_poly_mul_endpointWeight_le_frozenPole {rho eps : ℝ} (hrho : 0 < rho) (hrhoTwo : rho ≤ 2) (heps : 0 < eps) (hepsOne : eps ≤ 1) (hwindow : 2 * eps ≤ rho) : ∑' (n : ℕ), (↑n + 1) ^ 4 * endpointWeight rho n ≤ superposedFluxLowerPoleConst * eps⁻¹ ^ 5

The rounded order-five endpoint series, priced at the frozen window.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.outputConst_le_invSq_mul_gammaInv_of_gate {d : ℕ} (M : ABKModel d) {C sigma E : ℝ} (hC : 0 ≤ C) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hE : 1 ≤ E) (hgate : Real.exp (C / sigma) ≤ E) (hgamma : M.gamma ≤ E ^ (-5)) : C ≤ E⁻¹ ^ 2 * M.gamma⁻¹

The source scale restriction upgrades the frozen inverse-square factor to at least the output constant, using the output theorem's own exponential admissibility gate.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.prefactor_mul_exp_le_frozenRare_pow {K c C X : ℝ} {p : ℕ} (hK : 0 ≤ K) (hC : 0 < C) (hX : C ≤ X) (hchoice : K + ↑p ≤ c * C) : K * Real.exp (-(c * X)) ≤ Real.exp (-(C⁻¹ * X)) ^ p

A fixed prefactor can be absorbed using the output constant itself as a lower bound for E⁻² gamma⁻¹. This is the large-parameter refinement of the elementary exponential gate used for the final lower budget.

Rooted finite-exponent and endpoint weights

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.geometricWeight_rpow_two_div_eq_endpointWeight {s q : ℝ} (hsq : 0 ≤ s * q) (hq : q ≠ 0) (n : ℕ) : HCPolySupport.Book.Ch02.geometricWeight s q n ^ (2 / q) = gridSumConst s q * endpointWeight (2 * s) n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gridSumConst_le_one {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : gridSumConst s q ≤ 1

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_rootedWeight_mul_depthAmp {d : ℕ} (M : ABKModel d) (E : ℝ) {s q : ℝ} (hs : 0 < s) (hq : 0 < q) (hgap : 0 < 2 * s - M.gamma) : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s q n ^ (2 / q) * superposedFluxDepthAmpProfile M E n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_geometricWeight_rpow_two_div {s q : ℝ} (hs : 0 < s) (hq : 0 < q) : Summable fun (n : ℕ) => HCPolySupport.Book.Ch02.geometricWeight s q n ^ (2 / q)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.summable_endpointWeight_mul_depthAmp {d : ℕ} (M : ABKModel d) (E : ℝ) {s : ℝ} (hgap : 0 < 2 * s - M.gamma) : Summable fun (n : ℕ) => endpointWeight (2 * s) n * superposedFluxDepthAmpProfile M E n

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_rootedWeight_mul_depthAmp_le {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (E : ℝ) {s q eps : ℝ} (hs : 0 < s) (hsOne : s ≤ 1) (hq : 0 < q) (heps : 0 < eps) (hepsOne : eps ≤ 1) (hwindow : M.gamma / 2 + eps ≤ s) : ∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n ^ (2 / q) * superposedFluxDepthAmpProfile M E n ≤ superposedFluxDepthAmpConst d * superposedFluxLowerPoleConst * Real.exp (-(superposedFluxBfaRate d * (E⁻¹ ^ 2 * M.gamma⁻¹))) * eps⁻¹ ^ 5

Uniform budget for either the rooted finite-exponent linear series or the endpoint series.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.tsum_endpointWeight_mul_depthAmp_le {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (E : ℝ) {s eps : ℝ} (hsOne : s ≤ 1) (heps : 0 < eps) (hepsOne : eps ≤ 1) (hwindow : M.gamma / 2 + eps ≤ s) : ∑' (n : ℕ), endpointWeight (2 * s) n * superposedFluxDepthAmpProfile M E n ≤ superposedFluxDepthAmpConst d * superposedFluxLowerPoleConst * Real.exp (-(superposedFluxBfaRate d * (E⁻¹ ^ 2 * M.gamma⁻¹))) * eps⁻¹ ^ 5