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.

As an application, the minimum of a finite independent identically distributed exponential family is again exponential, with the rates added: hasLaw_min_iid_expMeasure. This is the d-fold form of TauCeti.Probability.hasLaw_min_expMeasure_of_indepFun, which handles two independent exponentials of possibly different rates.

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;
• TauCeti.Probability.hasLaw_min_iid_expMeasure — the minimum of d independent exponentials of rate r is exponential of rate d * r.

A general theory of order statistics is outside the scope of the roadmap target below.

References

• Roadmap: TauCetiRoadmap/StandardDistributions/README.md, Layer 4, item 6, Finite minima and maxima.

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.

theorem TauCeti.Probability.hasLaw_min_iid_expMeasure {Ω : Type u_1} {ι : Type u_2} {mΩ : MeasurableSpace Ω} [Fintype ι] [Nonempty ι] {P : MeasureTheory.Measure Ω} {X : ι → Ω → ℝ} {r : ℝ} (hr : 0 < r) (hindep : ProbabilityTheory.iIndepFun X P) (hlaw : ∀ (i : ι), ProbabilityTheory.HasLaw (X i) (ProbabilityTheory.expMeasure r) P) : ProbabilityTheory.HasLaw (fun (ω : Ω) => Finset.univ.inf' ⋯ fun (i : ι) => X i ω) (ProbabilityTheory.expMeasure (↑(Fintype.card ι) * r)) P

The minimum of d independent exponential variables of a common positive rate r is exponential of rate d * r. This is the d-fold form of TauCeti.Probability.hasLaw_min_expMeasure_of_indepFun, which allows two different rates.