OAI/Analysis/AffineBernstein/ConvexGradientBound.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.convex_fderiv_support line 15
2. lemma OAI.AffineBernstein.norm_le_card_of_coord_bound line 36
3. def OAI.AffineBernstein.graphProjection line 49

   Source documentation

   Projection to the coordinate hyperplane omitting the i-th original base coordinate, represented in its standard n coordinates.

   def graphProjection (u : Space n → ℝ) (i : Fin n) (x : Space n) : Space n :=
   …

   Mentions: OAI.AffineBernstein.Space

4. lemma OAI.AffineBernstein.contDiffAt_graphProjection line 52
5. lemma OAI.AffineBernstein.det_fderiv_graphProjection line 61
6. lemma OAI.AffineBernstein.graphProjection_difference line 85
7. lemma OAI.AffineBernstein.graphProjection_injOn_signed line 98
8. lemma OAI.AffineBernstein.reciprocalChart_coord_le_one line 126
9. lemma OAI.AffineBernstein.lintegral_geometric_mean_le line 141

   Source documentation

   Holder interpolation, with weights rather than reciprocal exponents. The endpoint masses may be infinite; no hidden integrability premise is used.

   lemma lintegral_geometric_mean_le {X : Type*} [MeasurableSpace X] (μ : Measure X)
       {p : ℝ} (hp : 0 < p) (hp1 : p < 1) {f g : X → ℝ≥0∞}
       (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) :
       (∫⁻ x, f x ^ p * g x ^ (1-p) ∂μ) ≤
         (∫⁻ x, f x ∂μ)^p * (∫⁻ x, g x ∂μ)^(1-p) := by
   …

10. lemma OAI.AffineBernstein.lintegral_ofReal_geometric_mean_le line 155

    Source documentation

    Real positive densities can be interpolated before or after ofReal.

    lemma lintegral_ofReal_geometric_mean_le {X : Type*} [MeasurableSpace X] (μ : Measure X)
        {p : ℝ} (hp : 0 < p) (hp1 : p < 1) {f g : X → ℝ}
        (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
        (hfp : ∀ᵐ x ∂μ, 0 ≤ f x) (hgp : ∀ᵐ x ∂μ, 0 ≤ g x) :
        (∫⁻ x, ENNReal.ofReal ((f x)^p * (g x)^(1-p)) ∂μ) ≤
          (∫⁻ x, ENNReal.ofReal (f x) ∂μ)^p *
          (∫⁻ x, ENNReal.ofReal (g x) ∂μ)^(1-p) := by
    …