Coarse-graining support: Support.HighContrast.EntryScale.MomentConsequences.P1

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Consequences of the high centered moment hypothesis

Planned home for the union-bound and terminal fluctuation steps derived from Assumption a.HM.

theorem HCPolySupport.HighContrast.EntryScale.highCenteredMoment_two_mul_p4_xi_le_Q {d : ℕ} [NeZero d] {P : Book.Ch04.RestrictionCoeffLaw d} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (hP4 : Book.Ch05.QuantitativeCoarseGrainedEllipticity P) (hparams : hP4.params = hm.p4Params) : 2 * ↑hP4.xi ≤ hm.Q

Source labels a.HM, e.Q.large, and p.HC.CR: the high moment exponent dominates the finite Holder exponent needed for the bad-event square.

theorem HCPolySupport.HighContrast.EntryScale.highCenteredMoment_Q_pos {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) : 0 < hm.Q

Source labels a.HM, e.Q.large, l.union.bound: the high-moment exponent is strictly positive.

theorem HCPolySupport.HighContrast.EntryScale.highCenteredMoment_Q_mul_rhoM_sub_dim_pos {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) : 0 < hm.Q * hc.rhoM - ↑d

Source label l.union.bound: Q rho_M > d + 4 implies the positive union-bound decay exponent Q rho_M - d.

theorem HCPolySupport.HighContrast.EntryScale.highCenteredMoment_min_decay_pos {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) : 0 < min (hm.Q * hc.rhoM - ↑d) (hm.Q * hm.gamma)

Source label l.union.bound: positivity of the convolution decay exponent c_Q = min {Q rho_M - d, Q gamma}.

theorem HCPolySupport.HighContrast.EntryScale.tendsto_linear_mul_rpow_three_neg_atTop_nhds_zero {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (n : ℕ) => (↑n + 1) * 3 ^ (-c * ↑n)) Filter.atTop (nhds 0)

Source label l.union.bound: the linear prefactor in (1 + m - N) 3^{-c(m-N)} is absorbed by the exponential decay.

theorem HCPolySupport.HighContrast.EntryScale.exists_forall_ge_const_mul_linear_rpow_three_neg_le {C c η : ℝ} (hc : 0 < c) (hη : 0 < η) : ∃ (K : ℕ), ∀ (n : ℕ), K ≤ n → C * ((↑n + 1) * 3 ^ (-c * ↑n)) ≤ η

Source label l.union.bound: a concrete threshold after which C (n+1) 3^{-c n} is smaller than any prescribed positive tolerance.

theorem HCPolySupport.HighContrast.EntryScale.buffered_polynomial_geometric_envelope_le_linear_geometric {C A c B T : ℝ} {n : ℕ} (hC : 0 ≤ C) (hc : 0 < c) (hT : 1 ≤ T) (hBlarge : 2 * A ≤ c * B) (hbuf : B * Real.logb 3 (2 + T) ≤ ↑n) : C * ((2 + T) ^ A * ((↑n + 1) * 3 ^ (-c * ↑n))) ≤ C * ((↑n + 1) * 3 ^ (-(c / 2) * ↑n))

Source label l.union.bound: the logarithmic buffer turns the polynomial contrast factor (2+T)^A into half of the geometric decay.

theorem HCPolySupport.HighContrast.EntryScale.exists_bufferExponent_for_polynomial_geometric_envelope_le {C A c η : ℝ} (hC : 0 ≤ C) (hc : 0 < c) (hη : 0 < η) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ {T : ℝ} {n : ℕ}, 1 ≤ T → B * Real.logb 3 (2 + T) ≤ ↑n → C * ((2 + T) ^ A * ((↑n + 1) * 3 ^ (-c * ↑n))) ≤ η

Source label l.union.bound: after choosing the buffer exponent large enough, the manuscript envelope C (2+T)^A (n+1) 3^{-c n} is uniformly small for n >= B log_3(2+T) and T >= 1.

theorem HCPolySupport.HighContrast.EntryScale.exists_bufferExponent_for_polynomial_geometric_envelope_no_linear_le {C A c η : ℝ} (hC : 0 ≤ C) (hc : 0 < c) (hη : 0 < η) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ {T : ℝ} {n : ℕ}, 1 ≤ T → B * Real.logb 3 (2 + T) ≤ ↑n → C * ((2 + T) ^ A * 3 ^ (-c * ↑n)) ≤ η

Source label l.union.bound: variant of the logarithmic-buffer absorption without the harmless linear prefactor.

