SuperposedFluxLowerProfile

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

Quantitative profile and exact lower coarse-ellipticity provider

This file develops the quantitative profile needed to turn the sharp superposed-flux payoff into the representative and three exponent branches.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpConst_le_profile {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (k : ℕ) {E : ℝ} (hE : 1 ≤ E) (hgamma20 : M.gamma ≤ 1 / 20) (hbeta9 : 9 * superposedFluxRateBeta M ≤ 1) (hk₀ : ↑(superposedFluxPrimaryDepth M E) ≤ superposedFluxRate M E) : superposedFluxSharpConst M (m - 1 - ↑k) (m - 1) (superposedFluxRateEps M) (superposedFluxRateBeta M) (superposedFluxPrimaryDepth M E) (superposedFluxRareDepth M E) ≤ superposedFluxSharpDetConst d * 3 ^ (M.gamma * ↑k)

The sharp deterministic slot has the required dimension-only geometric profile.

Exponential rate of the sharp random slot

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

The retained rare rate after paying the collar shift.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpRareRate d = Algsuperdiff.Section3.Provider.Percolation.siteRateBase d / 1152

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpRareRate_pos (d : ℕ) : 0 < superposedFluxSharpRareRate d

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxSharpRare_le_exp_rate {d : ℕ} (M : ABKModel d) {sigma E : ℝ} (hE : 1 ≤ E) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) : superposedFluxSharpRare (superposedFluxRateBeta M) (superposedFluxPrimaryDepth M E) (superposedFluxRareDepth M E) ≤ Real.exp (1 / 36) * Real.exp (-(superposedFluxSharpRareRate d * (E⁻¹ ^ 2 * M.gamma⁻¹)))

The collar shift consumes at most half of the kp/36 rate.

Uniform constants on the fixed B parameter window

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxHsepConst : ℝ

Uniform amplitude of the minimal-separation tail on 0 < sigma / 4 ≤ 1/8.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxHsepConst_pos : 0 < superposedFluxHsepConst

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.hsepAmplitude_le_superposedFluxHsepConst {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 8) : Percolation.hsepAmplitude sigma bfaProfileB ≤ superposedFluxHsepConst

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxTriangleConst : ℝ

A uniform bound for the triangle constant once the B exponent is at least 1/4.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxTriangleConst = 4 * 625 ^ 12

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gammaTriangleConst_le_superposedFluxTriangleConst {tau : ℝ} (htau : 1 / 4 ≤ tau) : HCPolySupport.IndependentSums.gammaTriangleConst tau ≤ superposedFluxTriangleConst

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.one_fourth_le_bfaTau_of_eighth_window {sigma gam b : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 8) (hgam : 0 < gam) (hb : 0 < b) (hgamb : gam ≤ b) : 1 / 4 ≤ Multiscale.bfaTau sigma gam b

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gammaProductConst_le_sixteen_of_eighth_window {sigma gam b : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 8) (hgam : 0 < gam) (hb : 0 < b) (hgamb : gam ≤ b) : HCPolySupport.Book.Ch04.gammaProductConst (1 - sigma) (Multiscale.bfaSigmaTwo sigma gam b) ≤ 16

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.hsepAmplitude_rpow_bfaPower_le_profile_cube {sigma gam : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 8) (hgamb : gam ≤ bfaProfileB) : Percolation.hsepAmplitude sigma bfaProfileB ^ Multiscale.bfaPower gam bfaProfileB ≤ superposedFluxHsepConst ^ 3

The uniform sharp B lane at a dimension-only rate

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxBfaTruncRate : ℝ

Exponential rate retained from the truncated minimal-separation lane after the local exponent is specialized to 7 * gamma.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxBfaTruncRate = Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaProfileB * Real.log 3 / 567

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxBfaTruncRate_pos : 0 < superposedFluxBfaTruncRate

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

The common exponential rate of the truncation and retained rare lanes.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.superposedFluxBfaRate_pos (d : ℕ) : 0 < superposedFluxBfaRate d

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

Dimension-only amplitude multiplying the common exponential B rate.

Equations

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

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.bfaLaneScale_sharp_le_exp_profile {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) (m : ℤ) (k : ℕ) {sigma E : ℝ} (hE : 1 ≤ E) (hsigma : 0 < sigma) (hsigmaHalf : sigma ≤ 1 / 2) (hmax : max (Real.exp (profileAuxiliaryConst d / sigma)) (Disorder.cstar M)⁻¹ ≤ E) (hEgamma : E ≤ M.gamma ^ (-(1 / 5))) : Multiscale.bfaLaneScale (bfaProfileSigma sigma) bfaProfileB (7 * M.gamma) (superposedFluxSharpConst M (m - 1 - ↑k) (m - 1) (superposedFluxRateEps M) (superposedFluxRateBeta M) (superposedFluxPrimaryDepth M E) (superposedFluxRareDepth M E)) (superposedFluxSharpRare (superposedFluxRateBeta M) (superposedFluxPrimaryDepth M E) (superposedFluxRareDepth M E)) ≤ superposedFluxBfaConst d * 3 ^ (M.gamma * ↑k) * Real.exp (-(superposedFluxBfaRate d * (E⁻¹ ^ 2 * M.gamma⁻¹)))

The exact sharp B amplitude has a dimension-only prefactor, the required 3^(gamma k) collar, and a strictly positive multiple of E⁻² gamma⁻¹ in its exponential rate.