awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂ν) ≠ ∞
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
⊢ μ.rnDeriv (ν.tilted f) =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x

Tactic:
refine (Measure.rnDeriv_withDensity_right μ ν ?_ ?_ ?_).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.Measure.rnDeriv_withDensity_right
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν

Tactic:
(hf.1.aemeasurable.div_const _).ennreal_ofReal

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.div_const, And.left, AEMeasurable.ennreal_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν)) ν

Tactic:
exact (hf.1.aemeasurable.div_const _).ennreal_ofReal

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, AEMeasurable.div_const, And.left, AEMeasurable.ennreal_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
inr : ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0
⊢ ∀ᵐ (x : α) ∂ν, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
inr : ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂ν
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂ν) ≠ 0

Tactic:
simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le]

Premises used: not_le, ENNReal.ofReal_eq_zero, ne_eq
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂ν

Tactic:
fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

Premises used: div_pos, MeasureTheory.integral_exp_pos, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
⊢ ∀ (a : α), 0 < rexp (f a) / ∫ (x : α), rexp (f x) ∂ν

Tactic:
exact fun _ ↦ div_pos (exp_pos _) (integral_exp_pos hf)

Premises used: div_pos, MeasureTheory.integral_exp_pos, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂ν) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂ν) ≠ ∞

Tactic:
refine ae_of_all _ (by simp)

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
inr :
  ∀ (x : α),
    (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ * μ.rnDeriv ν x =
      ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x
⊢ (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:
filter_upwards with x
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
inr :
  (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ = 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) ∂ν) * μ.rnDeriv ν x

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
inr : 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν
⊢ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂ν))⁻¹ = ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν)

Tactic:
rw [← ENNReal.ofReal_inv_of_pos, inv_div', ← exp_neg, div_eq_mul_inv, inv_inv]

Premises used: div_eq_mul_inv, ENNReal.ofReal_inv_of_pos, inv_inv, inv_div', Real.exp_neg
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν

Tactic:
div_pos (exp_pos _) (integral_exp_pos hf)

Premises used: div_pos, MeasureTheory.integral_exp_pos, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
h0 : NeZero ν
x : α
⊢ 0 < rexp (f x) / ∫ (x : α), rexp (f x) ∂ν

Tactic:
exact div_pos (exp_pos _) (integral_exp_pos hf)

Premises used: div_pos, MeasureTheory.integral_exp_pos, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f 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)

Premises used: not_le, MeasureTheory.AEStronglyMeasurable.aemeasurable, Filter.EventuallyEq.trans, ENNReal.ofReal_eq_zero, MeasureTheory.Measure.rnDeriv_withDensity_right, MeasureTheory.ae_zero, AEMeasurable.div_const, Filter.EventuallyEq, ne_eq, div_eq_mul_inv, ENNReal.ofReal_inv_of_pos, And.left, MeasureTheory.ae_of_all, inv_inv, inv_div', AEMeasurable.ennreal_ofReal, Real.exp_neg, eq_zero_or_neZero, Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
f : α → ℝ
μ ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) ν
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
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ (μ.rnDeriv (ν.tilted f) x).toReal) fun (x : α) ↦
    (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [rnDeriv_tilted_right μ ν hf] with x hx

Premises used: MeasureTheory.rnDeriv_tilted_right
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
h :
  (ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x).toReal =
    (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal
⊢ (μ.rnDeriv (ν.tilted f) x).toReal = (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
h : 0 ≤ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν ∨ (μ.rnDeriv ν x).toReal = 0
⊢ (ENNReal.ofReal (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * μ.rnDeriv ν x).toReal =
    (rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν) * (μ.rnDeriv ν x).toReal

Tactic:
simp only [ENNReal.toReal_mul, mul_eq_mul_right_iff, ENNReal.toReal_ofReal_eq_iff]

Premises used: mul_eq_mul_right_iff, ENNReal.toReal_mul, ENNReal.toReal_ofReal_eq_iff
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
⊢ 0 ≤ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
⊢ 0 ≤ rexp (-f x) * ∫ (x : α), rexp (f x) ∂ν ∨ (μ.rnDeriv ν x).toReal = 0

Tactic:
exact Or.inl (by positivity)

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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

Tactic:
Measure.rnDeriv_withDensity_left (μ := μ) (ν := ν) (f := g) ?_ ?_

Premises used: MeasureTheory.Measure.tilted, MeasureTheory.Measure.rnDeriv_withDensity_left
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 ν
refine_2 : ∀ᵐ (x : α) ∂μ, g x ≠ ∞
⊢ (μ.tilted f).rnDeriv ν =ᶠ[ae ν] fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x

Tactic:
refine Measure.rnDeriv_withDensity_left (μ := μ) (ν := ν) (f := g) ?_ ?_

Premises used: MeasureTheory.Measure.rnDeriv_withDensity_left
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ)
⊢ AEMeasurable g ν

Tactic:
((measurable_exp.comp_aemeasurable hfν).div_const _).ennreal_ofReal

Premises used: AEMeasurable.div_const, Real.exp, Real.measurable_exp, Measurable.comp_aemeasurable, AEMeasurable.ennreal_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ)
⊢ AEMeasurable g ν

Tactic:
exact ((measurable_exp.comp_aemeasurable hfν).div_const _).ennreal_ofReal

Premises used: AEMeasurable.div_const, Real.measurable_exp, Measurable.comp_aemeasurable, AEMeasurable.ennreal_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ)
x : α
⊢ g x ≠ ∞

Tactic:
simp [g]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ)
⊢ ∀ᵐ (x : α) ∂μ, g x ≠ ∞

