Stat.Polynomial­Tail

Polynomial lower-tail moment analysis: the polynomial small-value tail law for a bounded positive variable, truncated inverse first/second moment asymptotics, the trimming-bias bound, and the bias-variance rate-balancing algebra.

Basic 7 core · 14 supporting This module defines the reusable setup for polynomial lower-tail calculations. ★ measureReal_lt_le

Polynomial lower-tail setup

This module defines the reusable setup for polynomial lower-tail calculations. The structure PolyTail P U kappa t0 cm cp states that the lower CDF of a positive [0,1]-valued variable U is squeezed between cm * t ^ kappa and cp * t ^ kappa on (0, t0]; TailSetup P U records the measurability and almost-sure bounds 0 < U <= 1.

The main integrands are the truncated denominator truncDen U lam, the inverse second moment invMomentI P U lam = int U / (max U lam)^2, the inverse first moment invMomentJ P U lam = int (max U lam)^(-1), and the trimming weight trimWeight U lam = 1 - U / (max U lam). The file proves their measurability, elementary pointwise bounds, the open lower-level-set mass bound measureReal_lt_le, and bounded integrability lemmas used by the layer-cake and regime-bound modules.

structure PolyTail reviewed
Causalean.Stat.PolynomialTail

Polynomial lower tail. For a measurable [0,1]-valued function U, says that the lower CDF t ↦ P{U ≤ t} is squeezed between cm·tᵏ and cp·tᵏ on the window (0, t₀], with a positive exponent κ, a window endpoint t₀ strictly between 0 and 1, and constants with 0 < cm < cp. This is the sole distributional input to the inverse-moment asymptotics.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
P :
Measure Ω
U :
Ω → ℝ
κ t₀ cm cp :
ℝ
assumes
kappa_pos :
0 < κ

The tail exponent is positive.

t0_pos :
0 < t₀

The window upper endpoint is positive.

t0_lt_one :
t₀ < 1

The window endpoint is < 1.

cm_pos :
0 < cm

The lower constant is positive.

cm_lt_cp :
cm < cp

The lower constant is strictly below the upper constant.

tail_lower :
∀ t
if
0 < t
and
t ≤ t₀
then
cm * t ^ κ ≤ P.real {ω | U ω ≤ t}

Lower polynomial bound on the CDF over the window.

tail_upper :
∀ t
if
0 < t
and
t ≤ t₀
then
P.real {ω | U ω ≤ t} ≤ cp * t ^ κ

Upper polynomial bound on the CDF over the window.

Causalean.Stat.PolynomialTail.PolyTail · Causalean/Stat/PolynomialTail/Basic.lean:58
structure TailSetup reviewed
Causalean.Stat.PolynomialTail

Tail setup. Bundles the structural hypotheses on U: measurability and 0 < U ≤ 1 almost surely. IsProbabilityMeasure P is required separately as a typeclass on the theorems that need it.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
P :
Measure Ω
U :
Ω → ℝ
assumes
measurable :
Measurable U

U is measurable.

pos :
∀ᵐ ω ∂P, 0 < U ω

U is a.s. positive.

le_one :
∀ᵐ ω ∂P, U ω ≤ 1

U is a.s. bounded by 1.

Causalean.Stat.PolynomialTail.TailSetup · Causalean/Stat/PolynomialTail/Basic.lean:95
def truncDen reviewed
Causalean.Stat.PolynomialTail

For a sample space, a real-valued variable on that space, a real threshold, and a sample point, the truncated denominator is the larger of the variable's value at that point and the threshold.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
U :
Ω → ℝ
lam :
ℝ
ω :
Ω
def
truncDen U lam ω :
ℝ
given by
max (U ω) lam
Causalean.Stat.PolynomialTail.truncDen · Causalean/Stat/PolynomialTail/Basic.lean:112
def invMomentI reviewed
Causalean.Stat.PolynomialTail

For a measurable sample space, a measure on that space, a real-valued variable, and a real threshold, the truncated inverse second moment is the integral of the variable divided by the square of the larger of its value and the threshold.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
P :
Measure Ω
U :
Ω → ℝ
lam :
ℝ
def
invMomentI P U lam :
ℝ
given by
∫ ω, U ω / (max (U ω) lam) ^ 2 ∂P
Causalean.Stat.PolynomialTail.invMomentI · Causalean/Stat/PolynomialTail/Basic.lean:117
def invMomentJ reviewed
Causalean.Stat.PolynomialTail

For a measurable sample space, a measure on that space, a real-valued variable, and a real threshold, the truncated inverse first moment is the integral of the reciprocal of the larger of the variable's value and the threshold.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
P :
Measure Ω
U :
Ω → ℝ
lam :
ℝ
def
invMomentJ P U lam :
ℝ
given by
∫ ω, (max (U ω) lam)⁻¹ ∂P
Causalean.Stat.PolynomialTail.invMomentJ · Causalean/Stat/PolynomialTail/Basic.lean:125
def trimWeight reviewed
Causalean.Stat.PolynomialTail

For a sample space, a real-valued variable on that space, a real threshold, and a sample point, the trimming weight is one minus the variable's value divided by the larger of that value and the threshold.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
U :
Ω → ℝ
lam :
ℝ
ω :
Ω
def
trimWeight U lam ω :
ℝ
given by
1 - U ω / (max (U ω) lam)
Causalean.Stat.PolynomialTail.trimWeight · Causalean/Stat/PolynomialTail/Basic.lean:133
theorem measureReal_lt_le reviewed
Causalean.Stat.PolynomialTail

Mass below λ. Under the polynomial lower-tail hypothesis packaged in h, for a threshold λ that is positive and at most the window endpoint t₀, the open lower level set {U < λ} has P-mass at most cp · λᵏ. Immediate from monotonicity and the upper tail bound at t = λ.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
lam :
ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsFiniteMeasure P
h :
PolyTail P U κ t₀ cm cp
hlam_pos :
0 < lam
hlam_le :
lam ≤ t₀
conclusion
P.real {ω | U ω < lam} ≤ cp * lam ^ κ
Proof (Lean source)
theorem measureReal_lt_le [IsFiniteMeasure P] (h : PolyTail P U κ t₀ cm cp) (hlam_pos : 0 < lam) (hlam_le : lam ≤ t₀) : P.real {ω | U ω < lam} ≤ cp * lam ^ κ := by have hsub : {ω | U ω < lam} ⊆ {ω | U ω ≤ lam} := fun ω (hω : U ω < lam) => hω.le exact le_trans (measureReal_mono hsub (measure_ne_top P _)) (h.tail_upper lam hlam_pos hlam_le)
Causalean.Stat.PolynomialTail.measureReal_lt_le · Causalean/Stat/PolynomialTail/Basic.lean:184 · uses PolyTail
14 supporting declarations (lemmas, instances)
Layer­Cake­Reduction 2 core · 6 supporting This module isolates the one-dimensional threshold integral that controls the truncated inverse first moment. ★ invMomentJ_eq_one_add_tailIntegral

Layer-cake reduction to the tail integral

This module isolates the one-dimensional threshold integral that controls the truncated inverse first moment. The definition tailIntegral P U lam = int t in Ioc 1 lam^(-1), P.real {omega | U omega <= t^(-1)} captures the nonconstant part of the layer-cake formula for invMomentJ.

The central theorem invMomentJ_eq_one_add_tailIntegral proves the exact identity invMomentJ P U lam = 1 + tailIntegral P U lam for 0 < lam < 1 under TailSetup. Auxiliary results establish monotonicity and measurability of the lower CDF, bounded integrability of the tail integrand, and nonnegativity of tailIntegral. The polynomial-tail assumption is not used here; it enters later through the sandwich bounds in TailIntegralBounds.

def tailIntegral reviewed
Causalean.Stat.PolynomialTail

For a measurable sample space, a measure on that sample space, a real-valued random variable on that sample space, and a real threshold, the threshold tail integral is the integral over 1<t≤λ−11<t\leq\lambda^{-1} of the probability that the random variable is at most t−1t^{-1}.

Definition (Lean source)
parameters
Ω :
Type u_1
shared
P :
Measure Ω
U :
Ω → ℝ
lam :
ℝ
def
tailIntegral P U lam :
ℝ
given by
∫ t in Ioc 1 lam⁻¹, P.real {ω | U ω ≤ t⁻¹}
Causalean.Stat.PolynomialTail.tailIntegral · Causalean/Stat/PolynomialTail/LayerCakeReduction.lean:50
theorem invMomentJ_eq_one_add_tailIntegral reviewed
Causalean.Stat.PolynomialTail

