OAI/Analysis/ForestSpace/Lens.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ForestSpace.bounded_finiteDimensional_pair line 16
2. theorem OAI.ForestSpace.norm_half_sum_le line 36
3. theorem OAI.ForestSpace.norm_le_signed_average line 40
4. theorem OAI.ForestSpace.norm_right_le_signed_average line 45
5. theorem OAI.ForestSpace.main_head_pair line 49
6. theorem OAI.ForestSpace.main_lens_aprox line 67
7. theorem OAI.ForestSpace.main_lens line 136

   Source documentation

   The squared separated-midpoint deficit.

    theorem main_lens (R ε : ℝ) (hR : 0 < R) (hε : 0 < ε)
       (x : FullDual Vertex) (y : ℕ → FullDual Vertex)
       (hp : ∀ j, ‖x+y j‖ ≤ R) (hm : ∀ j, ‖x-y j‖ ≤ R)
       (hs : ∀ i j, i ≠ j → ε ≤ ‖y i-y j‖) :
       ε^2/48 ≤ R^2-‖x‖^2 := by
   …

   Mentions: OAI.ForestSpace.FullDual, OAI.ForestSpace.Vertex