OAI/Analysis/Daugavet/FiniteCoordinates.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.ExactModuli.KW.kwMeasure_probability line 13
2. abbrev OAI.ExactModuli.KW.KWL1 line 17
3. def OAI.ExactModuli.KW.coordinatesL1 line 20

   Source documentation

   Coordinate restriction induces an actual L1 linear isometry.

   def coordinatesL1 {ι : Type uIota} [Fintype ι] (c : ι → ℕ) (hc : Function.Injective c) :
       Lp ℝ 1 (cubeMeasure ι) →ₗᵢ[ℝ] KWL1 :=
   …

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

4. def OAI.ExactModuli.KW.FiniteCoordinates line 25

   Source documentation

   A common finite family of coordinates determines the whole subspace.

   def FiniteCoordinates (G : Submodule ℝ KWL1) : Prop :=
   …

   Mentions: OAI.ExactModuli.KW.KWL1

5. lemma OAI.ExactModuli.KW.extend_coordinates line 29
6. lemma OAI.ExactModuli.KW.curry_mp line 58
7. def OAI.ExactModuli.KW.splitCoordinates line 66
8. lemma OAI.ExactModuli.KW.splitCoordinates_mp line 70
9. def OAI.ExactModuli.KW.integrableL1 line 81
10. lemma OAI.ExactModuli.KW.integrableL1_ae line 84
11. lemma OAI.ExactModuli.KW.L1_norm_of_ae line 87
12. lemma OAI.ExactModuli.KW.norm_integrableL1 line 92
13. lemma OAI.ExactModuli.KW.coeFn_L1_sum line 95
14. lemma OAI.ExactModuli.KW.coeFn_L1_smul_sum line 107
15. def OAI.ExactModuli.KW.oldL1 line 116
16. lemma OAI.ExactModuli.KW.oldL1_ae line 120