awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (hypothesis)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
hQ :
  ∀ (i : Set ℕ) (i_1 : i ⊆ Iio N),
    ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) <
      HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i_2 ∈ i, thickening (ε / 3) (Es i_2)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3))
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)
have hQ₁ : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
  HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
    (ENNReal.ofReal (ε / 3))
Tactic: specialize hQ _ (show JB ⊆ Iio N from fun _ h ↦ h.2)
Cleared hypotheses: hQ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
hQ :
  ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3))
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞)
      (((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (((↑(ofMeasure P).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)
have apply : HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3)) +
    ENNReal.ofReal (ε / 3) ≤
  HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
    (ENNReal.ofReal δ)
Tactic: apply (add_le_add hQ.le hN.le).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
hQ :
  ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3))
⊢ HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
        (ENNReal.ofReal (ε / 3)) +
      ENNReal.ofReal (ε / 3) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)
have rw : HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
    (ENNReal.ofReal (2 * (ε / 3))) ≤
  HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
    (ENNReal.ofReal δ)
Tactic: rw [add_assoc, ← ENNReal.ofReal_add third_ε_pos.le third_ε_pos.le, ← two_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LevyProkhorovMetric (goal)
Goal:
Ω : Type u_1
inst : PseudoMetricSpace Ω
inst_1 : MeasurableSpace Ω
inst_2 : OpensMeasurableSpace Ω
inst_3 : SeparableSpace Ω
P : ProbabilityMeasure Ω
ε : ℝ
ε_pos : ε > 0
third_ε_pos : 0 < ε / 3
third_ε_pos' : 0 < ENNReal.ofReal (ε / 3)
Es : ℕ → Set Ω
Es_mble : ∀ (n : ℕ), MeasurableSet (Es n)
Es_bdd : ∀ (n : ℕ), Bornology.IsBounded (Es n)
Es_diam : ∀ (n : ℕ), diam (Es n) ≤ ε / 3
Es_cover : Eq.{u_1 + 1} (α := Set Ω) (⋃ (n : ℕ), Es n) univ
Es_disjoint : Pairwise fun (n m : ℕ) ↦ Disjoint (Es n) (Es m)
N : ℕ
hN : ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ j ∈ Iio N, Es j)ᶜ < ENNReal.ofReal (ε / 3)
Js_finite : Set.Finite (α := Set ℕ) {J : Set ℕ | J ⊆ Iio N}
Gs : Set (Set Ω) := (fun (J : Set ℕ) ↦ thickening (ε / 3) (⋃ j ∈ J, Es j)) '' {J : Set ℕ | J ⊆ Iio N}
Gs_open :
  ∀ (J : Set ℕ), IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (thickening (ε / 3) (⋃ j ∈ J, Es j))
mem_nhds_P :
  ∀ (G : Set Ω) (G_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] G),
    {Q : ProbabilityMeasure Ω |
        ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G <
          HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) G : ℝ≥0∞) (ENNReal.ofReal (ε / 3))} ∈
      𝓝 P
Q : ProbabilityMeasure Ω
δ : ℝ
B : Set Ω
δ_gt : 2 * (ε / 3) < δ
h : MeasurableSet B
JB : Set ℕ := {i : ℕ | (B ∩ Es i).Nonempty ∧ i ∈ Iio N}
B_subset : B ⊆ (⋃ i ∈ JB, thickening (ε / 3) (Es i)) ∪ (⋃ j ∈ Iio N, Es j)ᶜ
subset_thickB : ⋃ i ∈ JB, thickening (ε / 3) (Es i) ⊆ thickening δ B
hQ :
  ((↑P : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) <
    HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (ε / 3))
⊢ HAdd.hAdd (α := ℝ≥0∞) (((↑Q : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (⋃ i ∈ JB, thickening (ε / 3) (Es i)) : ℝ≥0∞)
      (ENNReal.ofReal (2 * (ε / 3))) ≤
    HAdd.hAdd (α := ℝ≥0∞) (((↑(ofMeasure Q).toMeasure : Measure Ω) : (a : Set Ω) → ℝ≥0∞) (thickening δ B) : ℝ≥0∞)
      (ENNReal.ofReal δ)
have apply : 2 * (ε / 3) ≤ δ
Tactic: apply add_le_add (measure_mono subset_thickB) (ofReal_le_ofReal _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
⊢ llr μ μ =ᶠ[ae μ] 0
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv μ x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ llr μ μ x = 0 x) x} x}
    a
