Other results

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

TheoremChapman–Kolmogorov lower bound#

The m + n-step mass of a measurable set s is at least the mass of the paths that sit at the intermediate state y at time m.

ProbabilityTheory.Kernel.pow_apply_singleton_mul_le_pow_add_apply.{u_1} {α : Type u_1}
  [MeasurableSpace α] (κ : ProbabilityTheory.Kernel α α) (m n : ℕ) (x y : α) {s : Set α}
  (hs : MeasurableSet s) : ((κ ^ m) x) {y} * ((κ ^ n) y) s ≤ ((κ ^ (m + n)) x) s
Lean

Formalized in Tau Ceti as ProbabilityTheory.Kernel.pow_apply_singleton_mul_le_pow_add_apply.

Sources
LeanProbabilityTheory.Kernel.pow_apply_singleton_mul_le_pow_add_apply

TheoremThe contractable form of de Finetti's theorem via L² averaging#

A contractable process valued in a nonempty standard Borel space is conditionally i.i.d.

The directing measure witnessing the conclusion is tailConditionalProbabilityMeasure μ X; its stronger witness-level statement is Contractable.conditionallyIIDWith_directingProbabilityMeasure.

TauCeti.Probability.conditionallyIID_of_contractable_viaL2.{u_1, u_2} {Ω : Type u_1} {α : Type u_2}
  [MeasurableSpace Ω] [MeasurableSpace α] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ → Ω → α}
  (hX : TauCeti.Probability.Contractable μ X) (hX_meas : ∀ (n : ℕ), Measurable (X n)) :
  TauCeti.Probability.ConditionallyIID μ X
Lean

Formalized in Tau Ceti as TauCeti.Probability.conditionallyIID_of_contractable_viaL2.

Sources
LeanTauCeti.Probability.conditionallyIID_of_contractable_viaL2
Used by 1
Used byDe Finetti's theorem

TheoremDe Finetti's theorem for the rows of a block of pairs#

The conclusion simultaneously describes both orientations of the selected rectangular cross-block.

TauCeti.Probability.JointlyExchangeable.conditionallyIID_arrayRow_arrayBlockPair.{u_1, u_2}
  {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} [StandardBorelSpace α]
  [Nonempty α] [MeasureTheory.IsFiniteMeasure μ] (h : TauCeti.Probability.JointlyExchangeable μ X)
  (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) (hf : Function.Injective f)
  (hd : Disjoint (Set.range e) (Set.range f)) :
  TauCeti.Probability.ConditionallyIID μ
    (TauCeti.Probability.arrayRow (TauCeti.Probability.arrayBlockPair X e f))
Lean

Formalized in Tau Ceti as TauCeti.Probability.JointlyExchangeable.conditionallyIID_arrayRow_arrayBlockPair.

Other forms

De Finetti's theorem for the columns of a separately exchangeable array. Formalized in Tau Ceti as TauCeti.Probability.SeparatelyExchangeable.conditionallyIID_arrayCol.

TauCeti.Probability.SeparatelyExchangeable.conditionallyIID_arrayCol.{u_1, u_2} {α : Type u_1}
  {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ × ℕ → Ω → α}
  (h : TauCeti.Probability.SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) :
  TauCeti.Probability.ConditionallyIID μ (TauCeti.Probability.arrayCol X)

De Finetti's theorem for the rows of a block of a jointly exchangeable array. Formalized in Tau Ceti as TauCeti.Probability.JointlyExchangeable.conditionallyIID_arrayRow_arrayBlock.

TauCeti.Probability.JointlyExchangeable.conditionallyIID_arrayRow_arrayBlock.{u_1, u_2}
  {α : Type u_1} {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} {X : ℕ × ℕ → Ω → α} {e f : ℕ → ℕ} [StandardBorelSpace α]
  [Nonempty α] [MeasureTheory.IsFiniteMeasure μ] (h : TauCeti.Probability.JointlyExchangeable μ X)
  (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) (he : Function.Injective e) (hf : Function.Injective f)
  (hd : Disjoint (Set.range e) (Set.range f)) :
  TauCeti.Probability.ConditionallyIID μ
    (TauCeti.Probability.arrayRow (TauCeti.Probability.arrayBlock X e f))

De Finetti's theorem for the rows of a separately exchangeable array. Formalized in Tau Ceti as TauCeti.Probability.SeparatelyExchangeable.conditionallyIID_arrayRow.

