awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a : α
⊢ (ENNReal.ofReal (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ)).toReal = rexp (f a) / ∫ (a : α), rexp (f a) ∂μ
have a₁ : 0 ≤ rexp (f a) / ∫ (a : α), rexp (f a) ∂μ
Tactic: rw [ENNReal.toReal_ofReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f x) • g x))
      μ
have a : ∀ (a : α),
  (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ) • g a = HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f a) • g a)
Tactic: congr! 2 with a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a : α
⊢ (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ) • g a = HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f a) • g a)
have a₁ : (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ) • g a = ((∫ (a : α), rexp (f a) ∂μ)⁻¹ * rexp (f a)) • g a
Tactic: rw [smul_smul, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
a : α
a₁ : (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ) • g a = ((∫ (a : α), rexp (f a) ∂μ)⁻¹ * rexp (f a)) • g a
⊢ (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ) • g a = HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f a) • g a)
have a₂ : ((∫ (a : α), rexp (f a) ∂μ)⁻¹ * rexp (f a)) • g a = ((∫ (a : α), rexp (f a) ∂μ)⁻¹ * rexp (f a)) • g a
Tactic: rw [smul_smul, div_eq_inv_mul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f x) • g x))
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
have hc : Ne (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ 0
Tactic: rw [integrable_fun_smul_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Ne (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ 0
have hc : ¬Eq (α := ℝ) (∫ (a : α), rexp (f a) ∂μ) 0
Tactic: simp only [ne_eq, inv_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ ¬Eq (α := ℝ) (∫ (a : α), rexp (f a) ∂μ) 0
have this : NeZero μ
Tactic: have : NeZero μ := ⟨hμ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
have calc : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ)).toReal • g x) μ ↔
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ
Tactic: calc Integrable (fun x ↦ (ENNReal.ofReal (exp (f x) / ∫ a, exp (f a) ∂μ)).toReal • g x) μ
  _ ↔ Integrable (fun x ↦ (exp (f x) / ∫ a, exp (f a) ∂μ) • g x) μ := by
    congr! with a
    rw [ENNReal.toReal_ofReal]
    positivity
  _ ↔ Integrable (fun x ↦ (∫ a, exp (f a) ∂μ)⁻¹ • exp (f x) • g x) μ := by
    congr! 2 with a
    rw [smul_smul, div_eq_inv_mul]
  _ ↔ Integrable (fun x ↦ exp (f x) • g x) μ := by
    rw [integrable_fun_smul_iff]
    simp only [ne_eq, inv_eq_zero]
    have : NeZero μ := ⟨hμ⟩
    exact (integral_exp_pos hf).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
calc :
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
have calc₁ : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ ↔
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f x) • g x)) μ
Tactic: calc Integrable (fun x ↦ (ENNReal.ofReal (exp (f x) / ∫ a, exp (f a) ∂μ)).toReal • g x) μ
  _ ↔ Integrable (fun x ↦ (exp (f x) / ∫ a, exp (f a) ∂μ) • g x) μ := by
    congr! with a
    rw [ENNReal.toReal_ofReal]
    positivity
  _ ↔ Integrable (fun x ↦ (∫ a, exp (f a) ∂μ)⁻¹ • exp (f x) • g x) μ := by
    congr! 2 with a
    rw [smul_smul, div_eq_inv_mul]
  _ ↔ Integrable (fun x ↦ exp (f x) • g x) μ := by
    rw [integrable_fun_smul_iff]
    simp only [ne_eq, inv_eq_zero]
    have : NeZero μ := ⟨hμ⟩
    exact (integral_exp_pos hf).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → E
hμ : ¬μ = 0
hf_meas : AEMeasurable f μ
calc :
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ
calc₁ :
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f x) • g x))
      μ
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
have calc₂ : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ HSMul.hSMul (α := ℝ) (∫ (a : α), rexp (f a) ∂μ)⁻¹ (rexp (f x) • g x)) μ ↔
  Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
Tactic: calc Integrable (fun x ↦ (ENNReal.ofReal (exp (f x) / ∫ a, exp (f a) ∂μ)).toReal • g x) μ
  _ ↔ Integrable (fun x ↦ (exp (f x) / ∫ a, exp (f a) ∂μ) • g x) μ := by
    congr! with a
    rw [ENNReal.toReal_ofReal]
    positivity
  _ ↔ Integrable (fun x ↦ (∫ a, exp (f a) ∂μ)⁻¹ • exp (f x) • g x) μ := by
    congr! 2 with a
    rw [smul_smul, div_eq_inv_mul]
  _ ↔ Integrable (fun x ↦ exp (f x) • g x) μ := by
    rw [integrable_fun_smul_iff]
    simp only [ne_eq, inv_eq_zero]
    have : NeZero μ := ⟨hμ⟩
    exact (integral_exp_pos hf).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h : ν = 0
⊢ μ.rnDeriv (ν.tilted f) =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
have inl : ∀ᶠ (x : α) in ⊥,
  μ.rnDeriv (Measure.tilted 0 f) x =
    ENNReal.ofReal (rexp (-f x) * @integral _ _ _ _ mα 0 fun (x : α) ↦ rexp (f x)) * μ.rnDeriv 0 x
