OAI/Analysis/AffineBernstein/TubeDensity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.tubeAffineAreaJet line 19

   Source comment

   The actual second-jet affine-area density in the base and orthonormal angular directions; the transverse column is (0,-e).

   def tubeAffineAreaJet (H : S × E → ℝ) (Y : S × E → E) (x : S × E)
       (bS : Module.Basis ι ℝ S) (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E) : ℝ :=
   …

2. lemma OAI.AffineBernstein.tubeAffineAreaJet_eq line 27
3. lemma OAI.AffineBernstein.supportConormal_transverse line 51
4. lemma OAI.AffineBernstein.supportConormal_inward_velocity line 58