awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
measure_univ : ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ 0
⊢ ∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ ∂μ = 1
have measure_univ₁ : ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ ∞
Tactic: rw [lintegral_mul_const'' _ hf.1.aemeasurable.ennreal_ofReal,
    ← ofReal_integral_eq_lintegral_ofReal hf (ae_of_all _ fun _ ↦ (exp_pos _).le),
    ENNReal.mul_inv_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ 0
have measure_univ : LT.lt (α := ℝ) 0 (∫ (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 α
μ : Measure α
f : α → ℝ
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)
have inl : ∀ (hμ : μ = 0), IsZeroOrProbabilityMeasure (μ.tilted f)
Tactic: rcases eq_zero_or_neZero μ with hμ | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inl : ∀ (hμ : μ = 0), IsZeroOrProbabilityMeasure (μ.tilted f)
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)
have inr : ∀ (hμ : NeZero μ), IsZeroOrProbabilityMeasure (μ.tilted f)
Tactic: rcases eq_zero_or_neZero μ with hμ | hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : μ = 0
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)
have inl : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := mα) 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 : α → ℝ
hμ : NeZero μ
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)
have pos : ∀ (hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ), IsZeroOrProbabilityMeasure (μ.tilted f)
Tactic: by_cases hf : Integrable (fun x ↦ exp (f x)) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
pos : ∀ (hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ), IsZeroOrProbabilityMeasure (μ.tilted f)
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)
have neg : ∀ (hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ), IsZeroOrProbabilityMeasure (μ.tilted f)
Tactic: by_cases hf : Integrable (fun x ↦ exp (f x)) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)
have this : IsProbabilityMeasure (μ.tilted f)
Tactic: have := isProbabilityMeasure_tilted hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)
have neg : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := mα) 0
Tactic: simp only [hf, not_false_eq_true, tilted_of_not_integrable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have pos : ∀ (hf : AEMeasurable f μ),
  ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (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 α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
pos :
  ∀ (hf : AEMeasurable f μ),
    ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have neg : ∀ (hf : ¬AEMeasurable f μ),
  ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (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 α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have pos : ∫⁻ (a : α) in s,
    HMul.hMul (α := α → ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) g a ∂μ =
  ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Tactic: rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
pos :
  ∫⁻ (a : α) in s,
      HMul.hMul (α := α → ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) g a ∂μ =
    ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have pos₁ : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) (μ.restrict s)
Tactic: rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
pos :
  ∫⁻ (a : α) in s,
      HMul.hMul (α := α → ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) g a ∂μ =
    ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
pos₁ : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) (μ.restrict s)
pos₂ : MeasurableSet s
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have pos₃ : ∀ᵐ (x : α) ∂μ.restrict s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) < ∞
Tactic: rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) (μ.restrict s)
have pos : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ
Tactic: refine AEMeasurable.restrict ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) < ∞
have pos : ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) < ∞
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (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 α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have neg : 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Tactic: simp only [hf, not_false_eq_true, tilted_of_not_aemeasurable, Measure.restrict_zero,
      lintegral_zero_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have neg : 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (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 α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have pos : ∀ (hf : AEMeasurable f μ),
  ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (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 α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
pos :
  ∀ (hf : AEMeasurable f μ),
    ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have neg : ∀ (hf : ¬AEMeasurable f μ),
  ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (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 α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have pos : ∫⁻ (a : α) in s,
    HMul.hMul (α := α → ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) g a ∂μ =
  ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Tactic: rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
pos :
  ∫⁻ (a : α) in s,
      HMul.hMul (α := α → ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) g a ∂μ =
    ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have pos₁ : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) (μ.restrict s)
Tactic: rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
pos :
  ∫⁻ (a : α) in s,
      HMul.hMul (α := α → ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) g a ∂μ =
    ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
pos₁ : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) (μ.restrict s)
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have pos₂ : ∀ᵐ (x : α) ∂μ.restrict s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) < ∞
Tactic: rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀']
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) (μ.restrict s)
have pos : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ
Tactic: refine AEMeasurable.restrict ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) < ∞
have pos : ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) < ∞
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (hypothesis)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (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 α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ ∫⁻ (x : α) in s, g x ∂μ.tilted f = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have neg : 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Tactic: simp only [hf, not_false_eq_true, tilted_of_not_aemeasurable, Measure.restrict_zero,
      lintegral_zero_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have neg : 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (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 α
f : α → ℝ
g : α → ℝ≥0∞
⊢ ∫⁻ (x : α), g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have rw : ∫⁻ (x : α) in Set.univ, g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Tactic: rw [← setLIntegral_univ, setLIntegral_tilted' f g MeasurableSet.univ, setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
rw :
  ∫⁻ (x : α) in Set.univ, g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
⊢ ∫⁻ (x : α), g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have rw₁ : ∫⁻ (x : α) in Set.univ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ =
  ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Tactic: rw [← setLIntegral_univ, setLIntegral_tilted' f g MeasurableSet.univ, setLIntegral_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Tilted (goal)
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
rw :
  ∫⁻ (x : α) in Set.univ, g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
rw₁ :
  ∫⁻ (x : α) in Set.univ, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ =
    ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
⊢ ∫⁻ (x : α), g x ∂μ.tilted f = ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
have rw₂ : ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ =
  ∫⁻ (x : α), ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ
Tactic: rw [← setLIntegral_univ, setLIntegral_tilted' f g MeasurableSet.univ, setLIntegral_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
s : Set α
hs : MeasurableSet s
⊢ 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 : ∀ (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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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₀ _ _ hs]
-- 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
s : Set α
hs : MeasurableSet s
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 rw : 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₀ _ _ hs]
-- 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
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)
have suffices : 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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
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
inst_2 : SFinite μ
f : α → ℝ
g : α → E
s : Set α
⊢ 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 : ∀ (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 μ