Moments

Results named in Tau Ceti's TauCeti.Probability.Moments modules and in no roadmap's section, as Tau Ceti has them at commit ace60277.

TheoremAzuma-Hoeffding inequality#

Let Y i be a strongly adapted sequence of martingale differences with |Y i| ≤ b i almost surely, mean zero at time zero, and conditional mean zero at each later step. Then the upper tail of the sum of its first n terms is bounded by exp (-ε ^ 2 / (2 * ∑ i < n, b i ^ 2)).

TauCeti.Probability.measureReal_sum_range_ge_le_of_bounded_martingale_differences.{u_1}
  {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω]
  [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ}
  {b : ℕ → NNReal} (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (n : ℕ)
  (hbound : ∀ i < n, ∀ᵐ (ω : Ω) ∂μ, |Y i ω| ≤ ↑(b i)) (hmean0 : ∫ (ω : Ω), Y 0 ω ∂μ = 0)
  (hmean : ∀ i < n - 1, μ[Y (i + 1) | ↑ℱ i] =ᵐ[μ] 0) {ε : ℝ} (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤
    Real.exp (-ε ^ 2 / (2 * ∑ i ∈ Finset.range n, ↑(b i) ^ 2))

Lean

Formalized in Tau Ceti as TauCeti.Probability.measureReal_sum_range_ge_le_of_bounded_martingale_differences.

Other forms

Azuma-Hoeffding inequality for interval-bounded martingale differences. Formalized in Tau Ceti as TauCeti.Probability.measureReal_sum_range_ge_le_of_mem_Icc_martingale_differences.

TauCeti.Probability.measureReal_sum_range_ge_le_of_mem_Icc_martingale_differences.{u_1}
  {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω]
  [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ}
  {a b : ℕ → ℝ} (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (n : ℕ)
  (hbound : ∀ i < n, ∀ᵐ (ω : Ω) ∂μ, Y i ω ∈ Set.Icc (a i) (b i)) (hmean0 : ∫ (ω : Ω), Y 0 ω ∂μ = 0)
  (hmean : ∀ i < n - 1, μ[Y (i + 1) | ↑ℱ i] =ᵐ[μ] 0) {ε : ℝ} (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ ∑ i ∈ Finset.range n, Y i ω} ≤
    Real.exp (-ε ^ 2 / (2 * ∑ i ∈ Finset.range n, (↑‖b i - a i‖₊ / 2) ^ 2))

Sources

• Tau Ceti documentation: TauCeti.Probability.measureReal_sum_range_ge_le_of_bounded_martingale_differences
• Source of TauCeti.Probability.measureReal_sum_range_ge_le_of_bounded_martingale_differences in TauCeti/Probability/Moments/Azuma.lean

LeanTauCeti.Probability.measureReal_sum_range_ge_le_of_bounded_martingale_differences · TauCeti.Probability.measureReal_sum_range_ge_le_of_mem_Icc_martingale_differences

Used by 1

Used byTwo-sided Azuma-Hoeffding inequality

TheoremBernstein's inequality#

Let the Xᵢ, i ∈ s, be independent with mean zero, finite second moments and Xᵢ ≤ b almost surely, and let v = ∑ i ∈ s, E Xᵢ². Then for 0 ≤ ε, P(ε ≤ ∑ i ∈ s, Xᵢ) ≤ exp (-ε ^ 2 / (2 * (v + b * ε / 3))).

ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_ae_le.{u_1, u_2} {Ω : Type u_1}
  {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  (h_indep : ProbabilityTheory.iIndepFun X μ) {s : Finset ι} {b ε : ℝ}
  (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0)
  (hb : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b) (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ ∑ i ∈ s, X i ω} ≤
    Real.exp (-ε ^ 2 / (2 * (∑ i ∈ s, ∫ (ω : Ω), X i ω ^ 2 ∂μ + b * ε / 3)))

Lean

Formalized in Tau Ceti as ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_ae_le.

Other forms

Bernstein's inequality, two-sided form. Formalized in Tau Ceti as ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_abs_le.

ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_abs_le.{u_1, u_2} {Ω : Type u_1}
  {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  (h_indep : ProbabilityTheory.iIndepFun X μ) {s : Finset ι} {b ε : ℝ}
  (hX : ∀ i ∈ s, AEMeasurable (X i) μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0)
  (hb : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, |X i ω| ≤ b) (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ |∑ i ∈ s, X i ω|} ≤
    2 * Real.exp (-ε ^ 2 / (2 * (∑ i ∈ s, ∫ (ω : Ω), X i ω ^ 2 ∂μ + b * ε / 3)))

Sources

• Tau Ceti documentation: ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_ae_le
• Source of ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_ae_le in TauCeti/Probability/Moments/Bernstein.lean

LeanProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_ae_le · ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_abs_le

Uses 1

Proof usesBernstein's moment-generating-function bound

TheoremBernstein's moment-generating-function bound#

If X has mean zero, a finite second moment and X ≤ b almost surely, then for 0 ≤ t with t * b < 3, E exp (t X) ≤ exp (E X² * t ^ 2 / (2 * (1 - t * b / 3))).

MeasureTheory.MemLp.mgf_le_exp_of_ae_le.{u_1} {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {b t : ℝ}
  (hX : MeasureTheory.MemLp X 2 μ) (hmean : ∫ (x : Ω), X x ∂μ = 0) (hb : ∀ᵐ (ω : Ω) ∂μ, X ω ≤ b)
  (ht : 0 ≤ t) (htb : t * b < 3) :
  ProbabilityTheory.mgf X μ t ≤ Real.exp ((∫ (ω : Ω), X ω ^ 2 ∂μ) * t ^ 2 / (2 * (1 - t * b / 3)))

Lean

Formalized in Tau Ceti as MeasureTheory.MemLp.mgf_le_exp_of_ae_le.

Other forms

Bernstein's moment-generating-function bound for independent sums. Formalized in Tau Ceti as ProbabilityTheory.iIndepFun.mgf_sum_le_exp_of_ae_le.

ProbabilityTheory.iIndepFun.mgf_sum_le_exp_of_ae_le.{u_1, u_2} {Ω : Type u_1}
  {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {ι : Type u_2} {X : ι → Ω → ℝ}
  (h_indep : ProbabilityTheory.iIndepFun X μ) {s : Finset ι} {b t : ℝ}
  (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0)
  (hb : ∀ i ∈ s, ∀ᵐ (ω : Ω) ∂μ, X i ω ≤ b) (ht : 0 ≤ t) (htb : t * b < 3) :
  ProbabilityTheory.mgf (fun ω => ∑ i ∈ s, X i ω) μ t ≤
    Real.exp ((∑ i ∈ s, ∫ (ω : Ω), X i ω ^ 2 ∂μ) * t ^ 2 / (2 * (1 - t * b / 3)))

Sources

• Tau Ceti documentation: MeasureTheory.MemLp.mgf_le_exp_of_ae_le
• Source of MeasureTheory.MemLp.mgf_le_exp_of_ae_le in TauCeti/Probability/Moments/Bernstein.lean

LeanMeasureTheory.MemLp.mgf_le_exp_of_ae_le · ProbabilityTheory.iIndepFun.mgf_sum_le_exp_of_ae_le

Uses 1 · Used by 1

Proof usesBernstein's exponential bound

Used byBernstein's inequality

TheoremBienaymé's identity for random vectors#

If the random vectors X i, i ∈ s, in a real Hilbert space are square-integrable, centered and pairwise independent, then the expected squared norm of their sum is the sum of their expected squared norms.

TauCeti.integral_norm_sum_sq_of_pairwise_indepFun.{u_1, u_2, u_3} {Ω : Type u_1} {ι : Type u_2}
  {E : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [NormedAddCommGroup E]
  [InnerProductSpace ℝ E] [CompleteSpace E] [MeasurableSpace E] [BorelSpace E]
  [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → E} {s : Finset ι}
  (hX : ∀ i ∈ s, MeasureTheory.MemLp (X i) 2 μ) (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0)
  (hindep : (↑s).Pairwise fun i j => ProbabilityTheory.IndepFun (X i) (X j) μ) :
  ∫ (ω : Ω), ‖∑ i ∈ s, X i ω‖ ^ 2 ∂μ = ∑ i ∈ s, ∫ (ω : Ω), ‖X i ω‖ ^ 2 ∂μ

Lean

Formalized in Tau Ceti as TauCeti.integral_norm_sum_sq_of_pairwise_indepFun.

Sources

• Tau Ceti documentation: TauCeti.integral_norm_sum_sq_of_pairwise_indepFun
• Source of TauCeti.integral_norm_sum_sq_of_pairwise_indepFun in TauCeti/Probability/Moments/SampleMean.lean

LeanTauCeti.integral_norm_sum_sq_of_pairwise_indepFun

TheoremChebyshev's inequality for the second moment#

For any measure, if ‖Y‖² is integrable and 0 < c, the set where ‖Y‖ is at least c has measure at most (∫ ‖Y‖²) / c². Unlike ProbabilityTheory.meas_ge_le_variance_div_sq, Y is not centered at its mean.

TauCeti.meas_ge_le_integral_norm_sq_div_sq.{u_1, u_2} {Ω : Type u_1} {E : Type u_2}
  {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Norm E] {Y : Ω → E}
  (hY : MeasureTheory.Integrable (fun ω => ‖Y ω‖ ^ 2) μ) {c : ℝ} (hc : 0 < c) :
  μ {ω | c ≤ ‖Y ω‖} ≤ ENNReal.ofReal ((∫ (ω : Ω), ‖Y ω‖ ^ 2 ∂μ) / c ^ 2)

Lean

Formalized in Tau Ceti as TauCeti.meas_ge_le_integral_norm_sq_div_sq.

Sources

• Tau Ceti documentation: TauCeti.meas_ge_le_integral_norm_sq_div_sq
• Source of TauCeti.meas_ge_le_integral_norm_sq_div_sq in TauCeti/Probability/Moments/Chebyshev.lean

LeanTauCeti.meas_ge_le_integral_norm_sq_div_sq

Used by 1

Used byThe uncentered Chebyshev inequality

TheoremEntrywise Chebyshev union bound#

For any measure μ, if every squared entrywise deviation of a matrix-valued function S from a fixed matrix A is integrable with integral at most v, then the measure of the event where some entry deviates by more than η > 0 is at most ENNReal.ofReal (card m * card n * v / η²).

TauCeti.measure_exists_lt_norm_sub_le.{u_1, u_2, u_3, u_4} {Ω : Type u_1} {m : Type u_2}
  {n : Type u_3} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [Fintype m] [Fintype n]
  {E : Type u_4} {S : Ω → Matrix m n E} {A : Matrix m n E} {v η : ℝ} [Norm E] [Sub E]
  (hint : ∀ (k : m) (l : n), MeasureTheory.Integrable (fun ω => ‖S ω k l - A k l‖ ^ 2) μ)
  (hmoment : ∀ (k : m) (l : n), ∫ (ω : Ω), ‖S ω k l - A k l‖ ^ 2 ∂μ ≤ v) (hη : 0 < η) :
  μ {ω | ∃ k l, η < ‖S ω k l - A k l‖} ≤
    ENNReal.ofReal (↑(Fintype.card m) * ↑(Fintype.card n) * v / η ^ 2)

Lean

Formalized in Tau Ceti as TauCeti.measure_exists_lt_norm_sub_le.

Sources

• Tau Ceti documentation: TauCeti.measure_exists_lt_norm_sub_le
• Source of TauCeti.measure_exists_lt_norm_sub_le in TauCeti/Probability/Moments/MatrixConcentration.lean

LeanTauCeti.measure_exists_lt_norm_sub_le

Uses 1

Proof usesThe uncentered Chebyshev inequality

TheoremOne-sided sub-exponential Bernstein inequality#

For independent centered variables with common parameter K, this bounds the upper tail of a finite sum.

ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_hasSubexponentialMGF.{u_1, u_2} {Ω : Type u_1}
  [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {ι : Type u_2} {X : ι → Ω → ℝ} (h_indep : ProbabilityTheory.iIndepFun X μ) {s : Finset ι}
  {K t : ℝ} (hK : 0 < K) (hX : ∀ i ∈ s, TauCeti.Probability.HasSubexponentialMGF (X i) K μ)
  (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (ht : 0 < t) :
  μ.real {ω | t ≤ ∑ i ∈ s, X i ω} ≤ Real.exp (-t ^ 2 / (4 * (↑s.card * K ^ 2 + K * t)))

Lean

Formalized in Tau Ceti as ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_hasSubexponentialMGF.

Sources

• Tau Ceti documentation: ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_hasSubexponentialMGF
• Source of ProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_hasSubexponentialMGF in TauCeti/Probability/Moments/SubExponential.lean

LeanProbabilityTheory.iIndepFun.measureReal_sum_ge_le_of_hasSubexponentialMGF

Used by 1

Used bySub-exponential Bernstein inequality

TheoremThe quadratic Fenchel–Young inequality in mean#

Let X and Y be square-integrable random vectors, where the law of X has covariance matrix A * T * A for a positive-semidefinite matrix A. Then the correlation of the centred variable X - 𝔼 X with Y is at most (𝔼 ⟪A Y, Y⟫ + tr (A * T)) / 2.

TauCeti.integral_inner_sub_integral_le.{u_1, u_2} {ι : Type u_1} [Fintype ι] [DecidableEq ι]
  {Ω : Type u_2} [MeasurableSpace Ω] {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {X Y : Ω → EuclideanSpace ℝ ι}
  (hX : MeasureTheory.MemLp X 2 P) (hY : MeasureTheory.MemLp Y 2 P) {A T : Matrix ι ι ℝ}
  (hA : A.PosSemidef) (hcov : TauCeti.covMatrix (MeasureTheory.Measure.map X P) = A * T * A) :
  ∫ (ω : Ω), inner ℝ (X ω - ∫ (ω' : Ω), X ω' ∂P) (Y ω) ∂P ≤
    (∫ (ω : Ω), inner ℝ ((Matrix.toEuclideanLin A) (Y ω)) (Y ω) ∂P + (A * T).trace) / 2

Lean

Formalized in Tau Ceti as TauCeti.integral_inner_sub_integral_le.

Sources

• Tau Ceti documentation: TauCeti.integral_inner_sub_integral_le
• Source of TauCeti.integral_inner_sub_integral_le in TauCeti/Probability/Moments/FenchelYoung.lean

LeanTauCeti.integral_inner_sub_integral_le

TheoremSub-exponential Bernstein inequality#

If the Xᵢ, i ∈ s, are independent, centered and sub-exponential with common parameter K, then for t > 0

P(|∑ i ∈ s, Xᵢ| ≥ t) ≤ 2 * exp (-t^2 / (4 * (|s| * K^2 + K * t))).

The constants follow directly from the centered MGF bound E exp (λ Xᵢ) ≤ exp (K ^ 2 * λ ^ 2) for |λ| ≤ 1 / K.

ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_hasSubexponentialMGF.{u_1, u_2}
  {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] {ι : Type u_2} {X : ι → Ω → ℝ}
  (h_indep : ProbabilityTheory.iIndepFun X μ) {s : Finset ι} {K t : ℝ} (hK : 0 < K)
  (hX : ∀ i ∈ s, TauCeti.Probability.HasSubexponentialMGF (X i) K μ)
  (hmean : ∀ i ∈ s, ∫ (x : Ω), X i x ∂μ = 0) (ht : 0 < t) :
  μ.real {ω | t ≤ |∑ i ∈ s, X i ω|} ≤ 2 * Real.exp (-t ^ 2 / (4 * (↑s.card * K ^ 2 + K * t)))

Lean

Formalized in Tau Ceti as ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_hasSubexponentialMGF.

Sources

• Tau Ceti documentation: ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_hasSubexponentialMGF
• Source of ProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_hasSubexponentialMGF in TauCeti/Probability/Moments/SubExponential.lean

LeanProbabilityTheory.iIndepFun.measureReal_abs_sum_ge_le_of_hasSubexponentialMGF

Uses 1

Proof usesOne-sided sub-exponential Bernstein inequality

TheoremSymmetrization by Jensen's inequality#

For a probability measure μ, the moment generating function of f - 𝔼 f at t is at most ∫∫ exp (t (f x - f y)) dμ(x) dμ(y).

TauCeti.ofReal_mgf_sub_integral_le_lintegral.{u_1} {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} {f : Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ]
  (hfm : Measurable f) (hfi : MeasureTheory.Integrable f μ) {t : ℝ}
  (hint : MeasureTheory.Integrable (fun x => Real.exp (t * (f x - ∫ (y : Ω), f y ∂μ))) μ)
  (hneg : MeasureTheory.Integrable (fun x => Real.exp (-t * f x)) μ) :
  ENNReal.ofReal (ProbabilityTheory.mgf (fun x => f x - ∫ (y : Ω), f y ∂μ) μ t) ≤
    ∫⁻ (p : Ω × Ω), ENNReal.ofReal (Real.exp (t * (f p.1 - f p.2))) ∂μ.prod μ

Lean

Formalized in Tau Ceti as TauCeti.ofReal_mgf_sub_integral_le_lintegral.

Sources

• Tau Ceti documentation: TauCeti.ofReal_mgf_sub_integral_le_lintegral
• Source of TauCeti.ofReal_mgf_sub_integral_le_lintegral in TauCeti/Probability/Moments/Basic.lean

LeanTauCeti.ofReal_mgf_sub_integral_le_lintegral

TheoremTwo-sided Azuma-Hoeffding inequality#

Under the assumptions of measureReal_sum_range_ge_le_of_bounded_martingale_differences, the absolute value of the sum exceeds ε with probability at most twice the one-sided bound.

TauCeti.Probability.measureReal_abs_sum_range_ge_le_of_bounded_martingale_differences.{u_1}
  {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω]
  [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ}
  {b : ℕ → NNReal} (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (n : ℕ)
  (hbound : ∀ i < n, ∀ᵐ (ω : Ω) ∂μ, |Y i ω| ≤ ↑(b i)) (hmean0 : ∫ (ω : Ω), Y 0 ω ∂μ = 0)
  (hmean : ∀ i < n - 1, μ[Y (i + 1) | ↑ℱ i] =ᵐ[μ] 0) {ε : ℝ} (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ |∑ i ∈ Finset.range n, Y i ω|} ≤
    2 * Real.exp (-ε ^ 2 / (2 * ∑ i ∈ Finset.range n, ↑(b i) ^ 2))

Lean

Formalized in Tau Ceti as TauCeti.Probability.measureReal_abs_sum_range_ge_le_of_bounded_martingale_differences.

Other forms

Two-sided Azuma-Hoeffding inequality for interval-bounded martingale differences. Formalized in Tau Ceti as TauCeti.Probability.measureReal_abs_sum_range_ge_le_of_mem_Icc_martingale_differences.

TauCeti.Probability.measureReal_abs_sum_range_ge_le_of_mem_Icc_martingale_differences.{u_1}
  {Ω : Type u_1} [mΩ : MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [StandardBorelSpace Ω]
  [MeasureTheory.IsProbabilityMeasure μ] {ℱ : MeasureTheory.Filtration ℕ mΩ} {Y : ℕ → Ω → ℝ}
  {a b : ℕ → ℝ} (h_adapted : MeasureTheory.StronglyAdapted ℱ Y) (n : ℕ)
  (hbound : ∀ i < n, ∀ᵐ (ω : Ω) ∂μ, Y i ω ∈ Set.Icc (a i) (b i)) (hmean0 : ∫ (ω : Ω), Y 0 ω ∂μ = 0)
  (hmean : ∀ i < n - 1, μ[Y (i + 1) | ↑ℱ i] =ᵐ[μ] 0) {ε : ℝ} (hε : 0 ≤ ε) :
  μ.real {ω | ε ≤ |∑ i ∈ Finset.range n, Y i ω|} ≤
    2 * Real.exp (-ε ^ 2 / (2 * ∑ i ∈ Finset.range n, (↑‖b i - a i‖₊ / 2) ^ 2))

Sources

• Tau Ceti documentation: TauCeti.Probability.measureReal_abs_sum_range_ge_le_of_bounded_martingale_differences
• Source of TauCeti.Probability.measureReal_abs_sum_range_ge_le_of_bounded_martingale_differences in TauCeti/Probability/Moments/Azuma.lean

LeanTauCeti.Probability.measureReal_abs_sum_range_ge_le_of_bounded_martingale_differences · TauCeti.Probability.measureReal_abs_sum_range_ge_le_of_mem_Icc_martingale_differences

Uses 1

Proof usesAzuma-Hoeffding inequality

TheoremThe uncentered Chebyshev inequality#

If Y² is integrable with ∫ Y² ≤ v and 0 < η, then the set where Y exceeds η has measure at most v / η².

TauCeti.meas_gt_le_div_sq_of_integral_sq_le.{u_1} {Ω : Type u_1} {mΩ : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} {Y : Ω → ℝ} (hY : MeasureTheory.Integrable (fun ω => Y ω ^ 2) μ)
  {v η : ℝ} (hv : ∫ (ω : Ω), Y ω ^ 2 ∂μ ≤ v) (hη : 0 < η) :
  μ {ω | η < Y ω} ≤ ENNReal.ofReal (v / η ^ 2)

Lean

Formalized in Tau Ceti as TauCeti.meas_gt_le_div_sq_of_integral_sq_le.

Sources

• Tau Ceti documentation: TauCeti.meas_gt_le_div_sq_of_integral_sq_le
• Source of TauCeti.meas_gt_le_div_sq_of_integral_sq_le in TauCeti/Probability/Moments/Chebyshev.lean

LeanTauCeti.meas_gt_le_div_sq_of_integral_sq_le

Uses 1 · Used by 1

Proof usesChebyshev's inequality for the second moment

Used byEntrywise Chebyshev union bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.