UpperProfileExponents

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

Exponent arithmetic for the Section 3.3 upper profile.

The percolation and wave-tail estimates are run at sigma / 4, while the exceptional exponent in the frozen theorem is Gamma_{(1-sigma)/3}. The definitions below record the arithmetic buffer needed for the extra seam and collar powers.

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileSigma (sigma : ℝ) : ℝ

The reduced profile exponent used in upper coarse-ellipticity estimates.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileSigma sigma = sigma / 4

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileBaseSigma (sigma : ℝ) : ℝ

The complementary exponent for the upper profile's base contribution.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileBaseSigma sigma = 1 - Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileSigma sigma

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTailSigma (sigma : ℝ) : ℝ

The product-tail exponent associated with the reduced upper profile exponent.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTailSigma sigma = 1 / (1 + Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileSigma sigma)

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTargetSigma (sigma : ℝ) : ℝ

The target exponent in the upper coarse-ellipticity tail estimate.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTargetSigma sigma = (1 - sigma) / 3

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileHsepTau (sigma : ℝ) : ℝ

The weakest hsep-factor exponent whose product with the profile tail exponent equals the target exponent in the frozen theorem.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileHsepTau sigma = 4 * (1 - sigma) / (8 + 3 * sigma + sigma ^ 2)

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileHsepAuxSigma (sigma : ℝ) : ℝ

Auxiliary exponent fed to the hsep indicator theorem.

Equations

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

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileBaseSigma_pos {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : 0 < upperProfileBaseSigma sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTailSigma_pos {sigma : ℝ} (hsigma0 : 0 < sigma) (_hsigma : sigma ≤ 1 / 2) : 0 < upperProfileTailSigma sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTargetSigma_pos {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : 0 < upperProfileTargetSigma sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileHsepTau_pos {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : 0 < upperProfileHsepTau sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileHsepTau_lt_base {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : upperProfileHsepTau sigma < upperProfileBaseSigma sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileHsepAuxSigma_pos {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : 0 < upperProfileHsepAuxSigma sigma

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfile_hsep_productSigma_eq {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : upperProfileBaseSigma sigma * upperProfileHsepAuxSigma sigma / (upperProfileBaseSigma sigma + upperProfileHsepAuxSigma sigma) = upperProfileHsepTau sigma

The hsep indicator product theorem at the auxiliary exponent produces the required hsep-factor exponent exactly.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfile_hsep_mul_tailSigma_eq {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : upperProfileHsepTau sigma * upperProfileTailSigma sigma / (upperProfileHsepTau sigma + upperProfileTailSigma sigma) = upperProfileTargetSigma sigma

The required hsep exponent times the profile tail exponent equals the exceptional exponent in the frozen theorem.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTargetSigma_le_hsep_mul_one {sigma : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) : upperProfileTargetSigma sigma ≤ upperProfileHsepTau sigma / (upperProfileHsepTau sigma + 1)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.productSigma_mono_left {a b r : ℝ} (ha : 0 < a) (hab : a ≤ b) (hr : 0 < r) : a * r / (a + r) ≤ b * r / (b + r)

Harmonic-product exponents are monotone in their first input.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileHsepTau_le_collarPowerSigma {sigma gamma b : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgamma0 : 0 ≤ gamma) (hb : 0 < b) (hgamma : gamma ≤ b * sigma) : upperProfileHsepTau sigma ≤ upperProfileBaseSigma sigma / ((2 * gamma + 2 * b) / b)

The direct collar power 3^((2 gamma + 2b) hsep) remains strong enough when the frozen gate has paid gamma ≤ b sigma.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.upperProfileTargetSigma_le_collarPower_mul_tail {sigma gamma b : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgamma0 : 0 ≤ gamma) (hb : 0 < b) (hgamma : gamma ≤ b * sigma) : upperProfileTargetSigma sigma ≤ upperProfileBaseSigma sigma / ((2 * gamma + 2 * b) / b) * upperProfileTailSigma sigma / (upperProfileBaseSigma sigma / ((2 * gamma + 2 * b) / b) + upperProfileTailSigma sigma)

Consequently the collar power times the profile tail still reaches the exceptional exponent in the frozen theorem.