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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
pos :
  ∀ (hf : AEMeasurable f μ),
    Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, g x ∂μ.tilted f)
      (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, g x ∂μ.tilted f)
    (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
have neg : ∀ (hf : ¬AEMeasurable f μ),
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, g x ∂μ.tilted f)
    (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
Tactic: by_cases hf : AEMeasurable f μ
-- 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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, g x ∂μ.tilted f)
    (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
have pos : Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) sorry • g x ∂μ)
  (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
Tactic: rw [tilted_eq_withDensity_nnreal, setIntegral_withDensity_eq_setIntegral_smul₀']
-- 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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
pos :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯ • g x ∂μ)
    (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, g x ∂μ.tilted f)
    (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
have pos₁ : AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) sorry) (μ.restrict s)
Tactic: rw [tilted_eq_withDensity_nnreal, setIntegral_withDensity_eq_setIntegral_smul₀']
-- 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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
this : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)
have rw : AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) sorry) : ℝ)) (μ.restrict s)
Tactic: rw [← aemeasurable_coe_nnreal_real_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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
this : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ)) (μ.restrict s)
have refine : AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) sorry) : ℝ)) μ
Tactic: refine AEMeasurable.restrict ?_
-- 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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)
have pos : AEMeasurable (β := ℝ) (fun (x : α) ↦ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
Tactic: suffices AEMeasurable (fun x ↦ exp (f x) / ∫ x, exp (f x) ∂μ) μ by
        rw [← aemeasurable_coe_nnreal_real_iff]
        refine AEMeasurable.restrict ?_
        simpa only [NNReal.coe_mk]
-- 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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, g x ∂μ.tilted f)
    (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
have hf' : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
Tactic: have hf' : ¬ Integrable (fun x ↦ exp (f x)) μ := by
      exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)
