UpperProfileProducts

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

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

The hsep exponent stays above one fifth throughout the terminal window.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gammaProductConst_one_le_sixtyFour {alpha : ℝ} (halphaLower : 1 / 5 ≤ alpha) : HCPolySupport.Book.Ch04.gammaProductConst alpha 1 ≤ 64

A first exponent of at least one fifth bounds the product constant by 64.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.gammaProductConst_collarPower_le_sixtyFour {sigma gamma b : ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgamma0 : 0 ≤ gamma) (hb : 0 < b) (hgamma : gamma ≤ b * sigma) : HCPolySupport.Book.Ch04.gammaProductConst (upperProfileBaseSigma sigma / ((2 * gamma + 2 * b) / b)) 1 ≤ 64

Collar exponents obey the same uniform product bound for any positive gate.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_hsep_mul_one {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {sigma AR AZ : ℝ} {R Z : Omega → ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hAR : 0 ≤ AR) (hAZ : 0 ≤ AZ) (hR0 : ∀ (omega : Omega), 0 ≤ R omega) (hZ0 : ∀ (omega : Omega), 0 ≤ Z omega) (hR : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileHsepTau sigma)) R AR) (hZ : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) Z AZ) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (fun (omega : Omega) => R omega * Z omega) (HCPolySupport.Book.Ch04.gammaProductConst (upperProfileHsepTau sigma) 1 * AR * AZ)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_hsep_mul_tail {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {sigma AR AZ : ℝ} {R Z : Omega → ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hAR : 0 ≤ AR) (hAZ : 0 ≤ AZ) (hR0 : ∀ (omega : Omega), 0 ≤ R omega) (hZ0 : ∀ (omega : Omega), 0 ≤ Z omega) (hR : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileHsepTau sigma)) R AR) (hZ : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileTailSigma sigma)) Z AZ) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (fun (omega : Omega) => R omega * Z omega) (HCPolySupport.Book.Ch04.gammaProductConst (upperProfileHsepTau sigma) (upperProfileTailSigma sigma) * AR * AZ)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_collarPower_mul_one {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {sigma gamma b AR AZ : ℝ} {R Z : Omega → ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgamma0 : 0 ≤ gamma) (hb : 0 < b) (hgamma : gamma ≤ b * sigma) (hAR : 0 ≤ AR) (hAZ : 0 ≤ AZ) (hR0 : ∀ (omega : Omega), 0 ≤ R omega) (hZ0 : ∀ (omega : Omega), 0 ≤ Z omega) (hR : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileBaseSigma sigma / ((2 * gamma + 2 * b) / b))) R AR) (hZ : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 1) Z AZ) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (fun (omega : Omega) => R omega * Z omega) (HCPolySupport.Book.Ch04.gammaProductConst (upperProfileBaseSigma sigma / ((2 * gamma + 2 * b) / b)) 1 * AR * AZ)

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.isBigOWith_upperProfileTarget_collarPower_mul_tail {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {sigma gamma b AR AZ : ℝ} {R Z : Omega → ℝ} (hsigma0 : 0 < sigma) (hsigma : sigma ≤ 1 / 2) (hgamma0 : 0 ≤ gamma) (hb : 0 < b) (hgamma : gamma ≤ b * sigma) (hAR : 0 ≤ AR) (hAZ : 0 ≤ AZ) (hR0 : ∀ (omega : Omega), 0 ≤ R omega) (hZ0 : ∀ (omega : Omega), 0 ≤ Z omega) (hR : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileBaseSigma sigma / ((2 * gamma + 2 * b) / b))) R AR) (hZ : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileTailSigma sigma)) Z AZ) : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma (upperProfileTargetSigma sigma)) (fun (omega : Omega) => R omega * Z omega) (HCPolySupport.Book.Ch04.gammaProductConst (upperProfileBaseSigma sigma / ((2 * gamma + 2 * b) / b)) (upperProfileTailSigma sigma) * AR * AZ)