Convexity results

noncomputable def Inv.deriv (x : ENNReal) : EReal

The derivative of the function Inv.inv on EReal.

Equations

• Inv.deriv x = if x = 0 then ⊤ else if x = ⊤ then 0 else ↑(deriv Inv.inv x.toReal)

@[simp]

theorem deriv_inv_ne_bot (x : ENNReal) : Inv.deriv x ≠ ⊥

theorem deriv_inv_ne_top {x : ENNReal} (hx : x ≠ 0) : Inv.deriv x ≠ ⊤

theorem Inv.le_add_deriv_mul {x y : ENNReal} (hx_top : x ≠ ⊤) (hy_zero : y ≠ 0) : ↑y⁻¹ + Inv.deriv y * (↑x - ↑y) ≤ ↑x⁻¹

theorem Inv.map_lintegral_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} [MeasureTheory.IsProbabilityMeasure μ] (hf : AEMeasurable f μ) (hf_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : (∫⁻ (x : α), f x ∂μ)⁻¹ ≤ ∫⁻ (x : α), (f x)⁻¹ ∂μ

theorem AEMeasurable.cond {α : Type u_1} [MeasurableSpace α] {t : Set α} {f : α → ENNReal} {μ : MeasureTheory.Measure α} (hf : AEMeasurable f (μ.restrict t)) : AEMeasurable f μ[|t]

theorem Inv.map_set_lintegral_le {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {t : Set α} {f : α → ENNReal} (ht : MeasurableSet t) (hf : AEMeasurable f (μ.restrict t)) (hμ_t₀ : μ t ≠ 0) (hμ_t₁ : μ t ≠ ⊤) (ht_top : ∀ᵐ (x : α) ∂μ, x ∈ t → f x ≠ ⊤) : μ t * (∫⁻ (x : α) in t, f x ∂μ)⁻¹ ≤ (μ t)⁻¹ * ∫⁻ (x : α) in t, (f x)⁻¹ ∂μ

theorem Inv.lt_add_deriv_mul {x y : ENNReal} (hx_top : x ≠ ⊤) (hy_zero : y ≠ 0) (hxy : x ≠ y) : ↑y⁻¹ + Inv.deriv y * (↑x - ↑y) < ↑x⁻¹

theorem Inv.ae_eq_const_or_map_lintegral_lt' {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} [MeasureTheory.IsProbabilityMeasure μ] (hf : Measurable f) (hf_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : f =ᵐ[μ] Function.const α (∫⁻ (x : α), f x ∂μ) ∨ (∫⁻ (x : α), f x ∂μ)⁻¹ < ∫⁻ (x : α), (f x)⁻¹ ∂μ

theorem Inv.ae_eq_const_or_map_lintegral_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal} [MeasureTheory.IsProbabilityMeasure μ] (hf : AEMeasurable f μ) (hf_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤) : f =ᵐ[μ] Function.const α (∫⁻ (x : α), f x ∂μ) ∨ (∫⁻ (x : α), f x ∂μ)⁻¹ < ∫⁻ (x : α), (f x)⁻¹ ∂μ

theorem Inv.ae_eq_const_or_map_set_lintegral_lt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {t : Set α} {f : α → ENNReal} (ht : MeasurableSet t) (hf : AEMeasurable f (μ.restrict t)) (hμ_t₀ : μ t ≠ 0) (hμ_t₁ : μ t ≠ ⊤) (ht_top : ∀ᵐ (x : α) ∂μ, x ∈ t → f x ≠ ⊤) : f =ᵐ[μ.restrict t] Function.const α ((μ t)⁻¹ * ∫⁻ (x : α) in t, f x ∂μ) ∨ μ t * (∫⁻ (x : α) in t, f x ∂μ)⁻¹ < (μ t)⁻¹ * ∫⁻ (x : α) in t, (f x)⁻¹ ∂μ