Tactic:
exact ae_of_all _ (fun x ↦ by simp [g])

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
ν : Measure α
inst : SigmaFinite μ
inst_1 : SigmaFinite ν
hfν : AEMeasurable f ν
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
⊢ (ae ν).EventuallyEq (β := ℝ) (fun (x : α) ↦ ((μ.tilted f).rnDeriv ν x).toReal) fun (x : α) ↦
    (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [rnDeriv_tilted_left μ hfν] with x hx

Premises used: MeasureTheory.rnDeriv_tilted_left
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
h :
  (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x).toReal =
    (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal
⊢ ((μ.tilted f).rnDeriv ν x).toReal = (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
h : 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ∨ (μ.rnDeriv ν x).toReal = 0
⊢ (ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * μ.rnDeriv ν x).toReal =
    (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * (μ.rnDeriv ν x).toReal

Tactic:
simp only [ENNReal.toReal_mul, mul_eq_mul_right_iff, ENNReal.toReal_ofReal_eq_iff]

Premises used: mul_eq_mul_right_iff, ENNReal.toReal_mul, ENNReal.toReal_ofReal_eq_iff
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ ∨ (μ.rnDeriv ν x).toReal = 0

Tactic:
exact Or.inl (by positivity)

Premises used: Or.inl
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ)

Tactic:
(rnDeriv_tilted_left μ hf).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.rnDeriv_tilted_left
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : AEMeasurable f μ
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) ∂μ)
⊢ (μ.tilted f).rnDeriv μ =ᶠ[ae μ] fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)

Tactic:
refine (rnDeriv_tilted_left μ hf).trans ?_

Premises used: Filter.EventuallyEq.trans, MeasureTheory.rnDeriv_tilted_left
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : AEMeasurable f μ
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) ∂μ)
⊢ (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:
filter_upwards [Measure.rnDeriv_self μ] with x hx

Premises used: MeasureTheory.Measure.rnDeriv_self
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ)
h₁ h₂ : ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) = 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) ∂μ)

Tactic:
rw [hx, mul_one]

Premises used: mul_one
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h : μ = 0
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))
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((μ.tilted f).rnDeriv μ x).toReal) fun (x : α) ↦
    f x - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
simp_rw [h, ae_zero, Filter.EventuallyEq]

Premises used: MeasureTheory.ae_zero, Filter.EventuallyEq
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h : μ = 0
⊢ ∀ᶠ (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:
Filter.eventually_bot

Premises used: Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h : μ = 0
⊢ ∀ᶠ (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:
exact Filter.eventually_bot

Premises used: Filter.eventually_bot
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ AEMeasurable f μ

Tactic:
have hf' : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
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) ∂μ)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ log ((μ.tilted f).rnDeriv μ x).toReal) fun (x : α) ↦
    f x - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
filter_upwards [rnDeriv_tilted_left_self hf'] with x hx

Premises used: MeasureTheory.rnDeriv_tilted_left_self
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
x : α
hx : (μ.tilted f).rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
x : α
hx : (μ.tilted f).rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
h : Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0
⊢ log ((μ.tilted f).rnDeriv μ x).toReal = f x - log (∫ (x : α), rexp (f x) ∂μ)

Tactic:
rw [hx, ENNReal.toReal_ofReal (by positivity), log_div (exp_pos _).ne', log_exp]

Premises used: Real.log_exp, Real.log_div, LT.lt.ne', ENNReal.toReal_ofReal, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
x : α
hx : (μ.tilted f).rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0

Tactic:
(integral_exp_pos hf).ne'

Premises used: LT.lt.ne', MeasureTheory.integral_exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
hf' : AEMeasurable f μ
x : α
hx : (μ.tilted f).rnDeriv μ x = ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)
⊢ Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0

Tactic:
exact (integral_exp_pos hf).ne'

Premises used: LT.lt.ne', MeasureTheory.integral_exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : SigmaFinite μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f 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 =>
    have hf' : AEMeasurable f μ := aemeasurable_of_aemeasurable_exp hf.1.aemeasurable
    filter_upwards [rnDeriv_tilted_left_self hf'] with x hx
    rw [hx, ENNReal.toReal_ofReal (by positivity), log_div (exp_pos _).ne', log_exp]
    exact (integral_exp_pos hf).ne'

Premises used: Real.log_exp, MeasureTheory.ae_zero, Filter.EventuallyEq, Real.log_div, LT.lt.ne', ENNReal.toReal_ofReal, eq_zero_or_neZero, Real.exp_pos, Filter.eventually_bot