OAI/Analysis/Daugavet/ProductModels.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactModuli.KW.cube line 15
2. abbrev OAI.ExactModuli.KW.cubeMeasure line 16
3. abbrev OAI.ExactModuli.KW.pairCubeMeasure line 18
4. abbrev OAI.ExactModuli.KW.arrayMeasure line 20
5. abbrev OAI.ExactModuli.KW.pairedArrayMeasure line 23
6. lemma OAI.ExactModuli.KW.mp_integral line 27
7. lemma OAI.ExactModuli.KW.mp_ident line 34
8. def OAI.ExactModuli.KW.rowSum line 43
9. def OAI.ExactModuli.KW.diffRowSum line 45
10. lemma OAI.ExactModuli.KW.measurable_rowSum line 48
11. lemma OAI.ExactModuli.KW.measurable_diffRowSum line 52
12. lemma OAI.ExactModuli.KW.integrable_rowSum line 56
13. lemma OAI.ExactModuli.KW.integrable_diffRowSum line 63
14. lemma OAI.ExactModuli.KW.diffRowSum_lower line 70
15. lemma OAI.ExactModuli.KW.diffRowSum_tail line 78
16. def OAI.ExactModuli.KW.selectRows line 88

    Source documentation

    Select, independently at every row, one of each pair of resampled coordinates.

    def selectRows (b : κ → Bool) (v : κ → ι → unitInterval × unitInterval) : κ → cube ι :=
    …

    Mentions: OAI.ExactModuli.KW.cube

17. lemma OAI.ExactModuli.KW.measurePreserving_selectRows line 91