Master layer-cake reduction. For a variable U that is measurable and almost surely strictly positive and at most 1, and a threshold λ that is positive and strictly below 1, the truncated inverse first moment J P U λ equals 1 plus the threshold tail integral tailIntegral P U λ:

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
lam :
ℝ
shared
IsProbabilityMeasure P
hsetup :
TailSetup P U
hlam_pos :
0 < lam
hlam_lt :
lam < 1
conclusion
invMomentJ P U lam = 1 + tailIntegral P U lam
Proof (Lean source)
theorem invMomentJ_eq_one_add_tailIntegral [IsProbabilityMeasure P] (hsetup : TailSetup P U) (hlam_pos : 0 < lam) (hlam_lt : lam < 1) : invMomentJ P U lam = 1 + tailIntegral P U lam := by have hU := hsetup.measurable -- Layer-cake on the J-integrand `f = (max U λ)⁻¹`, bounded by `M = λ⁻¹`. have hint : Integrable (fun ω => (max (U ω) lam)⁻¹) P := integrable_invMomentJ_integrand hsetup hlam_pos have hnn : 0 ≤ᵐ[P] fun ω => (max (U ω) lam)⁻¹ := Filter.Eventually.of_forall fun ω => (invMomentJ_integrand_mem hlam_pos (U ω)).1 have hbd : (fun ω => (max (U ω) lam)⁻¹) ≤ᵐ[P] fun _ => lam⁻¹ := Filter.Eventually.of_forall fun ω => (invMomentJ_integrand_mem hlam_pos (U ω)).2 rw [invMomentJ, hint.integral_eq_integral_Ioc_meas_le hnn hbd] have h1le : (1 : ℝ) ≤ lam⁻¹ := (one_le_inv₀ hlam_pos).mpr hlam_lt.le -- On the whole window `t ∈ (0, λ⁻¹]` the level set `{t ≤ (max U λ)⁻¹}` equals `{U ≤ t⁻¹}`. have hset : ∀ t : ℝ, 0 < t → t ≤ lam⁻¹ → {a | t ≤ (max (U a) lam)⁻¹} = {a | U a ≤ t⁻¹} := by intro t htpos htle have hlamt : lam ≤ t⁻¹ := (le_inv_comm₀ hlam_pos htpos).mpr htle ext a simp only [mem_setOf_eq] rw [le_inv_comm₀ htpos (lt_of_lt_of_le hlam_pos (le_max_right _ _)), max_le_iff] exact ⟨fun h => h.1, fun h => ⟨h, hlamt⟩⟩ have hcongr : EqOn (fun t => P.real {a | t ≤ (max (U a) lam)⁻¹}) (fun t => P.real {a | U a ≤ t⁻¹}) (Ioc 0 lam⁻¹) := by intro t ht simp only [hset t ht.1 ht.2] rw [setIntegral_congr_fun measurableSet_Ioc hcongr] -- Split `Ioc 0 λ⁻¹ = Ioc 0 1 ∪ Ioc 1 λ⁻¹`. have hdisj : Disjoint (Ioc (0 : ℝ) 1) (Ioc 1 lam⁻¹) := by rw [Set.disjoint_left] rintro x ⟨_, hx1⟩ ⟨hx2, _⟩ exact absurd hx2 (not_lt.mpr hx1) rw [← Set.Ioc_union_Ioc_eq_Ioc (by norm_num : (0 : ℝ) ≤ 1) h1le, setIntegral_union hdisj measurableSet_Ioc (integrableOn_tailIntegrand 0 1) (integrableOn_tailIntegrand 1 lam⁻¹)] rw [tailIntegral] congr 1 -- The `Ioc 0 1` part is the constant `1`. have hone : EqOn (fun t : ℝ => P.real {a | U a ≤ t⁻¹}) (fun _ => (1 : ℝ)) (Ioc 0 1) := by intro t ht have ht1 : (1 : ℝ) ≤ t⁻¹ := (one_le_inv₀ ht.1).mpr ht.2 have hfull : {a | U a ≤ t⁻¹} =ᵐ[P] (univ : Set Ω) := by filter_upwards [hsetup.le_one] with a ha exact eq_true (le_trans ha ht1) change P.real {a | U a ≤ t⁻¹} = 1 rw [measureReal_congr hfull, measureReal_def, measure_univ, ENNReal.toReal_one] rw [setIntegral_congr_fun measurableSet_Ioc hone] simp
Causalean.Stat.PolynomialTail.invMomentJ_eq_one_add_tailIntegral · Causalean/Stat/PolynomialTail/LayerCakeReduction.lean:91 · uses TailSetup , invMomentJ , tailIntegral
6 supporting declarations (lemmas, instances)
Moment­IBounds 7 core · 5 supporting This module proves the corresponding regime bounds for I P U lam = invMomentI P U lam = int U / (max U lam)^2. ★ invMomentI_bounds_lt★ invMomentI_bounds_eq★ invMomentI_bounds_gt★ invMomentJ_isTheta_lt★ invMomentI_isTheta_lt★ invMomentJ_isTheta_gt★ invMomentI_isTheta_gt

Bounds for the inverse second moment

This module proves the corresponding regime bounds for I P U lam = invMomentI P U lam = int U / (max U lam)^2. The upper side comes from the pointwise comparison invMomentI_le_invMomentJ, so the J bounds from MomentJBounds immediately control I.

The lower side is specific to I: invMomentI_ge_shell uses the annulus rho * lam < U <= lam, with rho = (cm / (2 * cp))^(1 / kappa), to extract a positive mass shell from the two-sided polynomial-tail assumption. The module then proves invMomentI_bounds_lt, invMomentI_bounds_eq, and invMomentI_bounds_gt for the three regimes, plus IsTheta corollaries invMomentJ_isTheta_lt, invMomentI_isTheta_lt, invMomentJ_isTheta_gt, and invMomentI_isTheta_gt as lam -> 0+.

theorem invMomentI_bounds_lt reviewed
Causalean.Stat.PolynomialTail

Regime 0 < κ < 1. Under the polynomial lower-tail hypothesis PolyTail P U κ t₀ cm cp with U measurable and almost surely in (0,1] and tail exponent strictly between 0 and 1, there exist constants 0 < a ≤ A such that the truncated inverse second moment I P U λ is squeezed between a·λ^{κ-1} and A·λ^{κ-1}, uniformly for every λ ∈ (0, t₀]. Lower: shell; upper: I ≤ J.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ1 :
κ < 1
conclusion
∃ a A : ℝ,
0 < a
a ≤ A
conclusion 1
lam :
ℝ
0 < lam
lam ≤ t₀
a * lam ^ (κ - 1) ≤ invMomentI P U lam
invMomentI P U lam ≤ A * lam ^ (κ - 1)
Proof (Lean source)
theorem invMomentI_bounds_lt [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ1 : κ < 1) : ∃ a A : ℝ, 0 < a ∧ a ≤ A ∧ ∀ lam : ℝ, 0 < lam → lam ≤ t₀ → a * lam ^ (κ - 1) ≤ invMomentI P U lam ∧ invMomentI P U lam ≤ A * lam ^ (κ - 1) := by obtain ⟨aJ, AJ, haJ, haAJ, hJ⟩ := invMomentJ_bounds_lt h hsetup hκ1 set aS : ℝ := (cm / 2) * (cm / (2 * cp)) ^ (1 / κ) with haS have haS_pos : 0 < aS := mul_pos (by linarith [h.cm_pos]) (Real.rpow_pos_of_pos (div_pos h.cm_pos (by linarith [h.cp_pos])) _) refine ⟨min aS AJ, AJ, lt_min haS_pos (lt_of_lt_of_le haJ haAJ), min_le_right _ _, fun lam hlp hll => ?_⟩ have hpow_nonneg : 0 ≤ lam ^ (κ - 1) := Real.rpow_nonneg hlp.le _ refine ⟨?_, le_trans (invMomentI_le_invMomentJ hsetup hlp) (hJ lam hlp hll).2⟩ calc min aS AJ * lam ^ (κ - 1) ≤ aS * lam ^ (κ - 1) := mul_le_mul_of_nonneg_right (min_le_left _ _) hpow_nonneg _ ≤ invMomentI P U lam := invMomentI_ge_shell h hsetup hlp hll
Causalean.Stat.PolynomialTail.invMomentI_bounds_lt · Causalean/Stat/PolynomialTail/MomentIBounds.lean:190 · uses PolyTail , TailSetup , invMomentI
theorem invMomentI_bounds_eq reviewed
Causalean.Stat.PolynomialTail

