← Copula mathematical handbook

noncomputable def ProbabilityTheory.Copula.RankRegion.XiBlest.Support.empiricalMean {Ω : Type u_1} (X : ℕ → Ω → ℝ) (n : ℕ) (ω : Ω) : ℝ

Equations

• ProbabilityTheory.Copula.RankRegion.XiBlest.Support.empiricalMean X n ω = (∑ i ∈ Finset.range n, X i ω) / ↑n

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.empiricalMean_deviation {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ℕ → Ω → ℝ) (hX : ∀ (i : ℕ), Measurable (X i)) (hI : iIndepFun X μ) (hb : ∀ (i : ℕ) (ω : Ω), X i ω ∈ Set.Icc 0 1) (p : ℝ) (hp : p ∈ Set.Icc 0 1) (hmean : ∀ (i : ℕ), ∫ (ω : Ω), X i ω ∂μ = p) (n : ℕ) (hn : 0 < n) (ε : ℝ) (hε : 0 ≤ ε) : μ.real {ω : Ω | ε ≤ |empiricalMean X n ω - p|} ≤ 2 * Real.exp (-↑n * ε ^ 2 / 2)

A two-sided Hoeffding bound, with a deliberately nonoptimal constant, for independent observations in the unit interval.

theorem ProbabilityTheory.Copula.RankRegion.XiBlest.Support.empiricalMean_finite_deviation {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] [Fintype ι] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (X : ι → ℕ → Ω → ℝ) (hX : ∀ (t : ι) (i : ℕ), Measurable (X t i)) (hI : ∀ (t : ι), iIndepFun (X t) μ) (hb : ∀ (t : ι) (i : ℕ) (ω : Ω), X t i ω ∈ Set.Icc 0 1) (p : ι → ℝ) (hp : ∀ (t : ι), p t ∈ Set.Icc 0 1) (hmean : ∀ (t : ι) (i : ℕ), ∫ (ω : Ω), X t i ω ∂μ = p t) (n : ℕ) (hn : 0 < n) (ε : ℝ) (hε : 0 ≤ ε) : μ.real {ω : Ω | ∃ (t : ι), ε ≤ |empiricalMean (X t) n ω - p t|} ≤ ↑(Fintype.card ι) * 2 * Real.exp (-↑n * ε ^ 2 / 2)