theorem HCPolySupport.HighContrast.EntryScale.exists_bufferExponent_subthresholdPolynomialMomentEnvelope_le {d : ℕ} (hc : HighContrastExponents d) (sub : SubthresholdPolynomialMomentParameters) {η : ℝ} (hη : 0 < η) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ {T : ℝ} {n : ℕ}, 1 ≤ T → B * Real.logb 3 (2 + T) ≤ ↑n → subthresholdPolynomialMomentEnvelope hc sub T n ≤ ENNReal.ofReal η

Source labels a.HM.subthreshold and l.union.bound: the old polynomial subthreshold bound is killed by the same logarithmic buffer, with squared weak-norm decay 3^{-2 rho_M (m-N)}.

theorem HCPolySupport.HighContrast.EntryScale.exists_bufferExponent_subthresholdPolynomialMomentEnvelope_le_of_Nstar {d : ℕ} (hc : HighContrastExponents d) (sub : SubthresholdPolynomialMomentParameters) {η : ℝ} (hη : 0 < η) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ {T : ℝ} {N m : ℕ}, 1 ≤ T → N + ⌈B * Real.logb 3 (2 + T)⌉₊ ≤ m → subthresholdPolynomialMomentEnvelope hc sub T (m - N) ≤ ENNReal.ofReal η

Source labels e.Nstar, a.HM.subthreshold, and l.union.bound: manuscript form of the subthreshold polynomial-envelope absorption with m >= N + ceil(B log_3(2+T)).

theorem HCPolySupport.HighContrast.EntryScale.exists_bufferExponent_lintegral_enorm_rpow_two_subthresholdMax_le_of_Nstar {d : ℕ} (hc : HighContrastExponents d) (sub : SubthresholdPolynomialMomentParameters) {η : ℝ} (hη : 0 < η) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {T : ℝ} {N m : ℕ}, 1 ≤ T → N + ⌈B * Real.logb 3 (2 + T)⌉₊ ≤ m → ∀ {M_sub : ℕ → Ω → ℝ}, SubthresholdPolynomialMomentEstimate hc sub μ T N M_sub → ∫⁻ (ω : Ω), ‖M_sub m ω‖ₑ ^ 2 ∂μ ≤ ENNReal.ofReal η

Source labels M_m^{<N}, a.HM.subthreshold, and l.union.bound: once the source-facing old polynomial subthreshold estimate is available, the logarithmic buffer makes its second moment smaller than η.

theorem HCPolySupport.HighContrast.EntryScale.nstar_le_of_bufferExponent_le {B₀ B T : ℝ} {N m : ℕ} (hB₀B : B₀ ≤ B) (hT : 1 ≤ T) (hNstar : N + ⌈B * Real.logb 3 (2 + T)⌉₊ ≤ m) : N + ⌈B₀ * Real.logb 3 (2 + T)⌉₊ ≤ m

Source label e.Nstar: increasing the buffer exponent preserves the manuscript lower bound m >= N + ceil(B log_3(2+T)).

theorem HCPolySupport.HighContrast.EntryScale.ofReal_highCenteredMoment_halfBudget_rpow_eq {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) {η : ℝ} (hη : 0 < η) : ENNReal.ofReal ((η / 2) ^ (hm.Q / 2)) ^ (2 / hm.Q) = ENNReal.ofReal (η / 2)

Source label l.union.bound: the terminal high-moment tolerance can be chosen so that the 2 / Q moment conversion lands exactly on half of the final second-moment budget.

theorem HCPolySupport.HighContrast.EntryScale.exists_bufferExponent_highCenteredMoment_convolutionEnvelope_le {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) {η : ℝ} (hη : 0 < η) : ∃ (B : ℝ), 1 ≤ B ∧ ∀ {T : ℝ} {n : ℕ}, 1 ≤ T → B * Real.logb 3 (2 + T) ≤ ↑n → hm.momentCoefficient * ((2 + T) ^ hm.Q * ((↑n + 1) * 3 ^ (-min (hm.Q * hc.rhoM - ↑d) (hm.Q * hm.gamma) * ↑n))) ≤ η

Source label l.union.bound: high-moment specialization of the buffer smallness statement for the convolution envelope C_Q (2+T)^Q (n+1) 3^{-c_Q n}.

theorem HCPolySupport.HighContrast.EntryScale.rpow_three_two_scale_decay_le_min_decay {α β c : ℝ} {N j m : ℕ} (hNj : N ≤ j) (hjm : j ≤ m) (hcα : c ≤ α) (hcβ : c ≤ β) : 3 ^ (-α * ↑(m - j)) * 3 ^ (-β * ↑(j - N)) ≤ 3 ^ (-c * ↑(m - N))