Tactic: filter_upwards [μ.rnDeriv_self] with a ha using by simp [llr, ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SigmaFinite μ
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ μ.rnDeriv μ x = (fun (x : α) ↦ (1 : ℝ≥0∞)) x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ llr μ μ x = 0 x) x} x}
      a
⊢ llr μ μ =ᶠ[ae μ] 0
have h₁ : ∀ (a : α), μ.rnDeriv μ a = 1 → llr μ μ a = 0 a
Tactic: filter_upwards [μ.rnDeriv_self] with a ha using by simp [llr, ha]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (llr μ ν x)) fun (x : α) ↦
    if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
have h : ∀ (x : α) (hx : μ.rnDeriv ν x < ∞), rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
Tactic: filter_upwards [Measure.rnDeriv_lt_top μ ν] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
have pos : ∀ (h_zero : μ.rnDeriv ν x = 0), rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
Tactic: by_cases h_zero : μ.rnDeriv ν x = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
pos : ∀ (h_zero : μ.rnDeriv ν x = 0), rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
have neg : ∀ (h_zero : ¬μ.rnDeriv ν x = 0), rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
Tactic: by_cases h_zero : μ.rnDeriv ν x = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
x : α
hx : μ.rnDeriv ν x < ∞
h_zero : ¬μ.rnDeriv ν x = 0
⊢ rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
have neg : 0 < (μ.rnDeriv ν x).toReal
Tactic: rw [llr, exp_log, if_neg h_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (llr μ ν x)) fun (x : α) ↦ (μ.rnDeriv ν x).toReal
have h : ∀ (x : α) (hx_eq : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal)
  (hx_pos : 0 < μ.rnDeriv ν x), rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