-- 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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α) in s, g x ∂μ.tilted f)
    (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
have neg : Eq.{u_2 + 1} (α := E) 0 (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
Tactic: simp only [hf, not_false_eq_true, tilted_of_not_aemeasurable, Measure.restrict_zero,
      integral_zero_measure]
-- 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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ Eq.{u_2 + 1} (α := E) 0 (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
have neg : Eq.{u_2 + 1} (α := E) 0 (∫ (x : α) in s, (rexp (f x) / 0) • g x ∂μ)
Tactic: rw [integral_undef hf']
-- 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 : α → ℝ
g : α → E
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), g x ∂μ.tilted f) (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
have rw : Eq.{u_2 + 1} (α := E) (∫ (x : α) in Set.univ, g x ∂μ.tilted f)
  (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
Tactic: rw [← setIntegral_univ, setIntegral_tilted' f g MeasurableSet.univ, setIntegral_univ]
-- 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 : α → ℝ
g : α → E
rw :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in Set.univ, g x ∂μ.tilted f)
    (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), g x ∂μ.tilted f) (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
have rw₁ : Eq.{u_2 + 1} (α := E) (∫ (x : α) in Set.univ, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
  (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
Tactic: rw [← setIntegral_univ, setIntegral_tilted' f g MeasurableSet.univ, setIntegral_univ]
-- 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 : α → ℝ
g : α → E
rw :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in Set.univ, g x ∂μ.tilted f)
    (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
rw₁ :
  Eq.{u_2 + 1} (α := E) (∫ (x : α) in Set.univ, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
    (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), g x ∂μ.tilted f) (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
have rw₂ : Eq.{u_2 + 1} (α := E) (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
  (∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)
Tactic: rw [← setIntegral_univ, setIntegral_tilted' f g MeasurableSet.univ, setIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)
have inl : (@integral _ _ _ _ mα (Measure.tilted 0 f) fun (x : α) ↦ rexp (g x)) =
  HDiv.hDiv (α := ℝ) (@integral _ _ _ _ mα 0 fun (x : α) ↦ rexp ((f + g) x))
    (@integral _ _ _ _ mα 0 fun (x : α) ↦ rexp (f x))
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)
have inr : ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • rexp (g x) ∂μ =
  HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)
Tactic: rw [integral_tilted f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
x : α
⊢ (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
have rw : (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x) ∂μ
Tactic: rw [Pi.add_apply, exp_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
⊢ ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) ∂μ =
    HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)
have this : ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
Tactic: have : ∀ x, (exp (f x) / ∫ x, exp (f x) ∂μ) * exp (g x)
        = (exp ((f + g) x) / ∫ x, exp (f x) ∂μ) := by
      intro x
      rw [Pi.add_apply, exp_add]
      ring
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
this : ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
⊢ ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) ∂μ =
    HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)
have inr : ∫ (x : α), rexp ((f + g) x) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ ∂μ =
  HMul.hMul (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)⁻¹
Tactic: simp_rw [this, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
this : ∀ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ
⊢ ∫ (x : α), rexp ((f + g) x) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ ∂μ =
    HMul.hMul (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)⁻¹
have inr : HMul.hMul (α := ℝ) (∫ (a : α), rexp ((f + g) a) ∂μ) (∫ (x : α), rexp (f x) ∂μ)⁻¹ =
  HMul.hMul (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)⁻¹
Tactic: rw [integral_mul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)
have x : μ = 0 ∨ NeZero μ
Tactic: cases eq_zero_or_neZero μ with
  | inl h => rw [h]; simp
  | inr h0 =>
    rw [integral_tilted f]
    simp_rw [smul_eq_mul]
    have : ∀ x, (exp (f x) / ∫ x, exp (f x) ∂μ) * exp (g x)
        = (exp ((f + g) x) / ∫ x, exp (f x) ∂μ) := by
      intro x
      rw [Pi.add_apply, exp_add]
      ring
    simp_rw [this, div_eq_mul_inv]
    rw [integral_mul_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
⊢ (μ.tilted f).tilted g = μ.tilted (f + g)
have inr : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) (((μ.tilted f).tilted g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.tilted (f + g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((μ.tilted f).tilted g : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    ((μ.tilted (f + g) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have inr : ∫⁻ (x : α) in s,
    ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
      ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) ∂μ =
  ∫⁻ (a : α) in s, ENNReal.ofReal (rexp ((f + g) a) / ∫ (x : α), rexp ((f + g) x) ∂μ) ∂μ
Tactic: rw [tilted_apply' _ _ hs, tilted_apply' _ _ hs, setLIntegral_tilted' f _ hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s,
      ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
        ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) ∂μ =
    ∫⁻ (a : α) in s, ENNReal.ofReal (rexp ((f + g) a) / ∫ (x : α), rexp ((f + g) x) ∂μ) ∂μ
have inr : ∀ (x : α),
  ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
      ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) =
    ENNReal.ofReal (rexp ((f + g) x) / ∫ (x : α), rexp ((f + g) x) ∂μ)
Tactic: congr with x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
      ENNReal.ofReal (rexp (g x) / ∫ (x : α), rexp (g x) ∂μ.tilted f) =
    ENNReal.ofReal (rexp ((f + g) x) / ∫ (x : α), rexp ((f + g) x) ∂μ)
have inr : ENNReal.ofReal
    ((rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
      (rexp (g x) / HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ))) =
  ENNReal.ofReal (rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ)
Tactic: rw [← ENNReal.ofReal_mul (by positivity),
      integral_exp_tilted f, Pi.add_apply, exp_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ ENNReal.ofReal
      ((rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
        (rexp (g x) / HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ))) =
    ENNReal.ofReal (rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ)
have inr : (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
    (rexp (g x) / HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)) =
  rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) *
      (rexp (g x) / HDiv.hDiv (α := ℝ) (∫ (x : α), rexp (f x + g x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)) =
    rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x + g x) ∂μ
have this : Ne (α := ℝ) (∫ (x : α), rexp (f x) ∂μ) 0
Tactic: have := (integral_exp_pos hf).ne'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
⊢ (μ.tilted f).tilted g = μ.tilted (f + g)
have x : μ = 0 ∨ NeZero μ
Tactic: cases eq_zero_or_neZero μ with
  | inl h => simp [h]
  | inr h0 =>
    ext1 s hs
    rw [tilted_apply' _ _ hs, tilted_apply' _ _ hs, setLIntegral_tilted' f _ hs]
    congr with x
    rw [← ENNReal.ofReal_mul (by positivity),
      integral_exp_tilted f, Pi.add_apply, exp_add]
    congr 1
    simp only [Pi.add_apply]
    have := (integral_exp_pos hf).ne'
    simp [field]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
hg : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (g x)) μ
⊢ (μ.tilted f).tilted g = (μ.tilted g).tilted f
have rw : μ.tilted (f + g) = (μ.tilted g).tilted f
Tactic: rw [tilted_tilted hf, add_comm, tilted_tilted hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
hg : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (g x)) μ
rw : μ.tilted (f + g) = (μ.tilted g).tilted f
⊢ (μ.tilted f).tilted g = (μ.tilted g).tilted f
have rw₁ : μ.tilted (g + f) = (μ.tilted g).tilted f
Tactic: rw [tilted_tilted hf, add_comm, tilted_tilted hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
hg : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (g x)) μ
rw : μ.tilted (f + g) = (μ.tilted g).tilted f
rw₁ : μ.tilted (g + f) = (μ.tilted g).tilted f
⊢ (μ.tilted f).tilted g = (μ.tilted g).tilted f
have rw₂ : μ.tilted (g + f) = μ.tilted (g + f)
Tactic: rw [tilted_tilted hf, add_comm, tilted_tilted hg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ (μ.tilted f).tilted (-f) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
have rw : μ.tilted (f + -f) = HSMul.hSMul (α := ℝ≥0∞) (((μ : (a : Set α) → ℝ≥0∞) Set.univ)⁻¹ : ℝ≥0∞) μ
Tactic: rw [tilted_tilted hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h : μ = 0
⊢ μ ≪ μ.tilted f
have inl : Measure.AbsolutelyContinuous.{u_1} (α := α) (_m0 := mα) 0 0
Tactic: simp only [h, tilted_zero_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
⊢ μ ≪ μ.tilted f
have inr : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ
Tactic: refine withDensity_absolutelyContinuous' ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
h0 : NeZero μ
inr : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ
⊢ μ ≪ μ.tilted f
have inr₁ : ∀ᵐ (x : α) ∂μ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ≠ 0
Tactic: refine withDensity_absolutelyContinuous' ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
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 α
μ : Measure α
f : α → ℝ
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 (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ μ ≪ μ.tilted f
have x : μ = 0 ∨ NeZero μ
Tactic: cases eq_zero_or_neZero μ with
  | inl h => simp only [h, tilted_zero_measure]; exact fun _ _ ↦ by simp
  | inr h0 =>
    refine withDensity_absolutelyContinuous' ?_ ?_
    · 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)
-- 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
⊢ Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
have pos : ∀ (hμ : μ = 0), Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
Tactic: by_cases hμ : μ = 0
-- 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
pos : ∀ (hμ : μ = 0), Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
⊢ Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
have neg : ∀ (hμ : ¬μ = 0), Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
Tactic: by_cases hμ : μ = 0
-- 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
⊢ Integrable g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
have hf_meas : AEMeasurable f μ
Tactic: have hf_meas : 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 α
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 g (μ.tilted f) ↔ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ rexp (f x) • g x) μ
have neg : 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) μ
Tactic: rw [Measure.tilted, integrable_withDensity_iff_integrable_smul₀' (by fun_prop) (by simp)]
-- 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) / ∫ (a : α), rexp (f a) ∂μ)).toReal • g x)
      μ ↔
    Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ (rexp (f x) / ∫ (a : α), rexp (f a) ∂μ) • g x) μ
have a : ∀ (a : α), (ENNReal.ofReal (rexp (f a) / ∫ (a : α), rexp (f a) ∂μ)).toReal = rexp (f a) / ∫ (a : α), rexp (f a) ∂μ
Tactic: congr! with a