OAI/Analysis/Daugavet/Stages.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ExactModuli.KW.ConstructionStage line 12

   Source documentation

   One finite-coordinate stage of the construction.

   structure ConstructionStage where
   …

2. structure OAI.ExactModuli.KW.StepEstimates line 19

   Source documentation

   All estimates propagated from one stage to the next.

   structure StepEstimates (G H : Submodule ℝ KWL1) (h : ℝ) : Prop where
   …

   Mentions: OAI.ExactModuli.H, OAI.ExactModuli.KW.KWL1

3. lemma OAI.ExactModuli.KW.stage_enlargement line 28
4. def OAI.ExactModuli.KW.oneVector line 74

   Source documentation

   The constant-one vector, so the initial stage is literally span{1}.

   def oneVector : KWL1 := Lp.const 1 kwMeasure (1:ℝ)

   Mentions: OAI.ExactModuli.KW.KWL1, OAI.ExactModuli.kwMeasure

5. lemma OAI.ExactModuli.KW.oneVector_norm line 76
6. lemma OAI.ExactModuli.KW.oneVector_finiteCoordinates line 79
7. def OAI.ExactModuli.KW.initialStage line 94
8. def OAI.ExactModuli.KW.stageError line 106
9. lemma OAI.ExactModuli.KW.stageError_pos line 108
10. lemma OAI.ExactModuli.KW.stageError_lt_one line 110
11. lemma OAI.ExactModuli.KW.stageError_succ line 114
12. def OAI.ExactModuli.KW.nextStage line 118
13. lemma OAI.ExactModuli.KW.nextStage_estimates line 121
14. def OAI.ExactModuli.KW.stages line 125
15. def OAI.ExactModuli.KW.stageSpace line 129
16. instance OAI.ExactModuli.KW.stageSpace_finite line 131
17. lemma OAI.ExactModuli.KW.stageSpace_nonzero line 134
18. lemma OAI.ExactModuli.KW.step_estimates line 136
19. lemma OAI.ExactModuli.KW.stageSpace_strictMono line 139
20. lemma OAI.ExactModuli.KW.stageSpace_mono line 142
21. def OAI.ExactModuli.KW.unionSpace line 144
22. def OAI.ExactModuli.KW.constructedSpace line 146
23. lemma OAI.ExactModuli.KW.stageSpace_le_constructed line 148
24. lemma OAI.ExactModuli.KW.constructedSpace_closed line 151
25. lemma OAI.ExactModuli.KW.constructedSpace_nonzero line 154