OAI/Analysis/SeparableQuotients/PartitionBlocks.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SeparableQuotient.ActualSpace.ordinalHull line 11
  2. lemma OAI.SeparableQuotient.ActualSpace.ordinalHull_connected line 14
  3. lemma OAI.SeparableQuotient.ActualSpace.mem_ordinalHull line 17
  4. lemma OAI.SeparableQuotient.ActualSpace.ordinalHull_successive line 20
  5. def OAI.SeparableQuotient.ActualSpace.intervalProjection line 26
  6. lemma OAI.SeparableQuotient.ActualSpace.abs_eval_supported_interval line 29
  7. def OAI.SeparableQuotient.ActualSpace.PartitionBound line 46

    Source documentation

    An interval-partition inequality and its constant-16 difference-vector version. Intervals may be unbounded or singletons.

    def PartitionBound (x : E) (N : ℕ) (A r : ℝ) : Prop :=
…

    Mentions: OAI.SeparableQuotient.ActualSpace.E

  8. lemma OAI.SeparableQuotient.ActualSpace.typeI_eval_le_of_partition line 51
  9. def OAI.SeparableQuotient.ActualSpace.BlockSequence.tailSpan line 90

    Source documentation

    Algebraic finite blocks in the specified tail, with no completion added.

    noncomputable def BlockSequence.tailSpan {f : Family} (z : BlockSequence f) (a : ℕ) :
    Submodule ℝ (Γ →₀ ℝ) := Submodule.span ℝ (Set.range (fun n => z.vector (n+a)))

    Mentions: OAI.SeparableQuotient.ActualSpace.BlockSequence

  10. structure OAI.SeparableQuotient.ActualSpace.UnitBlocks line 93
  11. lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.nonzero line 101
  12. def OAI.SeparableQuotient.ActualSpace.UnitBlocks.select line 106
  13. lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.select_sum line 114
  14. def OAI.SeparableQuotient.ActualSpace.BlockSequence.unitBlocks line 121
  15. def OAI.SeparableQuotient.ActualSpace.blockSumSup line 135
  16. lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.norm_sum_le_length line 138
  17. lemma OAI.SeparableQuotient.ActualSpace.blockSumSup_bdd line 143
  18. lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.norm_sum_le_sup line 147
  19. lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.norm_subsum_le_sup line 151
  20. lemma OAI.SeparableQuotient.ActualSpace.blockSumSup_le_length line 156
  21. lemma OAI.SeparableQuotient.ActualSpace.blockSumSup_nonneg line 162
  22. lemma OAI.SeparableQuotient.ActualSpace.unitBlocks_near_sup line 167
  23. def OAI.SeparableQuotient.ActualSpace.vectorCrop line 181
  24. lemma OAI.SeparableQuotient.ActualSpace.support_mem_vectorCrop line 188
  25. lemma OAI.SeparableQuotient.ActualSpace.vectorCrop_successive line 198
  26. lemma OAI.SeparableQuotient.ActualSpace.family_norming_crop line 217
  27. lemma OAI.SeparableQuotient.ActualSpace.exists_unit_vector_normer line 223
  28. lemma OAI.SeparableQuotient.ActualSpace.evaluateArray_finite_disjoint line 254
  29. lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.norm_sum_lower line 262