OAI/Analysis/AffineBernstein/GeneralCapCoordinates.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.AffineBernstein.exists_height_coordinates line 19

   Source comment

   A fixed genuine invertible coordinate map with the prescribed height functional. The product max norm is retained; no artificial inner-product instance is introduced on these coordinates.

   lemma exists_height_coordinates {n : ℕ}
       (ell : (Space n × ℝ) →L[ℝ] ℝ) (hne : ell ≠ 0) :
       ∃ A : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ), ∀ z, (A z).2 = ell z := by
   …

   Mentions: OAI.AffineBernstein.Space

2. def OAI.AffineBernstein.affineImageLinearCapArea line 36

   Source comment

   The affine-area cap for an arbitrary linear height, in the original literal graph chart.

   def affineImageLinearCapArea {n : ℕ} (Ω : Set (Space n)) (u : Space n → ℝ)
       (L : (Space n × ℝ) ≃L[ℝ] (Space n × ℝ)) (v : Space n × ℝ)
       (ell : (Space n × ℝ) →L[ℝ] ℝ) (b : ℝ) : ℝ :=
   …

   Mentions: OAI.AffineBernstein.Space

3. lemma OAI.AffineBernstein.affineImageCapArea_height_coordinates line 42
4. lemma OAI.AffineBernstein.image_height_cap line 58