The extremes of an independent identically distributed family

Let X : ι → Ω → ℝ be an independent family over a nonempty finite index type, all of whose members have the same law μ. This file computes the law of the two extremes of the family: the maximum Finset.univ.sup' Finset.univ_nonempty fun i => X i ω and the minimum Finset.univ.inf' Finset.univ_nonempty fun i => X i ω. Writing d = Fintype.card ι, the cumulative distribution functions are (cdf μ x) ^ d and 1 - (1 - cdf μ x) ^ d.

Both extremes are taken over Finset.univ together with its nonemptiness proof, so neither formula acquires the default value that an empty family would force on a Finset.sup or a Finset.inf: d = 0 never occurs.

One event identity does the work. The maximum is at most x exactly when every member is (Finset.sup'_le_iff), and x is below the minimum exactly when it is below every member (Finset.lt_inf'_iff). Independence turns each of those intersections into a product of d equal factors, which is where the two powers come from. The minimum is then read off its complementary event, which is why its formula is the one with the two subtractions.

cdf_min_iid specialises to the exponential family as hasLaw_min_iid_expMeasure: the minimum of d i.i.d. exponentials of rate r is exponential of rate d * r.

Main results

• TauCeti.Probability.measure_setOf_max_le_iid, TauCeti.Probability.measureReal_setOf_max_le_iid — the maximum is at most x with probability (cdf μ x) ^ d;
• TauCeti.Probability.measure_setOf_lt_min_iid, TauCeti.Probability.measureReal_setOf_min_le_iid — the minimum exceeds x with probability (1 - cdf μ x) ^ d, hence is at most x with probability 1 - (1 - cdf μ x) ^ d;
• TauCeti.Probability.cdf_max_iid, TauCeti.Probability.cdf_min_iid — the same two formulas for the laws of the two extremes.

Only the two extremes are treated; a general theory of order statistics is not.

theorem TauCeti.Probability.measure_setOf_max_le_iid {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : ι → Ω → ℝ} (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) μ P) (x : ℝ) : P {ω : Ω | (Finset.univ.sup' ⋯ fun (i : ι) => X i ω) ≤ x} = μ (Set.Iic x) ^ Fintype.card ι

The maximum of an independent identically distributed finite family is at most x with probability the Fintype.card ι-th power of the common lower-tail probability.

theorem TauCeti.Probability.measure_setOf_lt_min_iid {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : ι → Ω → ℝ} (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) μ P) (x : ℝ) : P {ω : Ω | x < Finset.univ.inf' ⋯ fun (i : ι) => X i ω} = μ (Set.Ioi x) ^ Fintype.card ι

The minimum of an independent identically distributed finite family exceeds x with probability the Fintype.card ι-th power of the common upper-tail probability.

theorem TauCeti.Probability.measureReal_setOf_max_le_iid {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : ι → Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) μ P) (x : ℝ) : P.real {ω : Ω | (Finset.univ.sup' ⋯ fun (i : ι) => X i ω) ≤ x} = ↑(ProbabilityTheory.cdf μ) x ^ Fintype.card ι

The real-valued form of TauCeti.Probability.measure_setOf_max_le_iid: the maximum of d independent identically distributed variables has cumulative distribution function (cdf μ x) ^ d.

theorem TauCeti.Probability.measureReal_setOf_lt_min_iid {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : ι → Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) μ P) (x : ℝ) : P.real {ω : Ω | x < Finset.univ.inf' ⋯ fun (i : ι) => X i ω} = (1 - ↑(ProbabilityTheory.cdf μ) x) ^ Fintype.card ι

The real-valued form of TauCeti.Probability.measure_setOf_lt_min_iid: the minimum of d independent identically distributed variables exceeds x with probability (1 - cdf μ x) ^ d.

theorem TauCeti.Probability.measureReal_setOf_min_le_iid {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : ι → Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) μ P) (x : ℝ) : P.real {ω : Ω | (Finset.univ.inf' ⋯ fun (i : ι) => X i ω) ≤ x} = 1 - (1 - ↑(ProbabilityTheory.cdf μ) x) ^ Fintype.card ι

The minimum of d independent identically distributed variables has cumulative distribution function 1 - (1 - cdf μ x) ^ d.

theorem TauCeti.Probability.cdf_max_iid {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : ι → Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) μ P) (x : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (ω : Ω) => Finset.univ.sup' ⋯ fun (i : ι) => X i ω) P)) x = ↑(ProbabilityTheory.cdf μ) x ^ Fintype.card ι

The law of the maximum of d independent identically distributed variables, in cumulative distribution function form.

theorem TauCeti.Probability.cdf_min_iid {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure ℝ} {X : ι → Ω → ℝ} [MeasureTheory.IsProbabilityMeasure μ] (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) μ P) (x : ℝ) : ↑(ProbabilityTheory.cdf (MeasureTheory.Measure.map (fun (ω : Ω) => Finset.univ.inf' ⋯ fun (i : ι) => X i ω) P)) x = 1 - (1 - ↑(ProbabilityTheory.cdf μ) x) ^ Fintype.card ι

The law of the minimum of d independent identically distributed variables, in cumulative distribution function form.