SiteTailsV2

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

Per-site tails at the successor logarithmic exponents

The localized-error leg is obtained from the Section 4 error-moment estimate. The localized-regularity leg is kept as one hypothesis with the exact existential shape of its successor moment estimate. The two Markov bounds and the shell estimate give the shifted per-site tail with logarithmic exponent -6 and accuracy floor sqrt gamma * |log gamma|^(7/2).

theorem Algsuperdiff.Section5.Provider.measureReal_localizedError_gt_le_v2 {d : ℕ} (M : Section3.ABKModel d) {c C ep : ℝ} (hc : 0 < c) (hC : 0 < C) (hep : 0 < ep) (hep4 : ep ≤ 1 / 4) (hcal : c ≤ (2 * Real.exp 1 * C)⁻¹ ^ 2) (hrange : c ≤ C⁻¹) (hfloor : 2 * Real.exp 1 * C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) (hmomE : ∀ (p : ℝ) (n : ℤ) (y : HCPolySupport.Vec d), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedError M n y omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) (hp1 : 1 ≤ Support.siteMarkovExponentV2 M c ep) (n : ℤ) (y : HCPolySupport.Vec d) : (↑(Section3.Cutoff.cutoffSampleLaw M)).real {omega : Section3.Cutoff.CutoffSample d | ENNReal.ofReal ep < Support.localizedError M n y omega} ≤ Real.exp (-Support.siteMarkovExponentV2 M c ep)

The error Markov leg at the successor exponent.

theorem Algsuperdiff.Section5.Provider.measureReal_localizedRegularity_gt_le_v2 {d : ℕ} (M : Section3.ABKModel d) {c creg Creg ep : ℝ} (hcreg : 0 < creg) (hCreg : 0 < Creg) (hc_le : c ≤ creg) (hmomX : ∀ (n : ℤ) (y : HCPolySupport.Vec d), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedRegularity M n y omega ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal Creg ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6))) (hep : 0 < ep) (hep4 : ep ≤ 1 / 4) (n : ℤ) (y : HCPolySupport.Vec d) : (↑(Section3.Cutoff.cutoffSampleLaw M)).real {omega : Section3.Cutoff.CutoffSample d | ENNReal.ofReal (2 * Creg) < Support.localizedRegularity M n y omega} ≤ Real.exp (-Support.siteMarkovExponentV2 M c ep)

The regularity Markov leg at the successor exponent.

noncomputable def Algsuperdiff.Section5.Provider.siteTailConstV2 (C creg Cinj : ℝ) : ℝ

The constant serving the error calibration, both moment ranges, and the shell comparison.

Equations

• Algsuperdiff.Section5.Provider.siteTailConstV2 C creg Cinj = min (min (min ((2 * Real.exp 1 * C)⁻¹ ^ 2) C⁻¹) creg) (Algsuperdiff.Section5.Support.siteThresholdConst Cinj ^ 2)

theorem Algsuperdiff.Section5.Provider.siteTailConstV2_pos {C creg Cinj : ℝ} (hC : 0 < C) (hcreg : 0 < creg) (hCinj : 0 < Cinj) : 0 < siteTailConstV2 C creg Cinj

theorem Algsuperdiff.Section5.Provider.siteTailConstV2_le_error (C creg Cinj : ℝ) : siteTailConstV2 C creg Cinj ≤ (2 * Real.exp 1 * C)⁻¹ ^ 2

theorem Algsuperdiff.Section5.Provider.siteTailConstV2_le_range (C creg Cinj : ℝ) : siteTailConstV2 C creg Cinj ≤ C⁻¹

theorem Algsuperdiff.Section5.Provider.siteTailConstV2_le_regularity (C creg Cinj : ℝ) : siteTailConstV2 C creg Cinj ≤ creg

theorem Algsuperdiff.Section5.Provider.siteTailConstV2_le_shell (C creg Cinj : ℝ) : siteTailConstV2 C creg Cinj ≤ Support.siteThresholdConst Cinj ^ 2

theorem Algsuperdiff.Section5.Provider.measureReal_compl_goodCubeEvent_le_v2 {d : ℕ} (M : Section3.ABKModel d) {c C creg Creg ep : ℝ} (hc : 0 < c) (hC : 0 < C) (hcreg : 0 < creg) (hCreg : 0 < Creg) (hep : 0 < ep) (hep4 : ep ≤ 1 / 4) (hcal : c ≤ (2 * Real.exp 1 * C)⁻¹ ^ 2) (hrange : c ≤ C⁻¹) (hc_le : c ≤ creg) (hfloor : 2 * Real.exp 1 * C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) (hmomE : ∀ (p : ℝ) (n : ℤ) (y : HCPolySupport.Vec d), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedError M n y omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) (hmomX : ∀ (n : ℤ) (y : HCPolySupport.Vec d), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedRegularity M n y omega ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal Creg ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6))) (hp1 : 1 ≤ Support.siteMarkovExponentV2 M c ep) (n : ℤ) (y : HCPolySupport.Vec d) : (↑(Section3.Cutoff.cutoffSampleLaw M)).real (Support.goodCubeEvent M Creg n y ep)ᶜ ≤ 2 * Real.exp (-Support.siteMarkovExponentV2 M c ep)

The complement of a good cube has the successor two-leg tail.

