OAI/Analysis/AffineBernstein/SigmaCapHelpers.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.tubeAngularDensity_reindex line 18
2. lemma OAI.AffineBernstein.one_le_norm_supportConormal line 31

   Source documentation

   The unnormalized support conormal has norm at least one at every unit normal. This is independent of graph stationarity and uses the product norm literally.

   lemma one_le_norm_supportConormal (H : S × E → ℝ) (s : S) {e : E} (he : ‖e‖ = 1) :
       1 ≤ ‖supportConormal H (s,e)‖ := by
   …

   Mentions: OAI.AffineBernstein.supportConormal

3. def OAI.AffineBernstein.capTiltedForm line 42

   Source documentation

   The actual continuous linear forms chosen in bounds.tex256.

   def capTiltedForm {k : ℕ} (j : Fin k) : Space k →L[ℝ] ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

4. lemma OAI.AffineBernstein.capTiltedForm_apply line 44
5. lemma OAI.AffineBernstein.capTiltedForm_basis line 47