Gumbel Distribution and Transformation to Exponential

This file contains lemmas about the Gumbel distribution and its transformation to the exponential distribution.

theorem gumbel_exp_neg_cdf_calc (y : ℝ) (hy : 0 < y) : 1 - gumbel_cdf (-Real.log y) = 1 - Real.exp (-y)

theorem gumbel_cdf_continuous : Continuous gumbel_cdf

theorem set_Ioc_eq_diff {Ω : Type u_1} (Y : Ω → ℝ) (a b : ℝ) : {ω : Ω | a < Y ω ∧ Y ω ≤ b} = {ω : Ω | Y ω ≤ b} \ {ω : Ω | Y ω ≤ a}

theorem cdf_mono {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Y : Ω → ℝ) (F : ℝ → ℝ) (h_cdf : ∀ (x : ℝ), μ {ω : Ω | Y ω ≤ x} = ENNReal.ofReal (F x)) (hF_nonneg : ∀ (x : ℝ), 0 ≤ F x) : Monotone F

theorem measure_Ioc_eq_cdf_sub {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Y : Ω → ℝ) (F : ℝ → ℝ) (h_meas : Measurable Y) (h_cdf : ∀ (x : ℝ), μ {ω : Ω | Y ω ≤ x} = ENNReal.ofReal (F x)) (hF_nonneg : ∀ (x : ℝ), 0 ≤ F x) (a b : ℝ) (hab : a < b) : μ {ω : Ω | a < Y ω ∧ Y ω ≤ b} = ENNReal.ofReal (F b - F a)

theorem measure_Ioc_eq_measure_le_sub_measure_le {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Y : Ω → ℝ) (h_meas : Measurable Y) (a b : ℝ) (hab : a < b) (h_finite : μ {ω : Ω | Y ω ≤ a} ≠ ⊤) : μ {ω : Ω | a < Y ω ∧ Y ω ≤ b} = μ {ω : Ω | Y ω ≤ b} - μ {ω : Ω | Y ω ≤ a}

theorem measure_singleton_eq_zero_of_continuous_cdf {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Y : Ω → ℝ) (F : ℝ → ℝ) (h_meas : Measurable Y) (y : ℝ) (h_cdf : ∀ (x : ℝ), μ {ω : Ω | Y ω ≤ x} = ENNReal.ofReal (F x)) (hF_nonneg : ∀ (x : ℝ), 0 ≤ F x) (h_cont : ContinuousAt F y) : μ {ω : Ω | Y ω = y} = 0

theorem cdf_diff_tendsto_zero (F : ℝ → ℝ) (y : ℝ) (h_cont : ContinuousAt F y) : Filter.Tendsto (fun (n : ℕ) => F y - F (y - 1 / (↑n + 1))) Filter.atTop (nhds 0)

theorem gumbel_measure_singleton_zero {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Y : Ω → ℝ) (h_meas : Measurable Y) (hY : ∀ (x : ℝ), μ {ω : Ω | Y ω ≤ x} = ENNReal.ofReal (gumbel_cdf x)) (y : ℝ) : μ {ω : Ω | Y ω = y} = 0

theorem gumbel_prob_ge {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → ℝ) (h_meas : Measurable Y) (hY : ∀ (x : ℝ), μ {ω : Ω | Y ω ≤ x} = ENNReal.ofReal (gumbel_cdf x)) (y : ℝ) : μ {ω : Ω | Y ω ≥ y} = ENNReal.ofReal (1 - gumbel_cdf y)

theorem gumbel_to_exp_cdf {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → ℝ) (h_meas : Measurable Y) (hY : ∀ (x : ℝ), μ {ω : Ω | Y ω ≤ x} = ENNReal.ofReal (gumbel_cdf x)) (x : ℝ) : μ {ω : Ω | Real.exp (-Y ω) ≤ x} = ENNReal.ofReal (if 0 ≤ x then 1 - Real.exp (-x) else 0)

theorem gumbel_to_exp_cdf_pos {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Ω → ℝ) (h_meas : Measurable Y) (hY : ∀ (x : ℝ), μ {ω : Ω | Y ω ≤ x} = ENNReal.ofReal (gumbel_cdf x)) (x : ℝ) (hx : 0 < x) : μ {ω : Ω | Real.exp (-Y ω) ≤ x} = ENNReal.ofReal (1 - Real.exp (-x))

theorem gumbel_to_exp_cdf_nonpos {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Y : Ω → ℝ) (x : ℝ) (hx : x ≤ 0) : μ {ω : Ω | Real.exp (-Y ω) ≤ x} = 0

theorem exp_neg_Y_is_exp_grid {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Y : Edge → Ω → ℝ) (hY : IsGumbelGrid μ Y) (h_meas : ∀ (e : Edge), Measurable (Y e)) : ProbabilityTheory.iIndepFun (fun (e : Edge) (ω : Ω) => Real.exp (-Y e ω)) μ ∧ ∀ (e : Edge) (x : ℝ), μ {ω : Ω | Real.exp (-Y e ω) ≤ x} = ENNReal.ofReal (if 0 ≤ x then 1 - Real.exp (-x) else 0)