awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
pos : Integrable (ε := ℝ) (fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)
pos₁ : (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
rw [tilted_apply _ _, ← ofReal_integral_eq_lintegral_ofReal]

Premises used: MeasureTheory.tilted_apply, MeasureTheory.ofReal_integral_eq_lintegral_ofReal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)

Tactic:
hf.integrableOn.div_const _

Premises used: MeasureTheory.Integrable.div_const, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ Integrable (ε := ℝ) (fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) (μ.restrict s)

Tactic:
exact hf.integrableOn.div_const _

Premises used: MeasureTheory.Integrable.div_const, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
x : α
⊢ LE.le (α := ℝ) (0 x) ((fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) x)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ (ae (μ.restrict s)).EventuallyLE (β := ℝ) 0 fun (a : α) ↦ rexp (f a) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
exact ae_of_all _ (fun _ ↦ by positivity)

Premises used: MeasureTheory.ae_of_all
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
s : Set α
hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ (μ.tilted f : (a : Set α) → ℝ≥0∞) s = ENNReal.ofReal (∫ (a : α) in s, rexp (f a) / ∫ (x : α), rexp (f x) ∂μ ∂μ)

Tactic:
simp [tilted_of_not_integrable hf, integral_undef hf]

Premises used: MeasureTheory.integral_undef, MeasureTheory.tilted_of_not_integrable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
measure_univ : Eq (α := ℝ≥0∞) ((μ.tilted f : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)
⊢ IsProbabilityMeasure (μ.tilted f)

Tactic:
constructor
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
measure_univ : ∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ ∂μ = 1
⊢ Eq (α := ℝ≥0∞) ((μ.tilted f : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
simp_rw [tilted_apply' _ _ MeasurableSet.univ, setLIntegral_univ,
    ENNReal.ofReal_div_of_pos (integral_exp_pos hf), div_eq_mul_inv]

Premises used: ENNReal.ofReal_div_of_pos, div_eq_mul_inv, MeasureTheory.integral_exp_pos, MeasurableSet.univ, MeasureTheory.tilted_apply', MeasureTheory.setLIntegral_univ
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
measure_univ₁ : ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ ∞
⊢ ∫⁻ (a : α), ENNReal.ofReal (rexp (f a)) * (ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ))⁻¹ ∂μ = 1

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]

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, LT.lt.le, MeasureTheory.lintegral_mul_const'', ENNReal.mul_inv_cancel, And.left, MeasureTheory.ae_of_all, MeasureTheory.ofReal_integral_eq_lintegral_ofReal, AEMeasurable.ennreal_ofReal, Real.exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
measure_univ : LT.lt (α := ℝ) 0 (∫ (x : α), rexp (f x) ∂μ)
⊢ ENNReal.ofReal (∫ (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 α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), rexp (f x) ∂μ)

Tactic:
integral_exp_pos hf

Premises used: MeasureTheory.integral_exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), rexp (f x) ∂μ)

Tactic:
exact integral_exp_pos hf

Premises used: MeasureTheory.integral_exp_pos
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ ENNReal.ofReal (∫ (x : α), rexp (f x) ∂μ) ≠ ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
inl : ∀ (hμ : μ = 0), IsZeroOrProbabilityMeasure (μ.tilted f)
inr : ∀ (hμ : NeZero μ), IsZeroOrProbabilityMeasure (μ.tilted f)
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)

Tactic:
rcases eq_zero_or_neZero μ with hμ | hμ

Premises used: eq_zero_or_neZero
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : μ = 0
inl : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := mα) 0
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)

Tactic:
simp only [hμ, tilted_zero_measure]

Premises used: MeasureTheory.tilted_zero_measure
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : μ = 0
⊢ IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := mα) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
pos : ∀ (hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ), IsZeroOrProbabilityMeasure (μ.tilted f)
neg : ∀ (hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ), IsZeroOrProbabilityMeasure (μ.tilted f)
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)

Tactic:
by_cases hf : Integrable (fun x ↦ exp (f x)) μ

Premises used: MeasureTheory.Integrable, Real.exp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ IsProbabilityMeasure (μ.tilted f)

Tactic:
have := isProbabilityMeasure_tilted hf
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
neg : IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := mα) 0
⊢ IsZeroOrProbabilityMeasure (μ.tilted f)

Tactic:
simp only [hf, not_false_eq_true, tilted_of_not_integrable]