Regime κ = 1. Under the polynomial lower-tail hypothesis PolyTail P U κ t₀ cm cp with U measurable and almost surely in (0,1] and tail exponent exactly 1, there exist constants 0 < a ≤ A such that the truncated inverse second moment I P U λ is squeezed between a·log(1/λ) and A·log(1/λ) + A, uniformly for every λ ∈ (0, t₀]. Upper: I ≤ J; lower: I = J − (J−I) ≥ J − cp, uniformized with the constant shell floor.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ :
κ = 1
conclusion
∃ a A : ℝ,
0 < a
a ≤ A
conclusion 1
lam :
ℝ
0 < lam
lam ≤ t₀
a * log (1 / lam) ≤ invMomentI P U lam
invMomentI P U lam ≤ A * log (1 / lam) + A
Proof (Lean source)
theorem invMomentI_bounds_eq [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ : κ = 1) : ∃ a A : ℝ, 0 < a ∧ a ≤ A ∧ ∀ lam : ℝ, 0 < lam → lam ≤ t₀ → a * log (1 / lam) ≤ invMomentI P U lam ∧ invMomentI P U lam ≤ A * log (1 / lam) + A := by subst hκ obtain ⟨aJ, AJ, haJ, haAJ, hJ⟩ := invMomentJ_bounds_eq h hsetup rfl have hcp_pos := h.cp_pos have hpow0 : ∀ x : ℝ, x ^ ((1 : ℝ) - 1) = 1 := fun x => by rw [show (1 : ℝ) - 1 = 0 from by norm_num, Real.rpow_zero] set L0 : ℝ := log (1 / t₀) with hL0 have hL0_pos : 0 < L0 := by rw [hL0]; apply Real.log_pos; rw [one_div]; exact (one_lt_inv₀ h.t0_pos).mpr h.t0_lt_one set cS : ℝ := (cm / 2) * (cm / (2 * cp)) ^ (1 / (1 : ℝ)) with hcS have hcS_pos : 0 < cS := mul_pos (by linarith [h.cm_pos]) (Real.rpow_pos_of_pos (div_pos h.cm_pos (by linarith)) _) set Lstar : ℝ := 2 * cp / aJ + L0 with hLstar have hLstar_pos : 0 < Lstar := by have : 0 < 2 * cp / aJ := div_pos (by linarith) haJ linarith refine ⟨min (aJ / 2) (cS / Lstar), AJ, lt_min (by linarith) (div_pos hcS_pos hLstar_pos), le_trans (min_le_left _ _) (by linarith), fun lam hlp hll => ?_⟩ obtain ⟨hJlo, hJhi⟩ := hJ lam hlp hll have hrel := invMomentJ_sub_invMomentI_le h hsetup hlp hll rw [hpow0] at hrel have hsh := invMomentI_ge_shell h hsetup hlp hll rw [hpow0, mul_one] at hsh have hIle_J := invMomentI_le_invMomentJ hsetup hlp have hL : L0 ≤ log (1 / lam) := by rw [hL0] exact Real.log_le_log (one_div_pos.mpr h.t0_pos) (one_div_le_one_div_of_le hlp hll) set L := log (1 / lam) with hLdef have hL_pos : 0 < L := lt_of_lt_of_le hL0_pos hL refine ⟨?_, by linarith [hIle_J, hJhi]⟩ -- lower: min(aJ/2, cS/Lstar) · L ≤ I by_cases hLcase : L ≤ Lstar · have hstep : (cS / Lstar) * L ≤ cS := by rw [div_mul_eq_mul_div, div_le_iff₀ hLstar_pos]; nlinarith [hcS_pos, hLcase] have : min (aJ / 2) (cS / Lstar) * L ≤ (cS / Lstar) * L := mul_le_mul_of_nonneg_right (min_le_right _ _) hL_pos.le linarith [hsh] · push_neg at hLcase have haJL : 2 * cp < aJ * L := by have h' : 2 * cp / aJ < L := by linarith [hL0_pos] rw [div_lt_iff₀ haJ] at h'; nlinarith [h'] have : min (aJ / 2) (cS / Lstar) * L ≤ (aJ / 2) * L := mul_le_mul_of_nonneg_right (min_le_left _ _) hL_pos.le nlinarith [hJlo, hrel, haJL, this]
Causalean.Stat.PolynomialTail.invMomentI_bounds_eq · Causalean/Stat/PolynomialTail/MomentIBounds.lean:214 · uses PolyTail , TailSetup , invMomentI
theorem invMomentI_bounds_gt reviewed
Causalean.Stat.PolynomialTail

Regime κ > 1. Under the polynomial lower-tail hypothesis PolyTail P U κ t₀ cm cp with U measurable and almost surely in (0,1] and tail exponent strictly above 1, there exist constants 0 < a ≤ A such that the truncated inverse second moment I P U λ is bounded between a and A, uniformly for every λ ∈ (0, t₀]: the inverse second moment does not blow up. Lower: I is antitone, so I(λ) ≥ I(t₀) ≥ (shell at t₀), a positive constant; upper: I ≤ J.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ1 :
1 < κ
conclusion
∃ a A : ℝ,
0 < a
a ≤ A
conclusion 1
lam :
ℝ
0 < lam
lam ≤ t₀
a ≤ invMomentI P U lam
invMomentI P U lam ≤ A
Proof (Lean source)
theorem invMomentI_bounds_gt [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ1 : 1 < κ) : ∃ a A : ℝ, 0 < a ∧ a ≤ A ∧ ∀ lam : ℝ, 0 < lam → lam ≤ t₀ → a ≤ invMomentI P U lam ∧ invMomentI P U lam ≤ A := by obtain ⟨aJ, AJ, haJ, haAJ, hJ⟩ := invMomentJ_bounds_gt h hsetup hκ1 set aI : ℝ := (cm / 2) * (cm / (2 * cp)) ^ (1 / κ) * t₀ ^ (κ - 1) with haI have haI_pos : 0 < aI := mul_pos (mul_pos (by linarith [h.cm_pos]) (Real.rpow_pos_of_pos (div_pos h.cm_pos (by linarith [h.cp_pos])) _)) (Real.rpow_pos_of_pos h.t0_pos _) have haI_le : aI ≤ invMomentI P U t₀ := invMomentI_ge_shell h hsetup h.t0_pos le_rfl have haI_le_AJ : aI ≤ AJ := le_trans haI_le (le_trans (invMomentI_le_invMomentJ hsetup h.t0_pos) (hJ t₀ h.t0_pos le_rfl).2) refine ⟨aI, AJ, haI_pos, haI_le_AJ, fun lam hlp hll => ?_⟩ exact ⟨le_trans haI_le (invMomentI_antitone hsetup hlp hll), le_trans (invMomentI_le_invMomentJ hsetup hlp) (hJ lam hlp hll).2⟩
Causalean.Stat.PolynomialTail.invMomentI_bounds_gt · Causalean/Stat/PolynomialTail/MomentIBounds.lean:272 · uses PolyTail , TailSetup , invMomentI
theorem invMomentJ_isTheta_lt reviewed
Causalean.Stat.PolynomialTail

IsTheta for J (κ < 1). Under the polynomial lower-tail hypothesis with U measurable and almost surely in (0,1] and tail exponent strictly between 0 and 1, the truncated inverse first moment J P U λ is Θ(λ^{κ-1}) as λ → 0⁺.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ1 :
κ < 1
conclusion
(fun lam => invMomentJ P U lam) =Θ[𝓝[>] (0 : ℝ)] fun lam => lam ^ (κ - 1)
Proof (Lean source)
theorem invMomentJ_isTheta_lt [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ1 : κ < 1) : (fun lam => invMomentJ P U lam) =Θ[𝓝[>] (0 : ℝ)] fun lam => lam ^ (κ - 1) := by obtain ⟨a, A, ha, _, hbd⟩ := invMomentJ_bounds_lt h hsetup hκ1 exact isTheta_of_two_sided h.t0_pos ha (fun lam hlp _ => Real.rpow_pos_of_pos hlp _) (fun lam hlp hll => le_trans (mul_nonneg ha.le (Real.rpow_nonneg hlp.le _)) (hbd lam hlp hll).1) hbd
Causalean.Stat.PolynomialTail.invMomentJ_isTheta_lt · Causalean/Stat/PolynomialTail/MomentIBounds.lean:319 · uses PolyTail , TailSetup , invMomentJ
theorem invMomentI_isTheta_lt reviewed
Causalean.Stat.PolynomialTail

IsTheta for I (κ < 1). Under the polynomial lower-tail hypothesis with U measurable and almost surely in (0,1] and tail exponent strictly between 0 and 1, the truncated inverse second moment I P U λ is Θ(λ^{κ-1}) as λ → 0⁺.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ1 :
κ < 1
conclusion
(fun lam => invMomentI P U lam) =Θ[𝓝[>] (0 : ℝ)] fun lam => lam ^ (κ - 1)
Proof (Lean source)
theorem invMomentI_isTheta_lt [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ1 : κ < 1) : (fun lam => invMomentI P U lam) =Θ[𝓝[>] (0 : ℝ)] fun lam => lam ^ (κ - 1) := by obtain ⟨a, A, ha, _, hbd⟩ := invMomentI_bounds_lt h hsetup hκ1 exact isTheta_of_two_sided h.t0_pos ha (fun lam hlp _ => Real.rpow_pos_of_pos hlp _) (fun lam hlp hll => le_trans (mul_nonneg ha.le (Real.rpow_nonneg hlp.le _)) (hbd lam hlp hll).1) hbd
Causalean.Stat.PolynomialTail.invMomentI_isTheta_lt · Causalean/Stat/PolynomialTail/MomentIBounds.lean:331 · uses PolyTail , TailSetup , invMomentI
theorem invMomentJ_isTheta_gt reviewed
Causalean.Stat.PolynomialTail

IsTheta for J (κ > 1). Under the polynomial lower-tail hypothesis with U measurable and almost surely in (0,1] and tail exponent strictly above 1, the truncated inverse first moment J P U λ is Θ(1) — bounded — as λ → 0⁺.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ1 :
1 < κ
conclusion
(fun lam => invMomentJ P U lam) =Θ[𝓝[>] (0 : ℝ)] fun _ => (1 : ℝ)
Proof (Lean source)
theorem invMomentJ_isTheta_gt [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ1 : 1 < κ) : (fun lam => invMomentJ P U lam) =Θ[𝓝[>] (0 : ℝ)] fun _ => (1 : ℝ) := by obtain ⟨a, A, ha, _, hbd⟩ := invMomentJ_bounds_gt h hsetup hκ1 exact isTheta_of_two_sided h.t0_pos ha (fun _ _ _ => one_pos) (fun lam hlp hll => le_trans ha.le (hbd lam hlp hll).1) (fun lam hlp hll => by simpa using hbd lam hlp hll)
Causalean.Stat.PolynomialTail.invMomentJ_isTheta_gt · Causalean/Stat/PolynomialTail/MomentIBounds.lean:343 · uses PolyTail , TailSetup , invMomentJ
theorem invMomentI_isTheta_gt reviewed
Causalean.Stat.PolynomialTail

IsTheta for I (κ > 1). Under the polynomial lower-tail hypothesis with U measurable and almost surely in (0,1] and tail exponent strictly above 1, the truncated inverse second moment I P U λ is Θ(1) — bounded — as λ → 0⁺.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ1 :
1 < κ
conclusion
(fun lam => invMomentI P U lam) =Θ[𝓝[>] (0 : ℝ)] fun _ => (1 : ℝ)
Proof (Lean source)
theorem invMomentI_isTheta_gt [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ1 : 1 < κ) : (fun lam => invMomentI P U lam) =Θ[𝓝[>] (0 : ℝ)] fun _ => (1 : ℝ) := by obtain ⟨a, A, ha, _, hbd⟩ := invMomentI_bounds_gt h hsetup hκ1 exact isTheta_of_two_sided h.t0_pos ha (fun _ _ _ => one_pos) (fun lam hlp hll => le_trans ha.le (hbd lam hlp hll).1) (fun lam hlp hll => by simpa using hbd lam hlp hll)
Causalean.Stat.PolynomialTail.invMomentI_isTheta_gt · Causalean/Stat/PolynomialTail/MomentIBounds.lean:355 · uses PolyTail , TailSetup , invMomentI
5 supporting declarations (lemmas, instances)
  • invMomentI_le_invMomentJ theorem — I ≤ J. Pointwise U/(max U λ)² ≤ (max U λ)⁻¹ (since U ≤ max U λ).
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    Ω → ℝ
    shared
    lam :
    ℝ
    shared
    IsProbabilityMeasure P
    hsetup :
    TailSetup P U
    hlam_pos :
    0 < lam
    conclusion
    invMomentI P U lam ≤ invMomentJ P U lam
    Proof (Lean source)
    theorem invMomentI_le_invMomentJ [IsProbabilityMeasure P] (hsetup : TailSetup P U) (hlam_pos : 0 < lam) : invMomentI P U lam ≤ invMomentJ P U lam := by rw [invMomentI, invMomentJ] refine integral_mono_ae (integrable_invMomentI_integrand hsetup hlam_pos) (integrable_invMomentJ_integrand hsetup hlam_pos) ?_ filter_upwards [hsetup.pos] with ω hUpos have hm : 0 < max (U ω) lam := lt_of_lt_of_le hlam_pos (le_max_right _ _) have hUm : U ω / max (U ω) lam ≤ 1 := by rw [div_le_one hm]; exact le_max_left _ _ calc U ω / (max (U ω) lam) ^ 2 = (U ω / max (U ω) lam) * (max (U ω) lam)⁻¹ := by rw [sq, ← div_div, div_eq_mul_inv] _ ≤ 1 * (max (U ω) lam)⁻¹ := mul_le_mul_of_nonneg_right hUm (inv_nonneg.mpr hm.le) _ = (max (U ω) lam)⁻¹ := one_mul _
    Causalean.Stat.PolynomialTail.invMomentI_le_invMomentJ · Causalean/Stat/PolynomialTail/MomentIBounds.lean:45
  • invMomentJ_sub_invMomentI_le theorem — J − I is controlled by the tail mass. J P U λ − I P U λ ≤ cp·λ^{κ-1}. Pointwise the gap equals wλ/(max U λ) ≤ λ⁻¹·wλ, and ∫ wλ ≤ P{U<λ} ≤ cp·λᵏ.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    Ω → ℝ
    shared
    κ :
    ℝ
    shared
    t₀ :
    ℝ
    shared
    cm :
    ℝ
    shared
    cp :
    ℝ
    shared
    lam :
    ℝ
    shared
    IsProbabilityMeasure P
    h :
    PolyTail P U κ t₀ cm cp
    hsetup :
    TailSetup P U
    hlam_pos :
    0 < lam
    hlam_le :
    lam ≤ t₀
    conclusion
    invMomentJ P U lam - invMomentI P U lam ≤ cp * lam ^ (κ - 1)
    Proof (Lean source)
    theorem invMomentJ_sub_invMomentI_le [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hlam_pos : 0 < lam) (hlam_le : lam ≤ t₀) : invMomentJ P U lam - invMomentI P U lam ≤ cp * lam ^ (κ - 1) := by have hJint := integrable_invMomentJ_integrand hsetup hlam_pos have hIint := integrable_invMomentI_integrand hsetup hlam_pos have hWint := integrable_trimWeight hsetup hlam_pos have hsmeas : MeasurableSet {ω | U ω < lam} := hsetup.measurable measurableSet_Iio have hptbound : ∀ᵐ ω ∂P, (max (U ω) lam)⁻¹ - U ω / (max (U ω) lam) ^ 2 ≤ lam⁻¹ * trimWeight U lam ω := by filter_upwards [hsetup.pos] with ω hUpos have hm : 0 < max (U ω) lam := lt_of_lt_of_le hlam_pos (le_max_right _ _) have heq : (max (U ω) lam)⁻¹ - U ω / (max (U ω) lam) ^ 2 = trimWeight U lam ω / max (U ω) lam := by simp only [trimWeight]; field_simp rw [heq, div_eq_mul_inv, mul_comm] exact mul_le_mul_of_nonneg_right (inv_anti₀ hlam_pos (le_max_right _ _)) (trimWeight_mem hlam_pos hUpos).1 have hWmass : ∫ ω, trimWeight U lam ω ∂P ≤ P.real {ω | U ω < lam} := by have hind : P.real {ω | U ω < lam} = ∫ ω, indicator {ω | U ω < lam} (fun _ => (1 : ℝ)) ω ∂P := by rw [integral_indicator hsmeas, setIntegral_const, smul_eq_mul, mul_one] rw [hind] refine integral_mono_ae hWint ((integrable_const (1 : ℝ)).indicator hsmeas) ?_ filter_upwards [hsetup.pos] with ω hUpos by_cases hω : U ω < lam · rw [Set.indicator_of_mem (show ω ∈ {ω | U ω < lam} from hω)] exact (trimWeight_mem hlam_pos hUpos).2 · have hw0 : trimWeight U lam ω = 0 := by simp only [trimWeight, max_eq_left (not_lt.mp hω), div_self (ne_of_gt hUpos), sub_self] rw [hw0, Set.indicator_of_notMem (show ω ∉ {ω | U ω < lam} from hω)] rw [invMomentJ, invMomentI, ← integral_sub hJint hIint] calc ∫ ω, ((max (U ω) lam)⁻¹ - U ω / (max (U ω) lam) ^ 2) ∂P ≤ ∫ ω, lam⁻¹ * trimWeight U lam ω ∂P := integral_mono_ae (hJint.sub hIint) (hWint.const_mul _) hptbound _ = lam⁻¹ * ∫ ω, trimWeight U lam ω ∂P := integral_const_mul _ _ _ ≤ lam⁻¹ * (cp * lam ^ κ) := by have h1 : (0 : ℝ) ≤ lam⁻¹ := by positivity exact mul_le_mul_of_nonneg_left (le_trans hWmass (measureReal_lt_le h hlam_pos hlam_le)) h1 _ = cp * lam ^ (κ - 1) := by rw [Real.rpow_sub hlam_pos, Real.rpow_one]; field_simp
    Causalean.Stat.PolynomialTail.invMomentJ_sub_invMomentI_le · Causalean/Stat/PolynomialTail/MomentIBounds.lean:61
  • invMomentI_antitone theorem — I is antitone in λ. As λ decreases, max U λ decreases, so the integrand U/(max U λ)² increases. Hence I P U λ₂ ≤ I P U λ₁ when λ₁ ≤ λ₂.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    Ω → ℝ
    shared
    IsProbabilityMeasure P
    hsetup :
    TailSetup P U
    l1 l2 :
    ℝ
    hl1 :
    0 < l1
    hl12 :
    l1 ≤ l2
    conclusion
    invMomentI P U l2 ≤ invMomentI P U l1
    Proof (Lean source)
    theorem invMomentI_antitone [IsProbabilityMeasure P] (hsetup : TailSetup P U) {l1 l2 : ℝ} (hl1 : 0 < l1) (hl12 : l1 ≤ l2) : invMomentI P U l2 ≤ invMomentI P U l1 := by rw [invMomentI, invMomentI] refine integral_mono_ae (integrable_invMomentI_integrand hsetup (lt_of_lt_of_le hl1 hl12)) (integrable_invMomentI_integrand hsetup hl1) ?_ filter_upwards [hsetup.pos] with ω hUpos have hm1 : 0 < max (U ω) l1 := lt_of_lt_of_le hl1 (le_max_right _ _) have hmono : max (U ω) l1 ≤ max (U ω) l2 := max_le_max le_rfl hl12 gcongr
    Causalean.Stat.PolynomialTail.invMomentI_antitone · Causalean/Stat/PolynomialTail/MomentIBounds.lean:103
  • invMomentI_ge_shell theorem — Shell lower bound on I. (ρ·cm/2)·λ^{κ-1} ≤ I P U λ, with ρ = (cm/(2cp))^{1/κ}. Valid for every λ ∈ (0, t₀].
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    Ω → ℝ
    shared
    κ :
    ℝ
    shared
    t₀ :
    ℝ
    shared
    cm :
    ℝ
    shared
    cp :
    ℝ
    shared
    lam :
    ℝ
    shared
    IsProbabilityMeasure P
    h :
    PolyTail P U κ t₀ cm cp
    hsetup :
    TailSetup P U
    hlam_pos :
    0 < lam
    hlam_le :
    lam ≤ t₀
    conclusion
    (cm / 2) * (cm / (2 * cp)) ^ (1 / κ) * lam ^ (κ - 1) ≤ invMomentI P U lam
    Proof (Lean source)
    theorem invMomentI_ge_shell [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hlam_pos : 0 < lam) (hlam_le : lam ≤ t₀) : (cm / 2) * (cm / (2 * cp)) ^ (1 / κ) * lam ^ (κ - 1) ≤ invMomentI P U lam := by have hcp_pos := h.cp_pos have hκ := h.kappa_pos set ρ : ℝ := (cm / (2 * cp)) ^ (1 / κ) with hρ have hbase_pos : 0 < cm / (2 * cp) := div_pos h.cm_pos (by linarith) have hbase_lt_one : cm / (2 * cp) < 1 := by rw [div_lt_one (by linarith)]; nlinarith [h.cm_lt_cp, h.cm_pos] have hρ_pos : 0 < ρ := Real.rpow_pos_of_pos hbase_pos _ have hρκ : ρ ^ κ = cm / (2 * cp) := by rw [hρ, ← Real.rpow_mul hbase_pos.le, one_div, inv_mul_cancel₀ (ne_of_gt hκ), Real.rpow_one] have hρ_lt_one : ρ < 1 := by by_contra hc push_neg at hc have := Real.one_le_rpow hc hκ.le rw [hρκ] at this; linarith have hrL_pos : 0 < ρ * lam := mul_pos hρ_pos hlam_pos have hrL_lt : ρ * lam < lam := by nlinarith [hlam_pos] have hrL_le_t0 : ρ * lam ≤ t₀ := le_of_lt (lt_of_lt_of_le hrL_lt hlam_le) -- shell set and its mass set S : Set Ω := {ω | ρ * lam < U ω ∧ U ω ≤ lam} with hS have hSmeas : MeasurableSet S := (hsetup.measurable measurableSet_Ioi).inter (hsetup.measurable measurableSet_Iic) have hSsub : S = {ω | U ω ≤ lam} \ {ω | U ω ≤ ρ * lam} := by ext ω; simp only [hS, mem_setOf_eq, mem_diff, not_le]; tauto have hmass : (cm / 2) * lam ^ κ ≤ P.real S := by have hsub : {ω | U ω ≤ ρ * lam} ⊆ {ω | U ω ≤ lam} := fun ω (hω : U ω ≤ ρ * lam) => le_trans hω hrL_lt.le rw [hSsub, measureReal_diff hsub (hsetup.measurable measurableSet_Iic) (measure_ne_top P _)] have hlo := h.tail_lower lam hlam_pos hlam_le have hhi := h.tail_upper (ρ * lam) hrL_pos hrL_le_t0 have hrLk : (ρ * lam) ^ κ = (cm / (2 * cp)) * lam ^ κ := by rw [Real.mul_rpow hρ_pos.le hlam_pos.le, hρκ] rw [hrLk] at hhi have hsimp : cp * (cm / (2 * cp) * lam ^ κ) = (cm / 2) * lam ^ κ := by field_simp rw [hsimp] at hhi linarith -- pointwise: `(ρ/λ)·𝟙_S ≤ integrand` have hsmeas_int : Integrable (fun ω => (ρ / lam) * indicator S (fun _ => (1 : ℝ)) ω) P := by fun_prop have hpt : ∀ᵐ ω ∂P, (ρ / lam) * indicator S (fun _ => (1 : ℝ)) ω ≤ U ω / (max (U ω) lam) ^ 2 := by filter_upwards [hsetup.pos] with ω hUpos by_cases hω : ω ∈ S · rw [Set.indicator_of_mem hω, mul_one, max_eq_right hω.2, show ρ / lam = ρ * lam / lam ^ 2 from by rw [sq]; exact (mul_div_mul_right ρ lam hlam_pos.ne').symm] exact (div_le_div_iff_of_pos_right (by positivity)).mpr hω.1.le · rw [Set.indicator_of_notMem hω, mul_zero] positivity -- assemble have hint := integrable_invMomentI_integrand hsetup hlam_pos calc (cm / 2) * ρ * lam ^ (κ - 1) = (ρ / lam) * ((cm / 2) * lam ^ κ) := by rw [Real.rpow_sub hlam_pos, Real.rpow_one]; field_simp _ ≤ (ρ / lam) * P.real S := mul_le_mul_of_nonneg_left hmass (div_nonneg hρ_pos.le hlam_pos.le) _ = ∫ ω, (ρ / lam) * indicator S (fun _ => (1 : ℝ)) ω ∂P := by rw [integral_const_mul, integral_indicator hSmeas, setIntegral_const, smul_eq_mul, mul_one] _ ≤ invMomentI P U lam := by rw [invMomentI]; exact integral_mono_ae hsmeas_int hint hpt
    Causalean.Stat.PolynomialTail.invMomentI_ge_shell · Causalean/Stat/PolynomialTail/MomentIBounds.lean:118
  • isTheta_of_two_sided theorem — Generic two-sided-bound ⟹ IsTheta packager on 𝓝[>] 0.
    hypotheses
    f g :
    ℝ → ℝ
    t₀ a A :
    ℝ
    ht0 :
    0 < t₀
    ha :
    0 < a
    hgpos :
    ∀ lam : ℝ
    if
    0 < lam
    and
    lam ≤ t₀
    then
    0 < g lam
    hfnn :
    ∀ lam : ℝ
    if
    0 < lam
    and
    lam ≤ t₀
    then
    0 ≤ f lam
    hbd :
    ∀ lam : ℝ
    if
    0 < lam
    and
    lam ≤ t₀
    then
    a * g lam ≤ f lam ∧ f lam ≤ A * g lam
    conclusion
    f =Θ[𝓝[>] (0 : ℝ)] g
    Proof (Lean source)
    theorem isTheta_of_two_sided {f g : ℝ → ℝ} {t₀ a A : ℝ} (ht0 : 0 < t₀) (ha : 0 < a) (hgpos : ∀ lam : ℝ, 0 < lam → lam ≤ t₀ → 0 < g lam) (hfnn : ∀ lam : ℝ, 0 < lam → lam ≤ t₀ → 0 ≤ f lam) (hbd : ∀ lam : ℝ, 0 < lam → lam ≤ t₀ → a * g lam ≤ f lam ∧ f lam ≤ A * g lam) : f =Θ[𝓝[>] (0 : ℝ)] g := by have hev : ∀ᶠ lam in 𝓝[>] (0 : ℝ), 0 < lam ∧ lam ≤ t₀ := by filter_upwards [self_mem_nhdsWithin, nhdsWithin_le_nhds (Iio_mem_nhds ht0)] with lam h1 h2 using ⟨h1, le_of_lt h2⟩ refine ⟨?_, ?_⟩ · rw [Asymptotics.isBigO_iff] refine ⟨A, hev.mono fun lam ⟨hlp, hll⟩ => ?_⟩ rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (hfnn lam hlp hll), abs_of_nonneg (hgpos lam hlp hll).le] exact (hbd lam hlp hll).2 · rw [Asymptotics.isBigO_iff] refine ⟨1 / a, hev.mono fun lam ⟨hlp, hll⟩ => ?_⟩ rw [Real.norm_eq_abs, Real.norm_eq_abs, abs_of_nonneg (hgpos lam hlp hll).le, abs_of_nonneg (hfnn lam hlp hll), one_div, inv_mul_eq_div, le_div_iff₀ ha, mul_comm] exact (hbd lam hlp hll).1
    Causalean.Stat.PolynomialTail.isTheta_of_two_sided · Causalean/Stat/PolynomialTail/MomentIBounds.lean:298
Moment­JBounds 3 core · 2 supporting This module combines the exact identity invMomentJ_eq_one_add_tailIntegral, the tail-integral sandwich from TailIntegralBounds, and the power-integral evaluations to prove uniform bounds for J P U lam = invMomentJ P U la ★ invMomentJ_bounds_lt★ invMomentJ_bounds_eq★ invMomentJ_bounds_gt

Three-regime bounds for the inverse first moment

This module combines the exact identity invMomentJ_eq_one_add_tailIntegral, the tail-integral sandwich from TailIntegralBounds, and the power-integral evaluations to prove uniform bounds for J P U lam = invMomentJ P U lam on lam in (0, t0].

The helper theorems powInt_ne_one and powInt_eq_one rewrite the comparison integral over (t0^(-1), lam^(-1)] into either a power expression or a logarithm. The main public bounds are invMomentJ_bounds_lt for 0 < kappa < 1, invMomentJ_bounds_eq for kappa = 1, and invMomentJ_bounds_gt for 1 < kappa, giving respectively power blow-up, logarithmic growth, and bounded inverse-moment behavior with constants depending only on the polynomial-tail parameters.

theorem invMomentJ_bounds_lt reviewed
Causalean.Stat.PolynomialTail

Regime 0 < κ < 1. Under the polynomial lower-tail hypothesis PolyTail P U κ t₀ cm cp with U measurable and almost surely in (0,1] and tail exponent strictly between 0 and 1, there exist constants 0 < a ≤ A, depending only on κ, cm, cp, t₀, such that the truncated inverse first moment J P U λ is squeezed between a·λ^{κ-1} and A·λ^{κ-1}, uniformly for every λ ∈ (0, t₀].

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ1 :
κ < 1
conclusion
∃ a A : ℝ,
0 < a
a ≤ A
conclusion 1
lam :
ℝ
0 < lam
lam ≤ t₀
a * lam ^ (κ - 1) ≤ invMomentJ P U lam
invMomentJ P U lam ≤ A * lam ^ (κ - 1)
Proof (Lean source)
theorem invMomentJ_bounds_lt [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ1 : κ < 1) : ∃ a A : ℝ, 0 < a ∧ a ≤ A ∧ ∀ lam : ℝ, 0 < lam → lam ≤ t₀ → a * lam ^ (κ - 1) ≤ invMomentJ P U lam ∧ invMomentJ P U lam ≤ A * lam ^ (κ - 1) := by have hone_sub : 0 < 1 - κ := by linarith set A1 : ℝ := cm / (1 - κ) with hA1 have hA1_pos : 0 < A1 := div_pos h.cm_pos hone_sub set a : ℝ := min A1 (t₀ ^ (1 - κ)) with ha_def set A : ℝ := t₀⁻¹ + cp / (1 - κ) with hA_def have ht0_pos := h.t0_pos have hBcoef_pos : 0 < cp / (1 - κ) := div_pos h.cp_pos hone_sub have ha_pos : 0 < a := lt_min hA1_pos (Real.rpow_pos_of_pos ht0_pos _) have hA_pos : 0 < A := by positivity have hcm_cp : cm / (1 - κ) ≤ cp / (1 - κ) := by gcongr; exact h.cm_lt_cp.le have ha_le_A : a ≤ A := le_trans (min_le_left _ _) (by simp only [hA1, hA_def]; linarith [inv_pos.mpr ht0_pos, hcm_cp]) refine ⟨a, A, ha_pos, ha_le_A, fun lam hlam_pos hlam_le => ?_⟩ set M : ℝ := lam ^ (κ - 1) with hM set M0 : ℝ := t₀ ^ (κ - 1) with hM0 have hM0_nonneg : 0 ≤ M0 := Real.rpow_nonneg ht0_pos.le _ have hlam_lt_one : lam < 1 := lt_of_le_of_lt hlam_le h.t0_lt_one have hM_ge_one : 1 ≤ M := le_of_eq_of_le (Real.one_rpow _).symm (Real.rpow_le_rpow_of_nonpos hlam_pos hlam_lt_one.le (by linarith)) have hM0_le_M : M0 ≤ M := Real.rpow_le_rpow_of_nonpos hlam_pos hlam_le (by linarith) have hPow := powInt_ne_one h (ne_of_lt hκ1) hlam_pos hlam_le have hJ : invMomentJ P U lam = 1 + tailIntegral P U lam := invMomentJ_eq_one_add_tailIntegral hsetup hlam_pos hlam_lt_one have hTle := tailIntegral_le h hlam_pos hlam_le have hTge := tailIntegral_ge h hlam_pos hlam_le rw [hPow] at hTle hTge -- cm·PowInt = A1·(M − M0), cp·PowInt = (cp/(1−κ))·(M − M0) have hcmPow : cm * ((M - M0) / (1 - κ)) = A1 * (M - M0) := by rw [hA1]; ring have hcpPow : cp * ((M - M0) / (1 - κ)) = (cp / (1 - κ)) * (M - M0) := by ring rw [hcmPow] at hTge rw [hcpPow] at hTle constructor · -- lower: a·M ≤ J have h_aM0_le_1 : a * M0 ≤ 1 := by have hmul : t₀ ^ (1 - κ) * M0 = 1 := by rw [hM0, ← Real.rpow_add ht0_pos, show (1 - κ) + (κ - 1) = 0 from by ring, Real.rpow_zero] calc a * M0 ≤ t₀ ^ (1 - κ) * M0 := mul_le_mul_of_nonneg_right (min_le_right _ _) hM0_nonneg _ = 1 := hmul have hprod : 0 ≤ (A1 - a) * (M - M0) := mul_nonneg (by linarith [min_le_left A1 (t₀ ^ (1 - κ))]) (by linarith) nlinarith [hJ, hTge, hprod, h_aM0_le_1] · -- upper: J ≤ A·M have h1 : 0 ≤ t₀⁻¹ * (M - 1) := mul_nonneg (inv_pos.mpr ht0_pos).le (by linarith) have h2 : 0 ≤ (cp / (1 - κ)) * M0 := mul_nonneg hBcoef_pos.le hM0_nonneg nlinarith [hJ, hTle, h1, h2]
Causalean.Stat.PolynomialTail.invMomentJ_bounds_lt · Causalean/Stat/PolynomialTail/MomentJBounds.lean:65 · uses PolyTail , TailSetup , invMomentJ
theorem invMomentJ_bounds_eq reviewed
Causalean.Stat.PolynomialTail

Regime κ = 1. Under the polynomial lower-tail hypothesis PolyTail P U κ t₀ cm cp with U measurable and almost surely in (0,1] and tail exponent exactly 1, there exist constants 0 < a ≤ A such that the truncated inverse first moment J P U λ is squeezed between a·log(1/λ) and A·log(1/λ) + A, uniformly for every λ ∈ (0, t₀].

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ :
κ = 1
conclusion
∃ a A : ℝ,
0 < a
a ≤ A
conclusion 1
lam :
ℝ
0 < lam
lam ≤ t₀
a * log (1 / lam) ≤ invMomentJ P U lam
invMomentJ P U lam ≤ A * log (1 / lam) + A
Proof (Lean source)
theorem invMomentJ_bounds_eq [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ : κ = 1) : ∃ a A : ℝ, 0 < a ∧ a ≤ A ∧ ∀ lam : ℝ, 0 < lam → lam ≤ t₀ → a * log (1 / lam) ≤ invMomentJ P U lam ∧ invMomentJ P U lam ≤ A * log (1 / lam) + A := by have ht0_pos := h.t0_pos set L0 : ℝ := log (1 / t₀) with hL0 have hL0_pos : 0 < L0 := by rw [hL0]; apply Real.log_pos; rw [one_div]; exact (one_lt_inv₀ ht0_pos).mpr h.t0_lt_one set a : ℝ := min cm (1 / L0) with ha_def set A : ℝ := t₀⁻¹ + cp with hA_def have ha_pos : 0 < a := lt_min h.cm_pos (by positivity) have ha_le_A : a ≤ A := le_trans (min_le_left _ _) (by simp only [hA_def]; linarith [inv_pos.mpr ht0_pos, h.cm_lt_cp]) refine ⟨a, A, ha_pos, ha_le_A, fun lam hlam_pos hlam_le => ?_⟩ have hlam_lt_one : lam < 1 := lt_of_le_of_lt hlam_le h.t0_lt_one have hL_ge_L0 : L0 ≤ log (1 / lam) := by rw [hL0] exact Real.log_le_log (by positivity) (one_div_le_one_div_of_le hlam_pos hlam_le) have hL_pos : 0 < log (1 / lam) := lt_of_lt_of_le hL0_pos hL_ge_L0 have hPow := powInt_eq_one h hκ hlam_pos hlam_le rw [← hL0] at hPow have hJ := invMomentJ_eq_one_add_tailIntegral hsetup hlam_pos hlam_lt_one have hTle := tailIntegral_le h hlam_pos hlam_le have hTge := tailIntegral_ge h hlam_pos hlam_le rw [hPow] at hTle hTge have h_aL0 : a * L0 ≤ 1 := by calc a * L0 ≤ (1 / L0) * L0 := mul_le_mul_of_nonneg_right (min_le_right _ _) hL0_pos.le _ = 1 := one_div_mul_cancel (ne_of_gt hL0_pos) constructor · -- lower have hprod : 0 ≤ (cm - a) * (log (1 / lam) - L0) := mul_nonneg (by linarith [min_le_left cm (1 / L0)]) (by linarith) nlinarith [hJ, hTge, hprod, h_aL0] · -- upper have h1 : 0 ≤ t₀⁻¹ * log (1 / lam) := mul_nonneg (inv_pos.mpr ht0_pos).le hL_pos.le have h2 : 0 ≤ cp * L0 := mul_nonneg h.cp_pos.le hL0_pos.le nlinarith [hJ, hTle, h1, h2]
Causalean.Stat.PolynomialTail.invMomentJ_bounds_eq · Causalean/Stat/PolynomialTail/MomentJBounds.lean:126 · uses PolyTail , TailSetup , invMomentJ
theorem invMomentJ_bounds_gt reviewed
Causalean.Stat.PolynomialTail

Regime κ > 1. Under the polynomial lower-tail hypothesis PolyTail P U κ t₀ cm cp with U measurable and almost surely in (0,1] and tail exponent strictly above 1, there exist constants 0 < a ≤ A such that the truncated inverse first moment J P U λ is bounded between a and A, uniformly for every λ ∈ (0, t₀]: the inverse first moment does not blow up.

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hκ1 :
1 < κ
conclusion
∃ a A : ℝ,
0 < a
a ≤ A
conclusion 1
lam :
ℝ
0 < lam
lam ≤ t₀
a ≤ invMomentJ P U lam
invMomentJ P U lam ≤ A
Proof (Lean source)
theorem invMomentJ_bounds_gt [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hκ1 : 1 < κ) : ∃ a A : ℝ, 0 < a ∧ a ≤ A ∧ ∀ lam : ℝ, 0 < lam → lam ≤ t₀ → a ≤ invMomentJ P U lam ∧ invMomentJ P U lam ≤ A := by have ht0_pos := h.t0_pos have hκm1_pos : 0 < κ - 1 := by linarith set A : ℝ := t₀⁻¹ + cp * t₀ ^ (κ - 1) / (κ - 1) with hA_def have hA_one : (1 : ℝ) ≤ A := by rw [hA_def] have h1 : (1 : ℝ) ≤ t₀⁻¹ := (one_le_inv₀ ht0_pos).mpr h.t0_lt_one.le have h2 : 0 ≤ cp * t₀ ^ (κ - 1) / (κ - 1) := div_nonneg (mul_nonneg h.cp_pos.le (Real.rpow_nonneg ht0_pos.le _)) hκm1_pos.le linarith refine ⟨1, A, one_pos, hA_one, fun lam hlam_pos hlam_le => ?_⟩ have hlam_lt_one : lam < 1 := lt_of_le_of_lt hlam_le h.t0_lt_one have hPow := powInt_ne_one h (by linarith : κ ≠ 1) hlam_pos hlam_le have hJ := invMomentJ_eq_one_add_tailIntegral hsetup hlam_pos hlam_lt_one have hTle := tailIntegral_le h hlam_pos hlam_le have hTnn : (0 : ℝ) ≤ tailIntegral P U lam := tailIntegral_nonneg rw [hPow] at hTle set M : ℝ := lam ^ (κ - 1) with hM set M0 : ℝ := t₀ ^ (κ - 1) with hM0 have hM_nonneg : 0 ≤ M := Real.rpow_nonneg hlam_pos.le _ have hM0_nonneg : 0 ≤ M0 := Real.rpow_nonneg ht0_pos.le _ have hM_le_M0 : M ≤ M0 := Real.rpow_le_rpow hlam_pos.le hlam_le hκm1_pos.le constructor · rw [hJ]; linarith [hTnn] · -- upper: rewrite PowInt = (M0 - M)/(κ-1) ≤ M0/(κ-1) have heq : (M - M0) / (1 - κ) = (M0 - M) / (κ - 1) := by rw [div_eq_div_iff (ne_of_lt (show (1 : ℝ) - κ < 0 by linarith)) (ne_of_gt hκm1_pos)] ring have hPI_bd : cp * ((M0 - M) / (κ - 1)) ≤ cp * (M0 / (κ - 1)) := mul_le_mul_of_nonneg_left (div_le_div_of_nonneg_right (by linarith [hM_nonneg]) hκm1_pos.le) h.cp_pos.le have hassoc : cp * (M0 / (κ - 1)) = cp * M0 / (κ - 1) := by rw [mul_div_assoc] rw [heq] at hTle rw [hJ, hA_def] linarith [hTle, hPI_bd, hassoc]
Causalean.Stat.PolynomialTail.invMomentJ_bounds_gt · Causalean/Stat/PolynomialTail/MomentJBounds.lean:173 · uses PolyTail , TailSetup , invMomentJ
2 supporting declarations (lemmas, instances)
  • powInt_ne_one theorem — PowInt = (λ^{κ-1} − t₀^{κ-1})/(1−κ) when κ ≠ 1.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    Ω → ℝ
    shared
    κ :
    ℝ
    shared
    t₀ :
    ℝ
    shared
    cm :
    ℝ
    shared
    cp :
    ℝ
    shared
    lam :
    ℝ
    shared
    h :
    PolyTail P U κ t₀ cm cp
    hκ :
    κ ≠ 1
    hlam_pos :
    0 < lam
    hlam_le :
    lam ≤ t₀
    conclusion
    ∫ t in Ioc t₀⁻¹ lam⁻¹, t ^ (-κ) = (lam ^ (κ - 1) - t₀ ^ (κ - 1)) / (1 - κ)
    Proof (Lean source)
    theorem powInt_ne_one (h : PolyTail P U κ t₀ cm cp) (hκ : κ ≠ 1) (hlam_pos : 0 < lam) (hlam_le : lam ≤ t₀) : ∫ t in Ioc t₀⁻¹ lam⁻¹, t ^ (-κ) = (lam ^ (κ - 1) - t₀ ^ (κ - 1)) / (1 - κ) := by rw [integral_rpow_neg_Ioc hκ (inv_pos.mpr h.t0_pos) ((inv_le_inv₀ h.t0_pos hlam_pos).mpr hlam_le), inv_rpow_eq_rpow_neg hlam_pos (1 - κ), inv_rpow_eq_rpow_neg h.t0_pos (1 - κ)] simp only [neg_sub]
    Causalean.Stat.PolynomialTail.powInt_ne_one · Causalean/Stat/PolynomialTail/MomentJBounds.lean:46
  • powInt_eq_one theorem — PowInt = log(1/λ) − log(1/t₀) when κ = 1.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    Ω → ℝ
    shared
    κ :
    ℝ
    shared
    t₀ :
    ℝ
    shared
    cm :
    ℝ
    shared
    cp :
    ℝ
    shared
    lam :
    ℝ
    shared
    h :
    PolyTail P U κ t₀ cm cp
    hκ :
    κ = 1
    hlam_pos :
    0 < lam
    hlam_le :
    lam ≤ t₀
    conclusion
    ∫ t in Ioc t₀⁻¹ lam⁻¹, t ^ (-κ) = log (1 / lam) - log (1 / t₀)
    Proof (Lean source)
    theorem powInt_eq_one (h : PolyTail P U κ t₀ cm cp) (hκ : κ = 1) (hlam_pos : 0 < lam) (hlam_le : lam ≤ t₀) : ∫ t in Ioc t₀⁻¹ lam⁻¹, t ^ (-κ) = log (1 / lam) - log (1 / t₀) := by subst hκ rw [integral_inv_neg_Ioc (inv_pos.mpr h.t0_pos) ((inv_le_inv₀ h.t0_pos hlam_pos).mpr hlam_le), one_div, one_div]
    Causalean.Stat.PolynomialTail.powInt_eq_one · Causalean/Stat/PolynomialTail/MomentJBounds.lean:55
Power­Integral 1 core · 2 supporting This module evaluates the deterministic interval integrals that appear after the polynomial-tail layer-cake reduction. ★ integral_rpow_neg_Ioc

Power-law interval integrals

This module evaluates the deterministic interval integrals that appear after the polynomial-tail layer-cake reduction. The helper zero_notMem_uIcc supplies the positivity side condition needed by intervalIntegral on a window 0 < a <= b.

The two public evaluations are integral_rpow_neg_Ioc, for the non-logarithmic case kappa != 1, and integral_inv_neg_Ioc, for the boundary case kappa = 1. Together they convert the threshold integral over (t0^(-1), lam^(-1)] into the lam^(kappa - 1) / log (1 / lam) alternatives used by the J and I moment bounds.

theorem integral_rpow_neg_Ioc reviewed
Causalean.Stat.PolynomialTail

Power integral, κ ≠ 1. If the exponent κ is not equal to 1, a is positive, and a is at most b, then the interval integral of t ↦ t^{-κ} over (a, b] equals (b^{1-κ} − a^{1-κ})/(1−κ).

Formal statement
hypotheses
κ :
ℝ
shared
hκ :
κ ≠ 1
a b :
ℝ
ha :
0 < a
hab :
a ≤ b
conclusion
∫ t in Ioc a b, t ^ (-κ) = (b ^ (1 - κ) - a ^ (1 - κ)) / (1 - κ)
Proof (Lean source)
theorem integral_rpow_neg_Ioc (hκ : κ ≠ 1) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : ∫ t in Ioc a b, t ^ (-κ) = (b ^ (1 - κ) - a ^ (1 - κ)) / (1 - κ) := by rw [← intervalIntegral.integral_of_le hab, integral_rpow (inr ⟨fun h => hκ (neg_inj.mp h), zero_notMem_uIcc ha hab⟩), show (-κ + 1 : ℝ) = 1 - κ from by ring]
Causalean.Stat.PolynomialTail.integral_rpow_neg_Ioc · Causalean/Stat/PolynomialTail/PowerIntegral.lean:45
2 supporting declarations (lemmas, instances)
  • zero_notMem_uIcc theorem — 0 ∉ [[a,b]] when 0 < a ≤ b.
    hypotheses
    a b :
    ℝ
    ha :
    0 < a
    hab :
    a ≤ b
    conclusion
    (0 : ℝ) ∉ uIcc a b
    Proof (Lean source)
    theorem zero_notMem_uIcc {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : (0 : ℝ) ∉ uIcc a b := by rw [Set.uIcc_of_le hab, Set.mem_Icc] exact fun h => absurd h.1 (not_le.mpr ha)
    Causalean.Stat.PolynomialTail.zero_notMem_uIcc · Causalean/Stat/PolynomialTail/PowerIntegral.lean:39
  • integral_inv_neg_Ioc theorem — Power integral, κ = 1. ∫ t in (a,b], t^{-1} = log b − log a.
    hypotheses
    a b :
    ℝ
    ha :
    0 < a
    hab :
    a ≤ b
    conclusion
    ∫ t in Ioc a b, t ^ (-(1 : ℝ)) = log b - log a
    Proof (Lean source)
    theorem integral_inv_neg_Ioc {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) : ∫ t in Ioc a b, t ^ (-(1 : ℝ)) = log b - log a := by have hcongr : EqOn (fun t : ℝ => t ^ (-(1 : ℝ))) (fun t => t⁻¹) (Ioc a b) := fun t _ => by simp [Real.rpow_neg_one] rw [setIntegral_congr_fun measurableSet_Ioc hcongr, ← intervalIntegral.integral_of_le hab, integral_inv (zero_notMem_uIcc ha hab), Real.log_div (ne_of_gt (lt_of_lt_of_le ha hab)) (ne_of_gt ha)]
    Causalean.Stat.PolynomialTail.integral_inv_neg_Ioc · Causalean/Stat/PolynomialTail/PowerIntegral.lean:54
Tail­Integral­Bounds 2 core · 4 supporting This module applies PolyTail to the layer-cake integrand from LayerCakeReduction. ★ tailIntegral_le★ tailIntegral_ge

Bounds on the polynomial-tail integral

This module applies PolyTail to the layer-cake integrand from LayerCakeReduction. On the window (t0^(-1), lam^(-1)], the substitution s = t^(-1) puts s in (0, t0], so the polynomial lower-tail bounds give cm * t^(-kappa) <= P.real {omega | U omega <= t^(-1)} <= cp * t^(-kappa).

The pointwise sandwich is recorded in tailIntegrand_lower_window and tailIntegrand_upper_window, with integrableOn_rpow_neg_window supplying the integrability of the power comparison function. The main results tailIntegral_ge and tailIntegral_le bound tailIntegral P U lam between cm times the power integral and an upper expression with the bounded pre-window contribution (t0^(-1) - 1) plus cp times the same power integral. These are the inputs for the three-regime J and I moment bounds.

theorem tailIntegral_le reviewed
Causalean.Stat.PolynomialTail

Upper bound on the tail integral. Under the polynomial lower-tail hypothesis PolyTail P U κ t₀ cm cp, for any threshold λ that is positive and at most the window endpoint t₀, the layer-cake tail integral tailIntegral P U λ is bounded by a constant pre-window contribution t₀⁻¹ − 1 plus cp times the power comparison integral over (t₀⁻¹, λ⁻¹]:

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
lam :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hlam_pos :
0 < lam
hlam_le :
lam ≤ t₀
conclusion
tailIntegral P U lam ≤ (t₀⁻¹ - 1) + cp * ∫ t in Ioc t₀⁻¹ lam⁻¹, t ^ (-κ)
Proof (Lean source)
theorem tailIntegral_le [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hlam_pos : 0 < lam) (hlam_le : lam ≤ t₀) : tailIntegral P U lam ≤ (t₀⁻¹ - 1) + cp * ∫ t in Ioc t₀⁻¹ lam⁻¹, t ^ (-κ) := by obtain ⟨h1t0, ht0lam⟩ := split_endpoints h hlam_pos hlam_le have hdisj : Disjoint (Ioc (1 : ℝ) t₀⁻¹) (Ioc t₀⁻¹ lam⁻¹) := by rw [Set.disjoint_left]; rintro x ⟨_, hx1⟩ ⟨hx2, _⟩; exact absurd hx2 (not_lt.mpr hx1) have hpow_int := integrableOn_rpow_neg_window h hlam_pos hlam_le have hconst_int : IntegrableOn (fun _ : ℝ => (1 : ℝ)) (Ioc 1 t₀⁻¹) volume := by haveI : IsFiniteMeasure (volume.restrict (Ioc (1 : ℝ) t₀⁻¹)) := ⟨by rw [Measure.restrict_apply_univ, Real.volume_Ioc]; exact ENNReal.ofReal_lt_top⟩ exact integrable_const 1 rw [tailIntegral, ← Set.Ioc_union_Ioc_eq_Ioc h1t0 ht0lam, setIntegral_union hdisj measurableSet_Ioc (integrableOn_tailIntegrand 1 t₀⁻¹) (integrableOn_tailIntegrand t₀⁻¹ lam⁻¹)] refine add_le_add ?_ ?_ · -- left piece: `≤ t₀⁻¹ - 1` calc ∫ t in Ioc (1 : ℝ) t₀⁻¹, P.real {ω | U ω ≤ t⁻¹} ≤ ∫ _t in Ioc (1 : ℝ) t₀⁻¹, (1 : ℝ) := setIntegral_mono_on (integrableOn_tailIntegrand 1 t₀⁻¹) hconst_int measurableSet_Ioc (fun t _ => tailIntegrand_le_one t) _ = t₀⁻¹ - 1 := by rw [setIntegral_const, smul_eq_mul, mul_one, measureReal_def, Real.volume_Ioc, ENNReal.toReal_ofReal (by linarith)] · -- right piece: `≤ cp * PowInt` rw [← integral_const_mul] exact setIntegral_mono_on (integrableOn_tailIntegrand t₀⁻¹ lam⁻¹) (hpow_int.const_mul cp) measurableSet_Ioc (fun t ht => tailIntegrand_upper_window h ht)
Causalean.Stat.PolynomialTail.tailIntegral_le · Causalean/Stat/PolynomialTail/TailIntegralBounds.lean:83 · uses PolyTail , tailIntegral
theorem tailIntegral_ge reviewed
Causalean.Stat.PolynomialTail

Lower bound on the tail integral. Under the polynomial lower-tail hypothesis PolyTail P U κ t₀ cm cp, for any threshold λ that is positive and at most the window endpoint t₀, cm times the power comparison integral over (t₀⁻¹, λ⁻¹] is a lower bound for the layer-cake tail integral tailIntegral P U λ:

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
lam :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hlam_pos :
0 < lam
hlam_le :
lam ≤ t₀
conclusion
cm * ∫ t in Ioc t₀⁻¹ lam⁻¹, t ^ (-κ) ≤ tailIntegral P U lam
Proof (Lean source)
theorem tailIntegral_ge [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hlam_pos : 0 < lam) (hlam_le : lam ≤ t₀) : cm * ∫ t in Ioc t₀⁻¹ lam⁻¹, t ^ (-κ) ≤ tailIntegral P U lam := by obtain ⟨h1t0, ht0lam⟩ := split_endpoints h hlam_pos hlam_le have hdisj : Disjoint (Ioc (1 : ℝ) t₀⁻¹) (Ioc t₀⁻¹ lam⁻¹) := by rw [Set.disjoint_left]; rintro x ⟨_, hx1⟩ ⟨hx2, _⟩; exact absurd hx2 (not_lt.mpr hx1) have hpow_int := integrableOn_rpow_neg_window h hlam_pos hlam_le rw [tailIntegral, ← Set.Ioc_union_Ioc_eq_Ioc h1t0 ht0lam, setIntegral_union hdisj measurableSet_Ioc (integrableOn_tailIntegrand 1 t₀⁻¹) (integrableOn_tailIntegrand t₀⁻¹ lam⁻¹)] have hleft : (0 : ℝ) ≤ ∫ t in Ioc (1 : ℝ) t₀⁻¹, P.real {ω | U ω ≤ t⁻¹} := setIntegral_nonneg measurableSet_Ioc (fun t _ => tailIntegrand_nonneg t) have hright : cm * ∫ t in Ioc t₀⁻¹ lam⁻¹, t ^ (-κ) ≤ ∫ t in Ioc t₀⁻¹ lam⁻¹, P.real {ω | U ω ≤ t⁻¹} := by rw [← integral_const_mul] exact setIntegral_mono_on (hpow_int.const_mul cm) (integrableOn_tailIntegrand t₀⁻¹ lam⁻¹) measurableSet_Ioc (fun t ht => tailIntegrand_lower_window h ht) linarith
Causalean.Stat.PolynomialTail.tailIntegral_ge · Causalean/Stat/PolynomialTail/TailIntegralBounds.lean:122 · uses PolyTail , tailIntegral
4 supporting declarations (lemmas, instances)
  • inv_rpow_eq_rpow_neg theorem — (t⁻¹)^κ = t^{-κ} for t > 0.
    hypotheses
    t :
    ℝ
    ht :
    0 < t
    κ :
    ℝ
    conclusion
    (t⁻¹) ^ κ = t ^ (-κ)
    Proof (Lean source)
    theorem inv_rpow_eq_rpow_neg {t : ℝ} (ht : 0 < t) (κ : ℝ) : (t⁻¹) ^ κ = t ^ (-κ) := by rw [Real.inv_rpow ht.le, ← Real.rpow_neg ht.le]
    Causalean.Stat.PolynomialTail.inv_rpow_eq_rpow_neg · Causalean/Stat/PolynomialTail/TailIntegralBounds.lean:48
  • tailIntegrand_upper_window theorem — Upper sandwich of the tail integrand on the polynomial window.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    Ω → ℝ
    shared
    κ :
    ℝ
    shared
    t₀ :
    ℝ
    shared
    cm :
    ℝ
    shared
    cp :
    ℝ
    shared
    lam :
    ℝ
    shared
    IsFiniteMeasure P
    h :
    PolyTail P U κ t₀ cm cp
    t :
    ℝ
    ht :
    t ∈ Ioc t₀⁻¹ lam⁻¹
    conclusion
    P.real {ω | U ω ≤ t⁻¹} ≤ cp * t ^ (-κ)
    Proof (Lean source)
    theorem tailIntegrand_upper_window [IsFiniteMeasure P] (h : PolyTail P U κ t₀ cm cp) {t : ℝ} (ht : t ∈ Ioc t₀⁻¹ lam⁻¹) : P.real {ω | U ω ≤ t⁻¹} ≤ cp * t ^ (-κ) := by have htpos : 0 < t := lt_trans (inv_pos.mpr h.t0_pos) ht.1 have htinv_le : t⁻¹ ≤ t₀ := le_of_lt ((inv_lt_comm₀ htpos h.t0_pos).mpr ht.1) calc P.real {ω | U ω ≤ t⁻¹} ≤ cp * (t⁻¹) ^ κ := h.tail_upper t⁻¹ (inv_pos.mpr htpos) htinv_le _ = cp * t ^ (-κ) := by rw [inv_rpow_eq_rpow_neg htpos]
    Causalean.Stat.PolynomialTail.tailIntegrand_upper_window · Causalean/Stat/PolynomialTail/TailIntegralBounds.lean:52
  • tailIntegrand_lower_window theorem — Lower sandwich of the tail integrand on the polynomial window.
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    Ω → ℝ
    shared
    κ :
    ℝ
    shared
    t₀ :
    ℝ
    shared
    cm :
    ℝ
    shared
    cp :
    ℝ
    shared
    lam :
    ℝ
    shared
    IsFiniteMeasure P
    h :
    PolyTail P U κ t₀ cm cp
    t :
    ℝ
    ht :
    t ∈ Ioc t₀⁻¹ lam⁻¹
    conclusion
    cm * t ^ (-κ) ≤ P.real {ω | U ω ≤ t⁻¹}
    Proof (Lean source)
    theorem tailIntegrand_lower_window [IsFiniteMeasure P] (h : PolyTail P U κ t₀ cm cp) {t : ℝ} (ht : t ∈ Ioc t₀⁻¹ lam⁻¹) : cm * t ^ (-κ) ≤ P.real {ω | U ω ≤ t⁻¹} := by have htpos : 0 < t := lt_trans (inv_pos.mpr h.t0_pos) ht.1 have htinv_le : t⁻¹ ≤ t₀ := le_of_lt ((inv_lt_comm₀ htpos h.t0_pos).mpr ht.1) calc cm * t ^ (-κ) = cm * (t⁻¹) ^ κ := by rw [inv_rpow_eq_rpow_neg htpos] _ ≤ P.real {ω | U ω ≤ t⁻¹} := h.tail_lower t⁻¹ (inv_pos.mpr htpos) htinv_le
    Causalean.Stat.PolynomialTail.tailIntegrand_lower_window · Causalean/Stat/PolynomialTail/TailIntegralBounds.lean:61
  • integrableOn_rpow_neg_window theorem — t^{-κ} is integrable on the window (t₀⁻¹, λ⁻¹].
    hypotheses
    Ω :
    Type u_1
    Measure Ω
    Ω → ℝ
    shared
    κ :
    ℝ
    shared
    t₀ :
    ℝ
    shared
    cm :
    ℝ
    shared
    cp :
    ℝ
    shared
    lam :
    ℝ
    shared
    h :
    PolyTail P U κ t₀ cm cp
    hlam_pos :
    0 < lam
    hlam_le :
    lam ≤ t₀
    conclusion
    IntegrableOn (fun t : ℝ => t ^ (-κ)) (Ioc t₀⁻¹ lam⁻¹) volume
    Proof (Lean source)
    theorem integrableOn_rpow_neg_window (h : PolyTail P U κ t₀ cm cp) (hlam_pos : 0 < lam) (hlam_le : lam ≤ t₀) : IntegrableOn (fun t : ℝ => t ^ (-κ)) (Ioc t₀⁻¹ lam⁻¹) volume := by have ht0lam : t₀⁻¹ ≤ lam⁻¹ := (inv_le_inv₀ h.t0_pos hlam_pos).mpr hlam_le exact (intervalIntegral.intervalIntegrable_rpow (inr (zero_notMem_uIcc (inv_pos.mpr h.t0_pos) ht0lam))).1
    Causalean.Stat.PolynomialTail.integrableOn_rpow_neg_window · Causalean/Stat/PolynomialTail/TailIntegralBounds.lean:70
Trim­Bias 1 core · 0 supporting This module bounds the contribution left by the trimming weight trimWeight U lam = 1 - U / (max U lam). ★ trimWeight_bias_bound

Bias from trimming the lower tail

This module bounds the contribution left by the trimming weight trimWeight U lam = 1 - U / (max U lam). Since this weight is between 0 and 1 and vanishes off {omega | U omega < lam}, any integrand g whose absolute value is bounded by Cbeta * lam^beta on the trimmed set has integrated bias controlled by the lower-tail mass.

The main theorem trimWeight_bias_bound proves |int trimWeight U lam * g dP| <= Cbeta * cp * lam^(kappa + beta) under PolyTail, TailSetup, and 0 < lam <= t0. It is the elementary "tail mass times local envelope" companion to the layer-cake inverse-moment bounds.

theorem trimWeight_bias_bound reviewed
Causalean.Stat.PolynomialTail

General trimming-bias bound. Under the polynomial lower-tail hypothesis PolyTail P U κ t₀ cm cp with U measurable and almost surely in (0,1], fix a threshold λ that is positive and at most the window endpoint t₀. If the envelope constant Cβ is nonnegative, g is measurable, and g obeys the Hölder envelope |g| ≤ Cβ · λ^β on the event {U < λ}, then the integrated bias |∫ wλ · g dP| is at most Cβ · cp · λ^{κ+β}:

Formal statement
hypotheses
Ω :
Type u_1
Measure Ω
Ω → ℝ
shared
κ :
ℝ
shared
t₀ :
ℝ
shared
cm :
ℝ
shared
cp :
ℝ
shared
lam :
ℝ
shared
β :
ℝ
shared
IsProbabilityMeasure P
h :
PolyTail P U κ t₀ cm cp
hsetup :
TailSetup P U
hlam_pos :
0 < lam
hlam_le :
lam ≤ t₀
g :
Ω → ℝ
Cβ :
ℝ
hCβ :
0 ≤ Cβ
hg_meas :
Measurable g
hg_bd :
∀ ω
if
U ω < lam
then
|g ω| ≤ Cβ * lam ^ β
conclusion
|∫ ω, trimWeight U lam ω * g ω ∂P| ≤ Cβ * cp * lam ^ (κ + β)
Proof (Lean source)
theorem trimWeight_bias_bound [IsProbabilityMeasure P] (h : PolyTail P U κ t₀ cm cp) (hsetup : TailSetup P U) (hlam_pos : 0 < lam) (hlam_le : lam ≤ t₀) {g : Ω → ℝ} {Cβ : ℝ} (hCβ : 0 ≤ Cβ) (hg_meas : Measurable g) (hg_bd : ∀ ω, U ω < lam → |g ω| ≤ Cβ * lam ^ β) : |∫ ω, trimWeight U lam ω * g ω ∂P| ≤ Cβ * cp * lam ^ (κ + β) := by have hmsβ : (0 : ℝ) ≤ Cβ * lam ^ β := mul_nonneg hCβ (Real.rpow_nonneg hlam_pos.le _) have hsmeas : MeasurableSet {ω | U ω < lam} := hsetup.measurable measurableSet_Iio -- a.e. pointwise bound by the envelope times the indicator of `{U < λ}` have hpt : ∀ᵐ ω ∂P, |trimWeight U lam ω * g ω| ≤ (Cβ * lam ^ β) * indicator {ω | U ω < lam} (fun _ => (1 : ℝ)) ω := by filter_upwards [hsetup.pos] with ω hUpos by_cases hω : U ω < lam · have hw := trimWeight_mem hlam_pos hUpos have hwle1 : trimWeight U lam ω ≤ 1 := hw.2 have hw0 : 0 ≤ trimWeight U lam ω := hw.1 rw [abs_mul, Set.indicator_of_mem (show ω ∈ {ω | U ω < lam} from hω), mul_one] calc |trimWeight U lam ω| * |g ω| ≤ 1 * (Cβ * lam ^ β) := mul_le_mul (by rw [abs_of_nonneg hw0]; exact hwle1) (hg_bd ω hω) (abs_nonneg _) (by norm_num) _ = Cβ * lam ^ β := one_mul _ · have hzero : trimWeight U lam ω = 0 := by simp only [trimWeight, max_eq_left (not_lt.mp hω), div_self (ne_of_gt hUpos), sub_self] rw [hzero, zero_mul, abs_zero] exact mul_nonneg hmsβ (Set.indicator_nonneg (fun _ _ => zero_le_one) ω) -- integrability of `wλ · g` (bounded a.e. by the integrable RHS) have hRHS_int : Integrable (fun ω => (Cβ * lam ^ β) * indicator {ω | U ω < lam} (fun _ => (1 : ℝ)) ω) P := by fun_prop have hint : Integrable (fun ω => trimWeight U lam ω * g ω) P := by refine Integrable.mono' hRHS_int ((measurable_trimWeight hsetup.measurable).mul hg_meas).aestronglyMeasurable ?_ filter_upwards [hpt] with ω hω; rwa [Real.norm_eq_abs] -- chain: |∫| ≤ ∫|·| ≤ ∫ envelope·𝟙 = Cβλ^β · P{U<λ} ≤ Cβ cp λ^{κ+β} calc |∫ ω, trimWeight U lam ω * g ω ∂P| ≤ ∫ ω, |trimWeight U lam ω * g ω| ∂P := abs_integral_le_integral_abs _ ≤ ∫ ω, (Cβ * lam ^ β) * indicator {ω | U ω < lam} (fun _ => (1 : ℝ)) ω ∂P := integral_mono_ae hint.abs hRHS_int hpt _ = (Cβ * lam ^ β) * P.real {ω | U ω < lam} := by rw [integral_const_mul, integral_indicator hsmeas, setIntegral_const, smul_eq_mul, mul_one] _ ≤ (Cβ * lam ^ β) * (cp * lam ^ κ) := by gcongr exact measureReal_lt_le h hlam_pos hlam_le _ = Cβ * cp * lam ^ (κ + β) := by rw [Real.rpow_add hlam_pos]; ring
Causalean.Stat.PolynomialTail.trimWeight_bias_bound · Causalean/Stat/PolynomialTail/TrimBias.lean:43 · uses PolyTail , TailSetup , trimWeight