TauCeti.Probability.SeparatelyExchangeable.conditionallyIID_arrayRow.{u_1, u_2} {α : Type u_1}
  {Ω : Type u_2} [MeasurableSpace α] [MeasurableSpace Ω] [StandardBorelSpace α] [Nonempty α]
  {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : ℕ × ℕ → Ω → α}
  (h : TauCeti.Probability.SeparatelyExchangeable μ X) (hX : ∀ (p : ℕ × ℕ), AEMeasurable (X p) μ) :
  TauCeti.Probability.ConditionallyIID μ (TauCeti.Probability.arrayRow X)
Sources
LeanTauCeti.Probability.JointlyExchangeable.conditionallyIID_arrayRow_arrayBlockPair · TauCeti.Probability.SeparatelyExchangeable.conditionallyIID_arrayCol · TauCeti.Probability.JointlyExchangeable.conditionallyIID_arrayRow_arrayBlock · TauCeti.Probability.SeparatelyExchangeable.conditionallyIID_arrayRow
Uses 1
Proof usesDe Finetti's theorem

TheoremDe Finetti's theorem transported along an explicit enumeration#

Under a finite measure, an exchangeable family with measurable coordinates whose index type is equivalent to ℕ is conditionally i.i.d.

TauCeti.Probability.conditionallyIID_of_exchangeableFamily_of_equiv_nat.{u_1, u_2, u_3}
  {Ω : Type u_1} {α : Type u_2} {ι : Type u_3} [MeasurableSpace Ω] [MeasurableSpace α]
  [StandardBorelSpace α] [Nonempty α] {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsFiniteMeasure μ] {X : ι → Ω → α}
  (hX : TauCeti.Probability.ExchangeableFamily μ X) (e : ι ≃ ℕ)
  (hX_meas : ∀ (i : ι), Measurable (X i)) : TauCeti.Probability.ConditionallyIID μ X
Informally uses
Lean

Formalized in Tau Ceti as TauCeti.Probability.conditionallyIID_of_exchangeableFamily_of_equiv_nat.

Sources
LeanTauCeti.Probability.conditionallyIID_of_exchangeableFamily_of_equiv_nat
Used by 1
Used byDe Finetti's theorem

TheoremDoob's maximal inequality in continuous time#

Let f be a nonnegative submartingale indexed by a densely ordered separable time set, such as ℝ≥0, whose paths are almost surely right-continuous at every time before T. Then ε P(∃ t ≤ T, ε < f_t) ≤ E[f_T].

