OAI/Analysis/AffineBernstein/ActualTubeWeights.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.AffineBernstein.tubeMeasureDensity line 19

   Source comment

   The manuscript's invariant density `μ₀` on base times unit normals.

   def tubeMeasureDensity (n : ℕ) (H : S × E → ℝ) (bS : Module.Basis ι ℝ S)
       (bE : OrthonormalBasis (κ ⊕ Unit) ℝ E) (q : S × E) : ℝ :=
   …

2. lemma OAI.AffineBernstein.tube_dimension_eq line 24
3. lemma OAI.AffineBernstein.invariantTubeF_unit line 30
4. lemma OAI.AffineBernstein.tubeMeasureDensity_base line 39
5. lemma OAI.AffineBernstein.tubeMeasureDensity_angular line 49
6. lemma OAI.AffineBernstein.tubeBaseMatrix_eq_slice line 60