-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma tilted_tilted (hf : Integrable (fun x ↦ exp (f x)) μ) (g : α → ℝ) :
    (μ.tilted f).tilted g = μ.tilted (f + g)

Proof state:
case inr.h.e_f.h
α : 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) / ((∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ))) =
    ENNReal.ofReal (rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ)

Tactic:
congr 1

Result:
case inr.h.e_f.h.e_r
α : 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) / ((∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ)) =
    rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
x : α
⊢ 0 ≤ rexp (f x) / ∫ (x : α), rexp (f x) ∂μ

Tactic:
positivity

Result:
no goals

Proof state:
case inr.h.e_f.h
α : 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) ∂μ)

Tactic:
rw [← ENNReal.ofReal_mul (by positivity),
  integral_exp_tilted f, Pi.add_apply, exp_add]

Result:
case inr.h.e_f.h
α : 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) / ((∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ))) =
    ENNReal.ofReal (rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ)

Proof state:
case inr.h.e_f.h.e_r
α : 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) / ((∫ (x : α), rexp (f x + g x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ)) =
    rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x + g x) ∂μ

Tactic:
field_simp

Result:
case inr.h.e_f.h.e_r
α : 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) * (rexp (g x) * ∫ (x : α), rexp (f x) ∂μ) / ((∫ (x : α), rexp (f x) ∂μ) * ∫ (x : α), rexp (f x + g x) ∂μ) =
    rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x + g x) ∂μ

Proof state:
case inr.h
α : 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) ∂μ) ∂μ

Tactic:
congr with x

Result:
case inr.h.e_f.h
α : 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) ∂μ)

Proof state:
case inr.h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
⊢ ((μ.tilted f).tilted g) s = (μ.tilted (f + g)) s

Tactic:
rw [tilted_apply' _ _ hs, tilted_apply' _ _ hs, setLIntegral_tilted' f _ hs]

Result:
case inr.h
α : 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) ∂μ) ∂μ

Proof state:
case inl
α : 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]

Result:
no goals

Proof state:
case inr.h.e_f.h.e_r
α : 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) / ((∫ (x : α), rexp ((f + g) x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ)) =
    rexp (f x) * rexp (g x) / ∫ (x : α), rexp ((f + g) x) ∂μ

Tactic:
simp only [Pi.add_apply]

Result:
case inr.h.e_f.h.e_r
α : 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) / ((∫ (x : α), rexp (f x + g x) ∂μ) / ∫ (x : α), rexp (f x) ∂μ)) =
    rexp (f x) * rexp (g x) / ∫ (x : α), rexp (f x + g x) ∂μ

Proof state:
case inr.h.e_f.h.e_r
α : 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) * rexp (g x) * ∫ (x : α), rexp (f x) ∂μ) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ *
      (∫ (x : α), rexp (f x + g x) ∂μ)⁻¹ =
    rexp (f x) * rexp (g x) * (∫ (x : α), rexp (f x + g x) ∂μ)⁻¹

Tactic:
congr 1

Result:
case inr.h.e_f.h.e_r.e_a
α : 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) * rexp (g x) * ∫ (x : α), rexp (f x) ∂μ) * (∫ (x : α), rexp (f x) ∂μ)⁻¹ = rexp (f x) * rexp (g x)

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
⊢ (μ.tilted f).tilted g = μ.tilted (f + g)

Tactic:
ext1 s hs

Result:
case inr.h
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
h0 : NeZero μ
s : Set α
hs : MeasurableSet s
⊢ ((μ.tilted f).tilted g) s = (μ.tilted (f + g)) s

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable (fun x => rexp (f x)) μ
g : α → ℝ
⊢ (μ.tilted f).tilted g = μ.tilted (f + g)

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]
  field_simp
  ring_nf
  congr 1
  rw [mul_assoc, mul_inv_cancel₀, mul_one]
  exact (integral_exp_pos hf).ne'

Result:
no goals