awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 ∂μ)
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 ∂μ)
⊢ 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 μ

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 ∂μ)
rw : AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict 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 ∂μ)

Tactic:
rw [tilted_eq_withDensity_nnreal, setIntegral_withDensity_eq_setIntegral_smul₀ _ _ hs]

Premises used: setIntegral_withDensity_eq_setIntegral_smul₀, MeasureTheory.tilted_eq_withDensity_nnreal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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, NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯ • g x ∂μ)
    (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ) μ
rw : AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ)) (μ.restrict s)
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)

Tactic:
rw [← aemeasurable_coe_nnreal_real_iff]

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

Tactic:
AEMeasurable.restrict ?_

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ) μ
refine : AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ)) μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(NNReal.mk (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 α
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) ∂μ) ⋯) : ℝ)) μ

Tactic:
simpa only [NNReal.coe_mk]

Premises used: NNReal.coe_mk
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 μ
suffices : 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)

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]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 (β := ℝ) (fun (x : α) ↦ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ

Tactic:
(measurable_exp.comp_aemeasurable hf).div_const _

Premises used: AEMeasurable.div_const, Real.exp, Real.measurable_exp, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 (β := ℝ) (fun (x : α) ↦ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ

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

Premises used: AEMeasurable.div_const, Real.measurable_exp, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 μ
⊢ ¬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 α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
g : α → E
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 α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
f : α → ℝ
g : α → E
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 α
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)) μ
neg : Eq.{u_2 + 1} (α := E) 0 (∫ (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 ∂μ)

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

Premises used: MeasureTheory.Measure.restrict_zero, MeasureTheory.integral_zero_measure, not_false_eq_true, MeasureTheory.tilted_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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)) μ
neg : Eq.{u_2 + 1} (α := E) 0 (∫ (x : α) in s, (rexp (f x) / 0) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) 0 (∫ (x : α) in s, (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 α
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) / 0) • g x ∂μ)

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

Premises used: AEMeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 ∂μ)
pos₁ : AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict 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 ∂μ)

Tactic:
rw [tilted_eq_withDensity_nnreal, setIntegral_withDensity_eq_setIntegral_smul₀']

Premises used: setIntegral_withDensity_eq_setIntegral_smul₀', MeasureTheory.tilted_eq_withDensity_nnreal
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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, NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯ • g x ∂μ)
    (∫ (x : α) in s, (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • g x ∂μ)

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ) μ
rw : AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ)) (μ.restrict s)
⊢ AEMeasurable (β := ℝ≥0) (fun (x : α) ↦ NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) (μ.restrict s)

Tactic:
rw [← aemeasurable_coe_nnreal_real_iff]

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

Tactic:
AEMeasurable.restrict ?_

Premises used: AEMeasurable.restrict
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ) μ
refine : AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(NNReal.mk (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) ⋯) : ℝ)) μ
⊢ AEMeasurable (β := ℝ) (fun (x : α) ↦ (↑(NNReal.mk (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 α
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) ∂μ) ⋯) : ℝ)) μ

Tactic:
simpa only [NNReal.coe_mk]

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

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]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 (β := ℝ) (fun (x : α) ↦ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ

Tactic:
(measurable_exp.comp_aemeasurable hf).div_const _

Premises used: AEMeasurable.div_const, Real.exp, Real.measurable_exp, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 (β := ℝ) (fun (x : α) ↦ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ

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

Premises used: AEMeasurable.div_const, Real.measurable_exp, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 μ
⊢ ¬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 α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SFinite μ
f : α → ℝ
g : α → E
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 α
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : SFinite μ
f : α → ℝ
g : α → E
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 α
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)) μ
neg : Eq.{u_2 + 1} (α := E) 0 (∫ (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 ∂μ)

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

Premises used: MeasureTheory.Measure.restrict_zero, MeasureTheory.integral_zero_measure, not_false_eq_true, MeasureTheory.tilted_of_not_aemeasurable
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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)) μ
neg : Eq.{u_2 + 1} (α := E) 0 (∫ (x : α) in s, (rexp (f x) / 0) • g x ∂μ)
⊢ Eq.{u_2 + 1} (α := E) 0 (∫ (x : α) in s, (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 α
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) / 0) • g x ∂μ)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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 ∂μ)
rw₂ 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 ∂μ)
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : α), 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]

Premises used: MeasureTheory.setIntegral_tilted', MeasureTheory.setIntegral_univ, MeasurableSet.univ
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
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))
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)

Tactic:
rw [h]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h : μ = 0
⊢ (@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:
simp
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
inr :
  ∫ (x : α), (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) • rexp (g x) ∂μ =
    HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)
⊢ ∫ (x : α), rexp (g x) ∂μ.tilted f = HDiv.hDiv (α := ℝ) (∫ (x : α), rexp ((f + g) x) ∂μ) (∫ (x : α), rexp (f x) ∂μ)

Tactic:
rw [integral_tilted f]

Premises used: MeasureTheory.integral_tilted
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
x : α
rw : (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x) ∂μ
⊢ (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp ((f + g) x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
rw [Pi.add_apply, exp_add]

Premises used: Pi.add_apply, Real.exp_add
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
h0 : NeZero μ
x : α
⊢ (rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) * rexp (g x) = rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
ring
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ

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
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ
inr :
  ∫ (x : α), rexp ((f + g) x) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ ∂μ =
    HMul.hMul (α := ℝ) (∫ (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) ∂μ)

Tactic:
simp_rw [this, div_eq_mul_inv]

Premises used: div_eq_mul_inv
-- Module: Mathlib.MeasureTheory.Measure.Tilted
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) ∂μ
inr inr₁ :
  HMul.hMul (α := ℝ) (∫ (a : α), rexp ((f + g) a) ∂μ) (∫ (x : α), rexp (f x) ∂μ)⁻¹ =
    HMul.hMul (α := ℝ) (∫ (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) ∂μ)⁻¹

Tactic:
rw [integral_mul_const]

Premises used: MeasureTheory.integral_mul_const
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f g : α → ℝ
⊢ μ = 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]

Premises used: MeasureTheory.integral_tilted, div_eq_mul_inv, smul_eq_mul, eq_zero_or_neZero, MeasureTheory.integral_mul_const
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h : μ = 0
⊢ (μ.tilted f).tilted g = μ.tilted (f + g)

Tactic:
simp [h]
-- Module: Mathlib.MeasureTheory.Measure.Tilted
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (ε := ℝ) (fun (x : α) ↦ rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
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∞)
⊢ (μ.tilted f).tilted g = μ.tilted (f + g)

Tactic:
ext1 s hs