OAI/Analysis/AffineBernstein/ProjectiveWeightContinuity.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.continuousAt_supportConormal line 18
2. lemma OAI.AffineBernstein.continuousAt_inverseMatrixPair line 27
3. lemma OAI.AffineBernstein.continuousAt_sphericalInverseArea line 37
4. lemma OAI.AffineBernstein.lintegral_smul_jacobian line 59
5. lemma OAI.AffineBernstein.projective_norm_pos line 72
6. lemma OAI.AffineBernstein.lintegral_pow_Ioo line 80

   Source comment

   Exact radial slice integral, retaining the dimension-zero tangent endpoint.

   lemma lintegral_pow_Ioo {k : ℕ} {r : ℝ} (hr : 0 < r) :
       (∫⁻ t in Ioo 0 r, ENNReal.ofReal (t^k)) = ENNReal.ofReal (r^(k+1)/(k+1)) := by
   …