Tactic: filter_upwards [hμν.ae_le (exp_llr μ ν), Measure.rnDeriv_pos hμν] with x hx_eq hx_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
x : α
hx_eq : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
⊢ rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
have h : (if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal) = (μ.rnDeriv ν x).toReal
Tactic: rw [hx_eq, if_neg hx_pos.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
x : α
hx_eq : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
h : (if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal) = (μ.rnDeriv ν x).toReal
⊢ rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
have h₁ : (μ.rnDeriv ν x).toReal = (μ.rnDeriv ν x).toReal
Tactic: rw [hx_eq, if_neg hx_pos.ne']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (llr μ ν x)) fun (x : α) ↦ (μ.rnDeriv ν x).toReal
have h : ∀ (x : α) (hx : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal)
  (hx_pos : 0 < μ.rnDeriv ν x), rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
Tactic: filter_upwards [exp_llr μ ν, Measure.rnDeriv_pos' hμν] with x hx hx_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : rexp (llr μ ν x) = if μ.rnDeriv ν x = 0 then 1 else (μ.rnDeriv ν x).toReal
hx_pos : 0 < μ.rnDeriv ν x
⊢ rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
have h : ∀ (hx : rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal) (hx_pos : 0 < μ.rnDeriv ν x),
  rexp (llr μ ν x) = (μ.rnDeriv ν x).toReal
Tactic: rwa [if_neg hx_pos.ne'] at hx
Cleared hypotheses: hx, hx_pos
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ -llr μ ν =ᶠ[ae μ] llr ν μ
have h : ∀ (x : α) (hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x), (-llr μ ν) x = llr ν μ x
Tactic: filter_upwards [Measure.inv_rnDeriv hμν] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (μ.rnDeriv ν)⁻¹ x = ν.rnDeriv μ x
⊢ (-llr μ ν) x = llr ν μ x
have h : log (μ.rnDeriv ν x)⁻¹.toReal = log (ν.rnDeriv μ x).toReal
Tactic: rw [Pi.neg_apply, llr, llr, ← log_inv, ← ENNReal.toReal_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (-llr μ ν x)) fun (x : α) ↦ (ν.rnDeriv μ x).toReal
have h : ∀ (x : α) (hx : (-llr μ ν) x = llr ν μ x) (hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal),
  rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
Tactic: filter_upwards [neg_llr hμν, exp_llr_of_ac' ν μ hμν] with x hx hx_exp_log
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : (-llr μ ν) x = llr ν μ x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
have hx₁ : -llr μ ν x = llr ν μ x
Tactic: rw [Pi.neg_apply] at hx
Cleared hypotheses: hx, hx_exp_log
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : μ ≪ ν
x : α
hx : -llr μ ν x = llr ν μ x
hx_exp_log h : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
have h₁ : (ν.rnDeriv μ x).toReal = (ν.rnDeriv μ x).toReal
Tactic: rw [hx, hx_exp_log]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ rexp (-llr μ ν x)) fun (x : α) ↦ (ν.rnDeriv μ x).toReal
have h : ∀ (x : α) (hx : (-llr ν μ) x = llr μ ν x) (hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal),
  rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
Tactic: filter_upwards [neg_llr hμν, exp_llr_of_ac ν μ hμν] with x hx hx_exp_log
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : (-llr ν μ) x = llr μ ν x
hx_exp_log : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
have hx₁ : llr ν μ x = -llr μ ν x
Tactic: rw [Pi.neg_apply, neg_eq_iff_eq_neg] at hx
Cleared hypotheses: hx, hx_exp_log
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hμν : ν ≪ μ
x : α
hx : llr ν μ x = -llr μ ν x
hx_exp_log h : rexp (llr ν μ x) = (ν.rnDeriv μ x).toReal
⊢ rexp (-llr μ ν x) = (ν.rnDeriv μ x).toReal
have h₁ : (ν.rnDeriv μ x).toReal = (ν.rnDeriv μ x).toReal
Tactic: rw [← hx, hx_exp_log]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((c • μ).rnDeriv ν x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal + log c.toReal
have h : (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν
Tactic: have h := Measure.rnDeriv_smul_left_of_ne_top μ ν hc_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((c • μ).rnDeriv ν x).toReal) fun (x : α) ↦
    log (μ.rnDeriv ν x).toReal + log c.toReal
have h₁ : ∀ (x : α) (hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x) (hx_pos : 0 < μ.rnDeriv ν x)
  (hx_ne_top : μ.rnDeriv ν x < ∞), log ((c • μ).rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
Tactic: filter_upwards [hμν.ae_le h, Measure.rnDeriv_pos hμν, hμν.ae_le (Measure.rnDeriv_lt_top μ ν)]
    with x hx_eq hx_pos hx_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log ((c • μ).rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
have h₁ : log ((c • μ.rnDeriv ν) x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
Tactic: rw [hx_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log ((c • μ.rnDeriv ν) x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
have h₁ : log (c.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal + log c.toReal
Tactic: simp only [Pi.smul_apply, smul_eq_mul, ENNReal.toReal_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ log (c.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal + log c.toReal
have h₁ : log c.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
Tactic: rw [log_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
h₁ : log c.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
⊢ log (c.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal + log c.toReal
have h₂ : c.toReal ≠ 0
Tactic: rw [log_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
h₁ : log c.toReal + log (μ.rnDeriv ν x).toReal = log (μ.rnDeriv ν x).toReal + log c.toReal
h₂ : c.toReal ≠ 0
⊢ log (c.toReal * (μ.rnDeriv ν x).toReal) = log (μ.rnDeriv ν x).toReal + log c.toReal
have h₃ : (μ.rnDeriv ν x).toReal ≠ 0
Tactic: rw [log_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.LogLikelihoodRatio (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
inst_1 : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
c : ℝ≥0∞
hc : c ≠ 0
hc_ne_top : c ≠ ∞
h : (c • μ).rnDeriv ν =ᶠ[ae ν] c • μ.rnDeriv ν
x : α
hx_eq : (c • μ).rnDeriv ν x = (c • μ.rnDeriv ν) x
hx_pos : 0 < μ.rnDeriv ν x
hx_ne_top : μ.rnDeriv ν x < ∞
⊢ c.toReal ≠ 0
have h₁ : c ≠ 0 ∧ c ≠ ∞
Tactic: rw [ENNReal.toReal_ne_zero]