OAI/Analysis/SeparableQuotients/TailBlocks.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.support_mem_tail line 11
  2. def OAI.SeparableQuotient.ActualSpace.BlockSequence.prefixSupport line 33
  3. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.prefixSupport_mono line 36
  4. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.support_subset_prefix line 40
  5. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.prefix_tail_successive line 65
  6. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.tailSpan_mono line 74
  7. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.tail_pure_color line 83
  8. def OAI.SeparableQuotient.ActualSpace.BlockSequence.prefixRho line 96
  9. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.le_prefixRho line 99
  10. structure OAI.SeparableQuotient.ActualSpace.PreliminaryData line 106

    Source documentation

    The recursively selected unit blocks, before pathwise-Cauchy differences. No weak compactness hypothesis is smuggled into this structure.

    structure PreliminaryData {f : Family} (z : BlockSequence f) (J : ℕ) (ε : ℝ) (n : ℕ) where
…

    Mentions: OAI.SeparableQuotient.ActualSpace.BlockSequence

  11. lemma OAI.SeparableQuotient.ActualSpace.exists_preliminaryData line 123
  12. def OAI.SeparableQuotient.ActualSpace.preliminaryChoice line 150
  13. lemma OAI.SeparableQuotient.ActualSpace.preliminaryChoice_spec line 153
  14. def OAI.SeparableQuotient.ActualSpace.preliminaryData line 157
  15. lemma OAI.SeparableQuotient.ActualSpace.preliminaryData_start_zero line 163
  16. lemma OAI.SeparableQuotient.ActualSpace.preliminaryData_start_succ line 166
  17. lemma OAI.SeparableQuotient.ActualSpace.preliminaryData_order_succ line 170
  18. lemma OAI.SeparableQuotient.ActualSpace.preliminaryData_start_mono line 174
  19. lemma OAI.SeparableQuotient.ActualSpace.preliminaryData_finish_le_start line 181
  20. lemma OAI.SeparableQuotient.ActualSpace.preliminaryData_order line 187
  21. def OAI.SeparableQuotient.ActualSpace.preliminaryBlocks line 196
  22. lemma OAI.SeparableQuotient.ActualSpace.preliminaryData_coherence line 207
  23. lemma OAI.SeparableQuotient.SeriesTails.tail_antitone line 224
  24. lemma OAI.SeparableQuotient.ActualSpace.vectorL1_eq_sum line 242
  25. lemma OAI.SeparableQuotient.ActualSpace.vectorL1_sub_le line 248
  26. lemma OAI.SeparableQuotient.ActualSpace.PartitionBound.mono line 254
  27. lemma OAI.SeparableQuotient.ActualSpace.PartitionBound.sub line 257
  28. def OAI.SeparableQuotient.ActualSpace.BlockSequence.subsequence line 271
  29. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.norm_sub_ge_one line 278
  30. def OAI.SeparableQuotient.ActualSpace.BlockSequence.pairDifferences line 298
  31. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.pairDifferences_norm line 316
  32. lemma OAI.SeparableQuotient.ActualSpace.BlockSequence.pairDifferences_path_null line 324