Premises used: MeasureTheory.tilted_of_not_integrable, not_false_eq_true
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hμ : NeZero μ
hf : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
⊢ IsZeroOrProbabilityMeasure.{u_1} (α := α) (m0 := mα) 0

Tactic:
infer_instance
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 ∂μ
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 ∂μ
⊢ ∫⁻ (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 μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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
pos₃ : ∀ᵐ (x : α) ∂μ.restrict s, ENNReal.ofReal (rexp (f x) / ∫ (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 ∂μ

Tactic:
rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀]

Premises used: MeasureTheory.Measure.tilted, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ ∫⁻ (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:
simp only [Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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)

Tactic:
AEMeasurable.restrict ?_

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
pos : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) (μ.restrict s)

Tactic:
refine AEMeasurable.restrict ?_

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

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 : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ

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 : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ MeasurableSet s

Tactic:
hs
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ MeasurableSet s

Tactic:
exact hs
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
pos : ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) < ∞
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) < ∞

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) < ∞

Tactic:
simp only [ENNReal.ofReal_lt_top, implies_true]

Premises used: ENNReal.ofReal_lt_top, implies_true
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, And.left, Real.aemeasurable_of_aemeasurable_exp, Not
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Premises used: Real.aemeasurable_of_aemeasurable_exp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
⊢ ¬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)
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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)) μ
neg : 0 = ∫⁻ (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 ∂μ

Tactic:
simp only [hf, not_false_eq_true, tilted_of_not_aemeasurable, Measure.restrict_zero,
      lintegral_zero_measure]

Premises used: MeasureTheory.Measure.restrict_zero, MeasureTheory.lintegral_zero_measure, not_false_eq_true, MeasureTheory.tilted_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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)) μ
neg : 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / 0) * g x ∂μ
⊢ 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
rw [integral_undef hf']

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) / 0) * g x ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 ∂μ
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 ∂μ
⊢ ∫⁻ (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 μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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)
pos₂ : ∀ᵐ (x : α) ∂μ.restrict s, ENNReal.ofReal (rexp (f x) / ∫ (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 ∂μ

Tactic:
rw [Measure.tilted, setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀']

Premises used: MeasureTheory.Measure.tilted, MeasureTheory.setLIntegral_withDensity_eq_setLIntegral_mul_non_measurable₀'
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ ∫⁻ (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:
simp only [Pi.mul_apply]

Premises used: Pi.mul_apply
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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)

Tactic:
AEMeasurable.restrict ?_

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
pos : AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) (μ.restrict s)

Tactic:
refine AEMeasurable.restrict ?_

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

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 α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ AEMeasurable (β := ℝ≥0∞) (fun (x : α) ↦ ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ)) μ

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 α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
pos : ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) < ∞
⊢ ∀ᵐ (x : α) ∂μ.restrict s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) < ∞

Tactic:
filter_upwards
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : AEMeasurable f μ
⊢ ∀ (a : α), ENNReal.ofReal (rexp (f a) / ∫ (x : α), rexp (f x) ∂μ) < ∞

Tactic:
simp only [ENNReal.ofReal_lt_top, implies_true]

Premises used: ENNReal.ofReal_lt_top, implies_true
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Premises used: MeasureTheory.AEStronglyMeasurable.aemeasurable, And.left, Real.aemeasurable_of_aemeasurable_exp, Not
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
⊢ ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ

Tactic:
exact fun h ↦ hf (aemeasurable_of_aemeasurable_exp h.1.aemeasurable)

Premises used: Real.aemeasurable_of_aemeasurable_exp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
⊢ ¬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)
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
neg : 0 = ∫⁻ (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 ∂μ

Tactic:
simp only [hf, not_false_eq_true, tilted_of_not_aemeasurable, Measure.restrict_zero,
      lintegral_zero_measure]

Premises used: MeasureTheory.Measure.restrict_zero, MeasureTheory.lintegral_zero_measure, not_false_eq_true, MeasureTheory.tilted_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
f : α → ℝ
g : α → ℝ≥0∞
s : Set α
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
neg : 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / 0) * g x ∂μ
⊢ 0 = ∫⁻ (x : α) in s, ENNReal.ofReal (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * g x ∂μ

Tactic:
rw [integral_undef hf']

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) / 0) * g x ∂μ

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 ∂μ
rw₂ 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 ∂μ
⊢ ∫⁻ (x : α), 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]

Premises used: MeasureTheory.setLIntegral_tilted', MeasurableSet.univ, MeasureTheory.setLIntegral_univ