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

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
⊢ ContinuousOn f (Ici 0)

Tactic:
intro x hx

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
⊢ ContinuousWithinAt f (Ici 0) x

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
hx_pos : 0 < x
h : 0 < x → ContinuousWithinAt f (Ioi 0) x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
rw [continuousWithinAt_iff_continuousAt (Ioi_mem_nhds hx_pos)] at h

Result:
case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
hx_pos : 0 < x
h : 0 < x → ContinuousAt f x
⊢ ContinuousWithinAt f (Ici 0) x

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
hx_pos : 0 < x
h : 0 < x → ContinuousAt f x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
exact (h hx_pos).continuousWithinAt

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
⊢ ∀ᵐ (x : α) ∂ν, (μ.rnDeriv ν x).toReal ∈ Ici 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
⊢ f (μ univ).toReal = f (∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν)

Tactic:
rw [Measure.integral_toReal_rnDeriv hμν]

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
⊢ f (μ univ).toReal ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
calc f (μ univ).toReal
  = f (∫ x, (μ.rnDeriv ν x).toReal ∂ν) := by rw [Measure.integral_toReal_rnDeriv hμν]
_ ≤ ∫ x, f (μ.rnDeriv ν x).toReal ∂ν := by
  rw [← average_eq_integral, ← average_eq_integral]
  exact ConvexOn.map_average_le hf_cvx hf_cont' isClosed_Ici (by simp)
    Measure.integrable_toReal_rnDeriv hf_int

Result:
no goals

Proof state:
case inl
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hx : 0 ∈ Ici 0
⊢ ContinuousWithinAt f (Ici 0) 0

Tactic:
exact hf_cont

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
⊢ f (⨍ (x : α), (μ.rnDeriv ν x).toReal ∂ν) ≤ ⨍ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
exact ConvexOn.map_average_le hf_cvx hf_cont' isClosed_Ici (by simp)
  Measure.integrable_toReal_rnDeriv hf_int

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
rcases eq_or_lt_of_le (α := ℝ) (hx : 0 ≤ x) with rfl | hx_pos

Result:
case inl
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hx : 0 ∈ Ici 0
⊢ ContinuousWithinAt f (Ici 0) 0

case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
hx_pos : 0 < x
⊢ ContinuousWithinAt f (Ici 0) x

Proof state:
case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
hx_pos : 0 < x
⊢ ContinuousWithinAt f (Ici 0) x

Tactic:
have h := hf_cvx.continuousOn_interior x

Result:
case inr
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
x : ℝ
hx : x ∈ Ici 0
hx_pos : 0 < x
h : x ∈ interior (Ici 0) → ContinuousWithinAt f (interior (Ici 0)) x
⊢ ContinuousWithinAt f (Ici 0) x

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
⊢ f (∫ (x : α), (μ.rnDeriv ν x).toReal ∂ν) ≤ ∫ (x : α), f (μ.rnDeriv ν x).toReal ∂ν

Tactic:
rw [← average_eq_integral, ← average_eq_integral]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
f : ℝ → ℝ
inst✝¹ : IsFiniteMeasure μ
inst✝ : IsProbabilityMeasure ν
hf_cvx : ConvexOn ℝ (Ici 0) f
hf_cont : ContinuousWithinAt f (Ici 0) 0
hf_int : Integrable (fun x => f (μ.rnDeriv ν x).toReal) ν
hμν : μ ≪ ν
hf_cont' : ContinuousOn f (Ici 0)
⊢ f (⨍ (x : α), (μ.rnDeriv ν x).toReal ∂ν) ≤ ⨍ (x : α), f (μ.rnDeriv ν x).toReal ∂ν