Source label l.union.bound: a single term in the two-scale convolution is controlled by the minimum decay exponent. Here α represents Q ρ_M - d, β represents Q γ, and c will be their minimum.

theorem HCPolySupport.HighContrast.EntryScale.sum_Icc_rpow_three_two_scale_decay_le_card_mul_min_decay {α β c : ℝ} {N m : ℕ} (hcα : c ≤ α) (hcβ : c ≤ β) : ∑ j ∈ Finset.Icc N m, 3 ^ (-α * ↑(m - j)) * 3 ^ (-β * ↑(j - N)) ≤ ↑(Finset.Icc N m).card * 3 ^ (-c * ↑(m - N))

Source label l.union.bound: finite convolution bound for the two decay mechanisms before substituting the high-moment exponents.

theorem HCPolySupport.HighContrast.EntryScale.sum_Icc_rpow_three_two_scale_decay_le_length_mul_min_decay {α β c : ℝ} {N m : ℕ} (hNm : N ≤ m) (hcα : c ≤ α) (hcβ : c ≤ β) : ∑ j ∈ Finset.Icc N m, 3 ^ (-α * ↑(m - j)) * 3 ^ (-β * ↑(j - N)) ≤ ↑(m - N + 1) * 3 ^ (-c * ↑(m - N))

Source label l.union.bound: finite convolution bound in the manuscript's (1 + m - N) 3^{-c_Q(m-N)} form.

theorem HCPolySupport.HighContrast.EntryScale.sum_Icc_rpow_three_highCenteredMoment_convolution_le {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) {N m : ℕ} (hNm : N ≤ m) : ∑ j ∈ Finset.Icc N m, 3 ^ (-(hm.Q * hc.rhoM - ↑d) * ↑(m - j)) * 3 ^ (-(hm.Q * hm.gamma) * ↑(j - N)) ≤ ↑(m - N + 1) * 3 ^ (-min (hm.Q * hc.rhoM - ↑d) (hm.Q * hm.gamma) * ↑(m - N))

Source labels l.union.bound, a.HM: high-moment specialization of the two-scale convolution estimate appearing in the stochastic maximal union bound.

