OAI/Analysis/AffineBernstein/SupportRadial.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.continuousAt_hessian line 17
2. lemma OAI.AffineBernstein.gaussPoint_pos_smul line 26
3. lemma OAI.AffineBernstein.homogeneousSupport_hessian_smul line 39
4. lemma OAI.AffineBernstein.support_cofactor_radial_expansion line 69
5. lemma OAI.AffineBernstein.sphere_lintegral_mul_radial_le line 89

   Source comment

   A homogeneous quantity which expands on inward rays has its spherical integral controlled by its integral over the punctured unit ball. The exact radial Haar normalization is retained.

   lemma sphere_lintegral_mul_radial_le {E : Type*} [NormedAddCommGroup E]
       [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E]
       (μ : Measure E) [μ.IsAddHaarMeasure] {f : E → ℝ≥0∞}
       (hf : Measurable (fun e : Metric.sphere (0:E) 1 => f e))
       (hscale : ∀ (e : Metric.sphere (0:E) 1) (r : ℝ), 0 < r → r < 1 → f e ≤ f (r • (e:E))) :
       (∫⁻ e : Metric.sphere (0:E) 1, f e ∂μ.toSphere) *
         ENNReal.ofReal (1 / ((Module.finrank ℝ E - 1 + 1 : ℕ):ℝ)) ≤
           ∫⁻ x in Metric.ball (0:E) 1 \ {0}, f x ∂μ := by
   …