RenyiTangent.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The finite Rényi tangent inequality

This is the scalar and integral tangent inequality used to differentiate the original curvature-dimension transport bound at a positive density. The exponent stays strictly below one.

theorem OAI.RegularPointCoordinates.rpow_tangent_upper line 18

theorem OAI.RegularPointCoordinates.integral_rpow_tangent_upper line 44

Source documentation

The density tangent is integrable even when the comparison density vanishes. Only the reference density has to be bounded below.

theorem integral_rpow_tangent_upper (ρ η : X → ℝ) (hρ : Measurable ρ) (hη : Measurable η)
    (hρi : Integrable ρ μ) (hηi : Integrable η μ) {ε q : ℝ} (hε : 0<ε)
    (hρ0 : ∀ᵐ x ∂μ, ε≤ρ x) (hη0 : ∀ᵐ x ∂μ, 0≤η x)
    (hq0 : 0<q) (hq1 : q<1) :
    Integrable (fun x => ρ x^(q-1)*η x) μ ∧
    (∫ x, η x^q ∂μ)≤(1-q)*(∫ x, ρ x^q ∂μ)+q*(∫ x, ρ x^(q-1)*η x ∂μ) := by
…