Tactic: simp_rw [h, ae_zero, Filter.EventuallyEq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ μ.rnDeriv (ν.tilted f) =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
have inr : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν
Tactic: refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
inr : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν
⊢ μ.rnDeriv (ν.tilted f) =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
have inr₁ : ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0
Tactic: refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
inr : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν
inr₁ : ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0
⊢ μ.rnDeriv (ν.tilted f) =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
have inr₂ : ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ∞
Tactic: refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
inr : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν
inr₁ : ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0
inr₂ : ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ ∞
⊢ μ.rnDeriv (ν.tilted f) =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
have inr₃ : (ae ν).EventuallyEq (β := ℝ≥0∞)
  (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) fun (x : α) ↦
  ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
Tactic: refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0
have inr : ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0
have inr : ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂ν
Tactic: simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ (ae ν).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x) fun (x : α) ↦
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
have inr : ∀ (x : α),
  (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x =
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
Tactic: filter_upwards with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x =
    ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
have inr : (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν)
Tactic: congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν)
have inr : 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν
Tactic: rw [← ENNReal.ofReal_inv_of_pos, inv_div', ← exp_neg, div_eq_mul_inv, inv_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
⊢ μ.rnDeriv (ν.tilted f) =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
have x : ν = 0 ∨ NeZero ν
Tactic: cases eq_zero_or_neZero ν with
  | inl h => simp_rw [h, ae_zero, Filter.EventuallyEq]; exact Filter.eventually_bot
  | inr h0 =>
    refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_
    · exact (hf.1.aemeasurable.div_const _).ennreal_ofReal
    · filter_upwards
      simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]
      exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)
    · refine ae_of_all _ (by simp)
    · filter_upwards with x
      congr
      rw [← ENNReal.ofReal_inv_of_pos, inv_div', ← exp_neg, div_eq_mul_inv, inv_inv]
      exact div_pos (exp_pos _) (integral_exp_pos hf)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ (μ.rnDeriv (ν.tilted f) x).toReal) fun (x : α) ↦
    (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
have h : ∀ (x : α) (hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x),
  (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
Tactic: filter_upwards [rnDeriv_tilted_right μ ν hf] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
have h : (ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x).toReal =
  (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
x : α
hx : μ.rnDeriv (ν.tilted f) x = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ (ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x).toReal =
    (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
have h : 0 ≤ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν ∨ (μ.rnDeriv ν x).toReal = 0
Tactic: simp only [ENNReal.toReal_mul, mul_eq_mul_right_iff, ENNReal.toReal_ofReal_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
g : (x : α) → ℝ≥0∞ := fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ (μ.tilted f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x
have refine_1 : AEMeasurable g ν
Tactic: refine Measure.rnDeriv_withDensity_left (μ := μ) (ν := ν) (f := g) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
g : (x : α) → ℝ≥0∞ := fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
refine_1 : AEMeasurable g ν
⊢ (μ.tilted f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x
have refine_2 : ∀ᵐ (x : α) ∂μ, g x ≠ ∞
Tactic: refine Measure.rnDeriv_withDensity_left (μ := μ) (ν := ν) (f := g) ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ ((μ.tilted f).rnDeriv ν x).toReal) fun (x : α) ↦
    (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
have h : ∀ (x : α) (hx : (μ.tilted f).rnDeriv ν x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x),
  ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
Tactic: filter_upwards [rnDeriv_tilted_left μ hfν] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
x : α
hx : (μ.tilted f).rnDeriv ν x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x
⊢ ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
have h : (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x).toReal =
  (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
x : α
hx : (μ.tilted f).rnDeriv ν x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x
⊢ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x).toReal =
    (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
have h : 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ∨ (μ.rnDeriv ν x).toReal = 0
Tactic: simp only [ENNReal.toReal_mul, mul_eq_mul_right_iff, ENNReal.toReal_ofReal_eq_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : AEMeasurable f μ
⊢ (μ.tilted f).rnDeriv μ =ᶠ[ae μ] fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
have refine : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x)
  fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
Tactic: refine (rnDeriv_tilted_left μ hf).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : AEMeasurable f μ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x)
    fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
have h : ∀ (x : α) (hx : μ.rnDeriv μ x = 1),
  ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x =
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
Tactic: filter_upwards [Measure.rnDeriv_self μ] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : AEMeasurable f μ
x : α
hx : μ.rnDeriv μ x = 1
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x =
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
have h : ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * 1 = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
Tactic: rw [hx, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : AEMeasurable f μ
x : α
hx : μ.rnDeriv μ x = 1
h : ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * 1 = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv μ x =
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
have h₁ : ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
Tactic: rw [hx, mul_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h : μ = 0
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((μ.tilted f).rnDeriv μ x).toReal) fun (x : α) ↦
    f x - log (∫ (x : α), rexp (f x) ∂μ)
have inl : ∀ᶠ (x : α) in ⊥,
  log (Measure.rnDeriv (m := mα) (Measure.tilted 0 f) 0 x).toReal =
    f x - log (@integral _ _ _ _ mα 0 fun (x : α) ↦ rexp (f x))
Tactic: simp_rw [h, ae_zero, Filter.EventuallyEq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((μ.tilted f).rnDeriv μ x).toReal) fun (x : α) ↦
    f x - log (∫ (x : α), rexp (f x) ∂μ)
have hf' : AEMeasurable f μ
Tactic: have hf' : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((μ.tilted f).rnDeriv μ x).toReal) fun (x : α) ↦
    f x - log (∫ (x : α), rexp (f x) ∂μ)
have h : ∀ (x : α) (hx : (μ.tilted f).rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)),
  log ((μ.tilted f).rnDeriv μ x).toReal = f x - log (∫ (x : α), rexp (f x) ∂μ)
Tactic: filter_upwards [rnDeriv_tilted_left_self hf'] with x hx