ProjectiveDensity.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.AffineBernstein.projective_area_exponents line 14

lemma OAI.AffineBernstein.homogeneous_projective_area_density line 41

Source comment

Exact projective-normal normalization of the affine area density. The factor is c^(-m), where m is the transverse dimension, including m=1. This is the density factor needed to pass from flat to spherical charts.

lemma homogeneous_projective_area_density {K : S → Set E} {s : S} {e : E}
    {D : Set S} (hD : IsOpen D) (hs : s ∈ D)
    (hK : ∀ y ∈ D, IsCompact (K y)) (hne : ∀ y ∈ D, (K y).Nonempty)
    {c : ℝ} (hc : 0 < c) (he : ‖e‖ = 1)
    (hH : ContDiffAt ℝ ∞ (fun q : S × E => homogeneousSupport (K q.1) q.2) (s,e))
    (hHc : ContDiffAt ℝ ∞ (fun q : S × E => homogeneousSupport (K q.1) q.2) (s,c • e))
    (bS : Module.Basis ι ℝ S) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E)
    (hflat : inner ℝ (c • e) (bE (Sum.inr ())) = 1)
    (hrad : ∀ v : E, fderiv ℝ (fderiv ℝ
      (fun q : S × E => homogeneousSupport (K q.1) q.2)) (s,c • e) (0,v) (0,c • e) = 0)
    (hB : 0 ≤ (tubeBaseMatrix (fun q : S × E => homogeneousSupport (K q.1) q.2) (s,e) bS).det)
    (hQ : 0 ≤ tubeAngularDensity (fun q : S × E => homogeneousSupport (K q.1) q.2) (s,e) bE) :
…

Mentions: OAI.AffineBernstein.homogeneousSupport, OAI.AffineBernstein.tubeBaseMatrix, OAI.AffineBernstein.tubeAngularDensity