OAI/Geometry/RuledCovering/Hyperbolic.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.RuledApproximation.physicalHyperbolic line 13

   Source documentation

   Scaled-plane approximation under every Euclidean isometry.

   theorem physicalHyperbolic : PhysicalHyperbolicStatement := by
   …

   Mentions: OAI.RuledApproximation.PhysicalHyperbolicStatement

2. lemma OAI.RuledApproximation.norm_plane_sq line 17
3. lemma OAI.RuledApproximation.physicalWeight_one line 20
4. def OAI.RuledApproximation.cycleCoordinates line 26

   Source documentation

   Cyclic permutation from the transverse physical normalization to (p+rv,r).

   def cycleCoordinates : Space ≃ₗᵢ[ℝ] Space where
   …

   Mentions: OAI.RuledApproximation.Space

5. lemma OAI.RuledApproximation.cycle_physicalRuled line 41
6. theorem OAI.RuledApproximation.hyperbolic line 54

   Source documentation

   General hyperbolic approximation: arbitrary compact labels, including positive-area frontiers and area-zero sets.

   theorem hyperbolic : HyperbolicStatement := by
   …

   Mentions: OAI.RuledApproximation.HyperbolicStatement