MeasureTheory.Submartingale.mul_measure_exists_le_lt_le.{u_1, u_2} {Ω : Type u_1} {ι : Type u_2}
  {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [LinearOrder ι]
  {ℱ : MeasureTheory.Filtration ι m0} {f : ι → Ω → ℝ} [TopologicalSpace ι] [OrderTopology ι]
  [DenselyOrdered ι] [TopologicalSpace.SeparableSpace ι] [MeasureTheory.IsFiniteMeasure μ]
  (hf : MeasureTheory.Submartingale f ℱ μ) (hnonneg : 0 ≤ f) {T : ι}
  (hcont : ∀ᵐ (ω : Ω) ∂μ, ∀ t < T, ContinuousWithinAt (fun u => f u ω) (Set.Ioi t) t) (ε : NNReal) :
  ↑ε * μ {ω | ∃ t ≤ T, ↑ε < f t ω} ≤ ENNReal.ofReal (∫ (ω : Ω), f T ω ∂μ)
Lean

Formalized in Tau Ceti as MeasureTheory.Submartingale.mul_measure_exists_le_lt_le.

Other forms

Doob's maximal inequality over a finite set of times. Formalized in Tau Ceti as MeasureTheory.Submartingale.mul_measure_exists_mem_le_le.

MeasureTheory.Submartingale.mul_measure_exists_mem_le_le.{u_1, u_2} {Ω : Type u_1} {ι : Type u_2}
  {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [LinearOrder ι]
  {ℱ : MeasureTheory.Filtration ι m0} {f : ι → Ω → ℝ} [MeasureTheory.IsFiniteMeasure μ]
  (hf : MeasureTheory.Submartingale f ℱ μ) (hnonneg : 0 ≤ f) (ε : NNReal) {F : Finset ι} {T : ι}
  (hF : ∀ t ∈ F, t ≤ T) : ↑ε * μ {ω | ∃ t ∈ F, ↑ε ≤ f t ω} ≤ ENNReal.ofReal (∫ (ω : Ω), f T ω ∂μ)
Sources
LeanMeasureTheory.Submartingale.mul_measure_exists_le_lt_le · MeasureTheory.Submartingale.mul_measure_exists_mem_le_le

TheoremThe Efron–Stein inequality on Measure.pi over a finite index type#

for a square integrable measurable function f of independent coordinates, the variance of f is at most the sum over i of the average variance of f in coordinate i with the other coordinates frozen.

TauCeti.Probability.efronStein.{u, u_1} {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u}
  [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i))
  [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {f : ((i : ι) → α i) → ℝ}
  (hf : Measurable f) (hL : MeasureTheory.MemLp f 2 (MeasureTheory.Measure.pi μ)) :
  ProbabilityTheory.evariance f (MeasureTheory.Measure.pi μ) ≤
    ∑ i,
      ∫⁻ (x : (i : ι) → α i),
        ProbabilityTheory.evariance (fun y => f (Function.update x i y))
          (μ i) ∂MeasureTheory.Measure.pi μ
Lean

Formalized in Tau Ceti as TauCeti.Probability.efronStein.

Sources
LeanTauCeti.Probability.efronStein
Uses 1
Proof usesHölder's inequality for the integral of a product

TheoremThe elementary renewal theorem#

For a probability measure μ on ℝ≥0 other than the point mass at zero, the renewal function satisfies m t / t → (𝔼 μ)⁻¹ as t → ∞, where the reciprocal of the extended mean is taken before conversion to a real number, so that the limit is zero for infinite mean.

MeasureTheory.Measure.tendsto_renewalFunction_div (μ : MeasureTheory.Measure NNReal)
  [MeasureTheory.IsProbabilityMeasure μ] (hμ : μ {0} < 1) :
  Filter.Tendsto (fun t => (μ.renewalFunction t).toReal / ↑t) Filter.atTop
    (nhds (∫⁻ (x : NNReal), ↑x ∂μ)⁻¹.toReal)
Lean

Formalized in Tau Ceti as MeasureTheory.Measure.tendsto_renewalFunction_div.

Other forms

The elementary renewal theorem, on any realization of the increments. Formalized in Tau Ceti as TauCeti.Probability.tendsto_integral_renewalCountNat_div.

TauCeti.Probability.tendsto_integral_renewalCountNat_div.{u_1} {Ω : Type u_1} [MeasurableSpace Ω]
  {P : MeasureTheory.Measure Ω} {T : ℕ → Ω → NNReal} (hT : ∀ (n : ℕ), Measurable (T n))
  (hindep : ProbabilityTheory.iIndepFun T P)
  (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P)
  (hzero : P {ω | T 0 ω = 0} < 1) :
  Filter.Tendsto (fun t => (∫ (ω : Ω), ↑(TauCeti.Probability.renewalCountNat T t ω) ∂P) / ↑t)
    Filter.atTop (nhds (∫⁻ (ω : Ω), ↑(T 0 ω) ∂P)⁻¹.toReal)
Sources
LeanMeasureTheory.Measure.tendsto_renewalFunction_div · TauCeti.Probability.tendsto_integral_renewalCountNat_div
Uses 7
Statement usesTauCeti.Probability.renewalCount
Proof usesChernoff bound for the arrival times · De la Vallée Poussin's criterion · Finite moments of the renewal counts · Finiteness of the renewal counts · Nonexplosion of a renewal process · TauCeti.Probability.renewalCount_eq_natCast_iff

TheoremGirsanov's theorem for a constant drift#

If W is a Brownian motion relative to ℱ under P, then t ↦ W t - θ min(t, T) is a Brownian motion relative to ℱ under the measure P.tilted (θ * W T ·), whose density with respect to P is exp (θ W_T - θ² T / 2).

TauCeti.Probability.IsFilteredPreBrownianReal.sub_mul_min_tilted_mul_eval.{u_1} {Ω : Type u_1}
  {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ℱ : MeasureTheory.Filtration NNReal mΩ}
  {W : NNReal → Ω → ℝ} (hW : TauCeti.Probability.IsFilteredPreBrownianReal ℱ W P) (θ : ℝ)
  (T : NNReal) :
  TauCeti.Probability.IsFilteredPreBrownianReal ℱ (fun t ω => W t ω - θ * ↑(min t T))
    (P.tilted fun ω => θ * W T ω)
Lean

Formalized in Tau Ceti as TauCeti.Probability.IsFilteredPreBrownianReal.sub_mul_min_tilted_mul_eval.

Other forms

Girsanov's theorem for a constant drift, with continuous paths. Formalized in Tau Ceti as TauCeti.Probability.IsFilteredPreBrownianReal.isBrownianReal_sub_mul_min_tilted_mul_eval.

TauCeti.Probability.IsFilteredPreBrownianReal.isBrownianReal_sub_mul_min_tilted_mul_eval.{u_1}
  {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  {ℱ : MeasureTheory.Filtration NNReal mΩ} {W : NNReal → Ω → ℝ}
  (hW : TauCeti.Probability.IsFilteredPreBrownianReal ℱ W P)
  (hcont : ∀ᵐ (ω : Ω) ∂P, Continuous fun x => W x ω) (θ : ℝ) (T : NNReal) :
  ProbabilityTheory.IsBrownianReal (fun t ω => W t ω - θ * ↑(min t T)) (P.tilted fun ω => θ * W T ω)
Sources
LeanTauCeti.Probability.IsFilteredPreBrownianReal.sub_mul_min_tilted_mul_eval · TauCeti.Probability.IsFilteredPreBrownianReal.isBrownianReal_sub_mul_min_tilted_mul_eval
Uses 1
Proof usesTauCeti.Probability.setIntegral_exp_mul_gaussianReal

TheoremLévy's downward theorem specializes correctly to an eventually constant filtration#

Run the flagship MeasureTheory.tendsto_ae_condExp_iInf on an antitone filtration that is constant from index N on, then collapse its limit through condExp_iInf_eq_of_eventually_const. The a.e. limit it delivers is μ[f | 𝔽 N] — exactly the value the sequence already reaches by the elementary tendsto_condExp_of_eventually_const. The general and elementary computations agree.

TauCeti.Probability.tendsto_ae_condExp_of_eventually_const.{u_1} {Ω : Type u_1} [MeasurableSpace Ω]
  {μ : MeasureTheory.Measure Ω} {𝔽 : ℕ → MeasurableSpace Ω} [MeasureTheory.IsFiniteMeasure μ]
  (h_anti : Antitone 𝔽) (h_le0 : 𝔽 0 ≤ inferInstance) {N : ℕ}
  (h_const : ∀ (n : ℕ), N ≤ n → 𝔽 n = 𝔽 N) (f : Ω → ℝ) :
  ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun n => μ[f | 𝔽 n] ω) Filter.atTop (nhds (μ[f | 𝔽 N] ω))
Lean

Formalized in Tau Ceti as TauCeti.Probability.tendsto_ae_condExp_of_eventually_const.

Sources
LeanTauCeti.Probability.tendsto_ae_condExp_of_eventually_const

TheoremThe mean ergodic theorem for conditional expectations#

The Birkhoff time averages of an integrable square-integrable observable converge in L² to its conditional expectation given the invariant σ-algebra of the transformation.

TauCeti.Probability.tendsto_eLpNorm_birkhoffAverage_sub_condExp.{u_1} {Ω : Type u_1}
  [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} (T : Ω → Ω)
  (hT : MeasureTheory.MeasurePreserving T μ μ) [MeasureTheory.SigmaFinite (μ.trim ⋯)] {f : Ω → ℝ}
  (hf : MeasureTheory.MemLp f 2 μ) (hf_int : MeasureTheory.Integrable f μ) :
  Filter.Tendsto
    (fun n =>
      MeasureTheory.eLpNorm (birkhoffAverage ℝ T f n - μ[f | MeasurableSpace.invariants T]) 2 μ)
    Filter.atTop (nhds 0)
Lean

Formalized in Tau Ceti as TauCeti.Probability.tendsto_eLpNorm_birkhoffAverage_sub_condExp.

Sources
LeanTauCeti.Probability.tendsto_eLpNorm_birkhoffAverage_sub_condExp
Used by 1
Used byDe Finetti's theorem

TheoremThe renewal central limit theorem#

Let T 0, T 1, … be independent, identically distributed nonnegative waiting times with nonzero variance σ² = Var[T 0; P] and expectation μ = P[T 0]. As t → ∞ in ℝ≥0, the standardized renewal count ((N_t : ℝ) - t / μ) / (σ * √(t / μ ^ 3)) converges in distribution to any standard normal random variable Z. Precomposing with MeasureTheory.TendstoInDistribution.comp_tendsto gives convergence along any time family (in particular any sequence) tending to atTop.

TauCeti.Probability.tendstoInDistribution_renewalCountNat_sub_div.{u_1, u_2} {Ω : Type u_1}
  {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P'] {T : ℕ → Ω → NNReal} {Z : Ω' → ℝ}
  (hZ : ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 1) P')
  (hindep : ProbabilityTheory.iIndepFun T P)
  (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P)
  (hvar : ProbabilityTheory.variance (fun ω => ↑(T 0 ω)) P ≠ 0) :
  MeasureTheory.TendstoInDistribution
    (fun t ω =>
      (↑(TauCeti.Probability.renewalCountNat T t ω) - ↑t / ∫ (x : Ω), (fun ω => ↑(T 0 ω)) x ∂P) /
        (√(ProbabilityTheory.variance (fun ω => ↑(T 0 ω)) P) *
          √(↑t / (∫ (x : Ω), (fun ω => ↑(T 0 ω)) x ∂P) ^ 3)))
    Filter.atTop Z (fun x => P) P'
Lean

Formalized in Tau Ceti as TauCeti.Probability.tendstoInDistribution_renewalCountNat_sub_div.

Other forms

The renewal central limit theorem (extended-mean formulation). Formalized in Tau Ceti as TauCeti.Probability.tendstoInDistribution_renewalCountNat_sub_div_toReal_lintegral.

TauCeti.Probability.tendstoInDistribution_renewalCountNat_sub_div_toReal_lintegral.{u_1, u_2}
  {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω']
  {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {P' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure P'] {T : ℕ → Ω → NNReal}
  {Z : Ω' → ℝ} (hZ : ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 1) P')
  (hindep : ProbabilityTheory.iIndepFun T P)
  (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P)
  (hvar : ProbabilityTheory.variance (fun ω => ↑(T 0 ω)) P ≠ 0) :
  MeasureTheory.TendstoInDistribution
    (fun t ω =>
      (↑(TauCeti.Probability.renewalCountNat T t ω) - ↑t / (∫⁻ (ω : Ω), ↑(T 0 ω) ∂P).toReal) /
        (√(ProbabilityTheory.variance (fun ω => ↑(T 0 ω)) P) *
          √(↑t / (∫⁻ (ω : Ω), ↑(T 0 ω) ∂P).toReal ^ 3)))
    Filter.atTop Z (fun x => P) P'

The renewal central limit theorem on the real time axis. Formalized in Tau Ceti as TauCeti.Probability.tendstoInDistribution_renewalCountNat_toNNReal_sub_div.

TauCeti.Probability.tendstoInDistribution_renewalCountNat_toNNReal_sub_div.{u_1, u_2} {Ω : Type u_1}
  {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {P : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure P] {P' : MeasureTheory.Measure Ω'}
  [MeasureTheory.IsProbabilityMeasure P'] {T : ℕ → Ω → NNReal} {Z : Ω' → ℝ}
  (hZ : ProbabilityTheory.HasLaw Z (ProbabilityTheory.gaussianReal 0 1) P')
  (hindep : ProbabilityTheory.iIndepFun T P)
  (hid : ∀ (n : ℕ), ProbabilityTheory.IdentDistrib (T n) (T 0) P P)
  (hvar : ProbabilityTheory.variance (fun ω => ↑(T 0 ω)) P ≠ 0) :
  MeasureTheory.TendstoInDistribution
    (fun t ω =>
      (↑(TauCeti.Probability.renewalCountNat T t.toNNReal ω) -
          t / ∫ (x : Ω), (fun ω => ↑(T 0 ω)) x ∂P) /
        (√(ProbabilityTheory.variance (fun ω => ↑(T 0 ω)) P) *
          √(t / (∫ (x : Ω), (fun ω => ↑(T 0 ω)) x ∂P) ^ 3)))
    Filter.atTop Z (fun x => P) P'
Sources
LeanTauCeti.Probability.tendstoInDistribution_renewalCountNat_sub_div · TauCeti.Probability.tendstoInDistribution_renewalCountNat_sub_div_toReal_lintegral · TauCeti.Probability.tendstoInDistribution_renewalCountNat_toNNReal_sub_div
Uses 3
Statement usesTauCeti.Probability.renewalCount
Proof usesNonexplosion of a renewal process · TauCeti.Probability.renewalCount_eq_natCast_iff

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.