theorem Algsuperdiff.Section5.Provider.measureReal_siteBadEventFive_le_v2 {d : ℕ} (M : Section3.ABKModel d) {c C creg Creg Cinj ep : ℝ} (hc : 0 < c) (hC : 0 < C) (hcreg : 0 < creg) (hCreg : 0 < Creg) (hCinj : 0 < Cinj) (hep : 0 < ep) (hep4 : ep ≤ 1 / 4) (hcal : c ≤ (2 * Real.exp 1 * C)⁻¹ ^ 2) (hrange : c ≤ C⁻¹) (hc_reg : c ≤ creg) (hc_shell : c ≤ Support.siteThresholdConst Cinj ^ 2) (hfloor : 2 * Real.exp 1 * C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) (hmomE : ∀ (p : ℝ) (n : ℤ) (y : HCPolySupport.Vec d), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedError M n y omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) (hmomX : ∀ (n : ℤ) (y : HCPolySupport.Vec d), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedRegularity M n y omega ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal Creg ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6))) (hp1 : 1 ≤ Support.siteMarkovExponentV2 M c ep) (hlog3 : Real.log 3 ≤ Support.siteBadRateSqV2 M c ep) (hthr : 1 ≤ Support.siteThresholdConst Cinj * ep * (√M.gamma)⁻¹) (n : ℤ) (L : ℕ) (z : Percolation.Site d) : (↑(Section3.Cutoff.cutoffSampleLaw M)).real (Support.siteBadEventFive M Creg (Support.siteThresholdConst Cinj) ep n L z) ≤ Real.exp (-(Support.siteBadRateSqV2 M c ep * 3 ^ (Support.sitePathExponent * ↑L)))

The unshifted site family has the successor per-site tail.

theorem Algsuperdiff.Section5.Provider.measureReal_shiftedSiteBadEventFive_le_v2 {d : ℕ} (M : Section3.ABKModel d) {c C creg Creg Cinj ep : ℝ} (hc : 0 < c) (hC : 0 < C) (hcreg : 0 < creg) (hCreg : 0 < Creg) (hCinj : 0 < Cinj) (hep : 0 < ep) (hep4 : ep ≤ 1 / 4) (hcal : c ≤ (2 * Real.exp 1 * C)⁻¹ ^ 2) (hrange : c ≤ C⁻¹) (hc_reg : c ≤ creg) (hc_shell : c ≤ Support.siteThresholdConst Cinj ^ 2) (hfloor : 2 * Real.exp 1 * C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2) ≤ ep) (hmomE : ∀ (p : ℝ) (n : ℤ) (y : HCPolySupport.Vec d), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedError M n y omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) (hmomX : ∀ (n : ℤ) (y : HCPolySupport.Vec d), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedRegularity M n y omega ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal Creg ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6))) (hp1 : 1 ≤ Support.siteMarkovExponentV2 M c ep) (hlog3 : Real.log 3 ≤ Support.siteBadRateSqV2 M c ep) (hthr : 1 ≤ Support.siteThresholdConst Cinj * ep * (√M.gamma)⁻¹) (n : ℤ) (l : ℕ) (z : Percolation.Site d) : (↑(Section3.Cutoff.cutoffSampleLaw M)).real (Support.shiftedSiteBadEventFive M Creg (Support.siteThresholdConst Cinj) ep n l z) ≤ Real.exp (-(Support.siteTailRateV2 d M c ep ^ 2 * 3 ^ (Support.sitePathExponent * ↑l)))

The shifted site family has the successor per-site tail.

theorem Algsuperdiff.Section5.Provider.measureReal_shiftedSiteBadEventFive_le_of_epsLower_v2 {d : ℕ} (M : Section3.ABKModel d) {c C creg Creg Cinj Cpath ep : ℝ} (hc : 0 < c) (hC : 0 < C) (hcreg : 0 < creg) (hCreg : 0 < Creg) (hCinj : 0 < Cinj) (hcal : c ≤ (2 * Real.exp 1 * C)⁻¹ ^ 2) (hrange : c ≤ C⁻¹) (hc_reg : c ≤ creg) (hc_shell : c ≤ Support.siteThresholdConst Cinj ^ 2) (hmomE : ∀ (p : ℝ) (n : ℤ) (y : HCPolySupport.Vec d), 1 ≤ p → p ≤ C⁻¹ * M.gamma⁻¹ * |Real.log M.gamma|⁻¹ → ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedError M n y omega ^ p ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal (C * (√p + √|Real.log M.gamma|) * √M.gamma * |Real.log M.gamma| ^ 3) ^ p) (hmomX : ∀ (n : ℤ) (y : HCPolySupport.Vec d), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), Support.localizedRegularity M n y omega ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6)) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal Creg ^ (creg * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6))) (hep : ep ∈ Set.Icc (Support.siteEpsLowerConstV2 d c Cinj Cpath C * √M.gamma * |Real.log M.gamma|.rpow (7 / 2)) (1 / 4)) (n : ℤ) (l : ℕ) (z : Percolation.Site d) : (↑(Section3.Cutoff.cutoffSampleLaw M)).real (Support.shiftedSiteBadEventFive M Creg (Support.siteThresholdConst Cinj) ep n l z) ≤ Real.exp (-(Support.siteTailRateV2 d M c ep ^ 2 * 3 ^ (Support.sitePathExponent * ↑l)))

The shifted site-tail estimate derived from the two successor moment inputs.