noncomputable def HCPolySupport.HighContrast.EntryScale.terminalWeakMomentWeight {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (terminalCost : ENNReal) (m j : ℕ) : ENNReal

Source label l.union.bound: the deterministic Q-moment envelope for the product of the terminal-normalization cost and the weak-norm scale weight 3^{-rho_M(m-j)}.

Equations

• HCPolySupport.HighContrast.EntryScale.terminalWeakMomentWeight hm terminalCost m j = terminalCost ^ hm.Q * ENNReal.ofReal (3 ^ (-(hm.Q * hc.rhoM) * ↑(m - j)))

theorem HCPolySupport.HighContrast.EntryScale.rpow_le_terminalWeakMomentWeight_of_le {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) {terminalCost : ENNReal} {m j : ℕ} {w : TriadicCube d → ENNReal} {R : TriadicCube d} (hw : w R ≤ terminalCost * ENNReal.ofReal (3 ^ (-hc.rhoM * ↑(m - j)))) : w R ^ hm.Q ≤ terminalWeakMomentWeight hm terminalCost m j

Source label l.union.bound: if the deterministic multiplier is bounded by terminalCost * 3^{-rho_M(m-j)}, then its Q-moment is bounded by the factorized terminal weak-moment envelope used in the descendant sum.

theorem HCPolySupport.HighContrast.EntryScale.real_descendant_count_mul_highCenteredMoment_decay_eq {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) {N m j : ℕ} : ↑((3 ^ d) ^ (m - j)) * 3 ^ (-(hm.Q * hc.rhoM) * ↑(m - j)) * (hm.momentCoefficient * 3 ^ (-(hm.Q * hm.gamma) * ↑(j - N))) = hm.momentCoefficient * (3 ^ (-(hm.Q * hc.rhoM - ↑d) * ↑(m - j)) * 3 ^ (-(hm.Q * hm.gamma) * ↑(j - N)))

Source label l.union.bound: real algebra turning descendant counting and the two decay weights into the manuscript's convolution summand.

theorem HCPolySupport.HighContrast.EntryScale.terminalWeak_highCenteredMoment_summand_eq_convolution {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (terminalCost : ENNReal) {N m j : ℕ} : ↑((3 ^ d) ^ (m - j)) * (terminalWeakMomentWeight hm terminalCost m j * highCenteredMomentEnvelope hm N j) = terminalCost ^ hm.Q * ENNReal.ofReal (hm.momentCoefficient * (3 ^ (-(hm.Q * hc.rhoM - ↑d) * ↑(m - j)) * 3 ^ (-(hm.Q * hm.gamma) * ↑(j - N))))

Source label l.union.bound: the explicit ENNReal summand produced by the terminal/weak bridge and a.HM is exactly the C_Q multiple of the real two-scale convolution summand, times the terminal normalization cost.

theorem HCPolySupport.HighContrast.EntryScale.sum_Icc_terminalWeak_highCenteredMomentEnvelope_le_convolution {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (terminalCost : ENNReal) {N m : ℕ} (hNm : N ≤ m) : ∑ j ∈ Finset.Icc N m, ↑((3 ^ d) ^ (m - j)) * (terminalWeakMomentWeight hm terminalCost m j * highCenteredMomentEnvelope hm N j) ≤ terminalCost ^ hm.Q * ENNReal.ofReal (hm.momentCoefficient * (↑(m - N + 1) * 3 ^ (-min (hm.Q * hc.rhoM - ↑d) (hm.Q * hm.gamma) * ↑(m - N))))

Source label l.union.bound: after substituting a.HM, terminal normalization, weak weights, and the library's descendant counting, the finite ENNReal sum is bounded by the real convolution envelope from the paper.

theorem HCPolySupport.HighContrast.EntryScale.terminalCost_rpow_le_polynomial_of_le {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) {terminalCost : ENNReal} {T A : ℝ} (hT : 1 ≤ T) (hcost : terminalCost ≤ ENNReal.ofReal ((2 + T) ^ A)) : terminalCost ^ hm.Q ≤ ENNReal.ofReal ((2 + T) ^ (A * hm.Q))

Source label l.union.bound: once the terminal-normalization multiplier is bounded by (2+T)^A, its Q-moment contribution is bounded by (2+T)^{A Q}.

theorem HCPolySupport.HighContrast.EntryScale.eLpNorm_two_le_eLpNorm_of_two_le_real_exponent {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {Q : ℝ} (hQ : 2 ≤ Q) : MeasureTheory.eLpNorm X 2 μ ≤ MeasureTheory.eLpNorm X (ENNReal.ofReal Q) μ

Source label l.S.and.J: Lyapunov monotonicity from the high Q moment to the second moment on a probability space.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_enorm_rpow_two_le_lintegral_enorm_rpow_rpow_of_two_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {Q : ℝ} {B : ENNReal} (hQ : 2 ≤ Q) (hX : MeasureTheory.AEStronglyMeasurable X μ) (hB : ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ Q ∂μ ≤ B) : ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ ≤ B ^ (2 / Q)

Source label l.union.bound: the manuscript step "Taking the power 2 / Q" from a Q-moment estimate to a second-moment estimate.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_enorm_rpow_two_le_lintegral_enorm_rpow_rpow_highCenteredMoment {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (hX : MeasureTheory.AEStronglyMeasurable X μ) {B : ENNReal} (hB : ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ hm.Q ∂μ ≤ B) : ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ ≤ B ^ (2 / hm.Q)

Source labels a.HM, l.union.bound: high-moment-parameter specialization of the 2 / Q power conversion for stochastic maximal variables.

theorem HCPolySupport.HighContrast.EntryScale.enorm_ennreal_toReal_le (x : ENNReal) : ‖x.toReal‖ₑ ≤ x

Source label M_m^st: the coercion from an ENNReal finite maximum to the real maximum is harmless for upper bounds by the original ENNReal quantity.

theorem HCPolySupport.HighContrast.EntryScale.lintegral_enorm_rpow_two_le_of_lintegral_ennreal_envelope_highCenteredMoment {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {Z : Ω → ENNReal} {d : ℕ} {hc : HighContrastExponents d} (hm : HighCenteredMomentParameters d hc) (hX : MeasureTheory.AEStronglyMeasurable X μ) {B : ENNReal} (hpoint : ∀ (ω : Ω), ‖X ω‖ₑ ^ hm.Q ≤ Z ω) (hB : ∫⁻ (ω : Ω), Z ω ∂μ ≤ B) : ∫⁻ (ω : Ω), ‖X ω‖ₑ ^ 2 ∂μ ≤ B ^ (2 / hm.Q)

Source labels l.union.bound, M_m^st: an ENNReal envelope controlling the Q-th power of a real stochastic maximum also controls its second moment.