-- Mathlib/MeasureTheory/Decomposition/IntegralRNDeriv.lean
/-- For a convex continuous function `f` on `[0, ∞)`, if `μ` is absolutely continuous
with respect to `ν`, then
`(ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal) ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν`. -/
lemma mul_le_integral_rnDeriv_of_ac [IsFiniteMeasure μ] [IsFiniteMeasure ν]
    (hf_cvx : ConvexOn ℝ (Ici 0) f) (hf_cont : ContinuousWithinAt f (Ici 0) 0)
    (hf_int : Integrable (fun x ↦ f (μ.rnDeriv ν x).toReal) ν) (hμν : μ ≪ ν) :
    (ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal)
      ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1✝ : μ'.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2✝ : μ.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
x : α
h1 : μ'.rnDeriv ν' x = ((ν univ)⁻¹ • μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = ((ν univ)⁻¹⁻¹ • μ.rnDeriv ν) x
⊢ (ν univ)⁻¹ * (ν univ * μ.rnDeriv ν x) = μ.rnDeriv ν x

Tactic:
rw [← mul_assoc, ENNReal.inv_mul_cancel, one_mul]

Result:
case h.h0
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1✝ : μ'.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2✝ : μ.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
x : α
h1 : μ'.rnDeriv ν' x = ((ν univ)⁻¹ • μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = ((ν univ)⁻¹⁻¹ • μ.rnDeriv ν) x
⊢ ν univ ≠ 0

case h.ht
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h1' : μ'.rnDeriv ν' =ᶠ[ae ν'] (ν univ)⁻¹ • μ.rnDeriv ν'
h1✝ : μ'.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹ • μ.rnDeriv ν'
h2✝ : μ.rnDeriv ν' =ᶠ[ae ν] (ν univ)⁻¹⁻¹ • μ.rnDeriv ν
x : α
h1 : μ'.rnDeriv ν' x = ((ν univ)⁻¹ • μ.rnDeriv ν') x
h2 : μ.rnDeriv ν' x = ((ν univ)⁻¹⁻¹ • μ.rnDeriv ν) x
⊢ ν univ ≠ ⊤

Proof state:
case neg.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν univ).toReal⁻¹ * ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
⊢ Integrable (fun x => f (μ'.rnDeriv ν' x).toReal) ν'

Tactic:
refine Integrable.smul_measure ?_ (by simp [hν])

Result:
case neg.refine_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν univ).toReal⁻¹ * ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
⊢ Integrable (fun x => f (μ'.rnDeriv ν' x).toReal) ν

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν univ).toReal⁻¹ * ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
x : α
hx : μ'.rnDeriv ν' x = μ.rnDeriv ν x
⊢ f (μ'.rnDeriv ν' x).toReal = f (μ.rnDeriv ν x).toReal

Tactic:
rw [hx]

Result:
no goals

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
⊢ (ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
have h_eq : ∫ x, f (μ'.rnDeriv ν' x).toReal ∂ν'
    = (ν univ).toReal⁻¹ * ∫ x, f ((μ.rnDeriv ν x).toReal) ∂ν := by
  rw [integral_smul_measure, smul_eq_mul, ENNReal.toReal_inv]
  congr 1
  refine integral_congr_ae ?_
  filter_upwards [h_rnDeriv_eq] with x hx
  rw [hx]

Result:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν univ).toReal⁻¹ * ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
⊢ (ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

Proof state:
case h.e'_3.h.e'_6.h.e'_1
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsFiniteMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hν : ¬ν = 0
this✝ : NeZero ν
μ' : Measure α := (ν univ)⁻¹ • μ
ν' : Measure α := (ν univ)⁻¹ • ν
this : IsFiniteMeasure μ'
hμν' : μ' ≪ ν'
h_rnDeriv_eq : μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν
h_eq : ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν' = (ν univ).toReal⁻¹ * ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
h : (ν univ).toReal * f (μ' univ).toReal ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν
⊢ (μ univ).toReal / (ν univ).toReal = (μ' univ).toReal

Tactic:
simp only [div_eq_inv_mul, Measure.smul_apply, smul_eq_mul, ENNReal.toReal_mul,
ENNReal.toReal_inv, μ']

Result:
no goals