OAI/Analysis/Daugavet/ClosedUnion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactModuli.KW.constructedSpace_infiniteDimensional line 11
2. lemma OAI.ExactModuli.KW.constructed_union_approx line 22
3. lemma OAI.ExactModuli.KW.constructed_ball_approx line 30
4. lemma OAI.ExactModuli.KW.constructed_sphere_approx line 37
5. lemma OAI.ExactModuli.KW.stageError_tendsto line 49
6. lemma OAI.ExactModuli.KW.stageError_eventually_small line 54
7. lemma OAI.ExactModuli.KW.stage_ball_control line 59

   Source documentation

   The exact telescoping finite-stage error; the remaining tail equals 2 h_b.

   lemma stage_ball_control (b a : ℕ) (hba : b ≤ a) :
       ∀ g ∈ stageSpace a, ‖g‖ ≤ 1 → ∃ ψ ∈ stageSpace b, ‖ψ‖ ≤ 1 ∧
         measureDistance kwMeasure g ψ ≤ 2 * stageError b - 2 * stageError a := by
   …

   Mentions: OAI.ExactModuli.KW.stageSpace, OAI.ExactModuli.measureDistance, OAI.ExactModuli.kwMeasure, OAI.ExactModuli.KW.stageError

8. lemma OAI.ExactModuli.KW.stage_ball_control_uniform line 75
9. lemma OAI.ExactModuli.KW.constructed_ball_stage_control line 82
10. lemma OAI.ExactModuli.KW.constructedSpace_measurePrecompact line 92