-- 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 e_a
α : 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 ν
⊢ (fun x => f (μ'.rnDeriv ν' x).toReal) =ᶠ[ae ν] fun x => f (μ.rnDeriv ν x).toReal

Tactic:
filter_upwards [h_rnDeriv_eq] with x hx

Result:
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 ν
x : α
hx : μ'.rnDeriv ν' x = μ.rnDeriv ν x
⊢ f (μ'.rnDeriv ν' x).toReal = f (μ.rnDeriv ν x).toReal

Proof state:
α : 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μν' : μ' ≪ ν'
⊢ (ν univ)⁻¹ ≠ ⊤

Tactic:
simp [hν]

Result:
no goals

Proof state:
α : 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 ν
⊢ μ'.rnDeriv ν' =ᶠ[ae ν] μ.rnDeriv ν

Tactic:
filter_upwards [h1, h2] with x h1 h2

Result:
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
⊢ μ'.rnDeriv ν' x = μ.rnDeriv ν x

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 ν
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 ∂ν

Tactic:
have h : f (μ' univ).toReal ≤ ∫ x, f (μ'.rnDeriv ν' x).toReal ∂ν' :=
  le_integral_rnDeriv_of_ac hf_cvx hf_cont ?_ hμν'

Result:
case neg.refine_2
α : 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 : f (μ' univ).toReal ≤ ∫ (x : α), f (μ'.rnDeriv ν' x).toReal ∂ν'
⊢ (ν univ).toReal * f ((μ univ).toReal / (ν univ).toReal) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

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μν' : μ' ≪ ν'
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
⊢ μ'.rnDeriv ν' x = μ.rnDeriv ν x

Tactic:
rw [h1, Pi.smul_apply, smul_eq_mul, h2]

Result:
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