OAI/Analysis/SeparableQuotients/NormingTrees.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SeparableQuotient.Norming.TypeI.value_ne_zero line 11
  2. def OAI.SeparableQuotient.Norming.TypeI.singletonMetadata line 28
  3. def OAI.SeparableQuotient.Norming.TypeI.singletonRaw line 31
  4. lemma OAI.SeparableQuotient.Norming.TypeI.singletonRaw_valid line 37
  5. def OAI.SeparableQuotient.Norming.TypeI.singletonPath line 55
  6. lemma OAI.SeparableQuotient.Norming.TypeI.singletonPath_value line 65
  7. def OAI.SeparableQuotient.Norming.TypeI.toTypeII line 69
  8. lemma OAI.SeparableQuotient.Norming.TypeI.toTypeII_value line 71
  9. def OAI.SeparableQuotient.ActualSpace.TypeI.childRange line 80
  10. lemma OAI.SeparableQuotient.ActualSpace.TypeI.childRange_connected line 83
  11. lemma OAI.SeparableQuotient.ActualSpace.TypeI.mem_childRange line 86
  12. lemma OAI.SeparableQuotient.ActualSpace.TypeI.childRange_successive line 89
  13. def OAI.SeparableQuotient.ActualSpace.TypeI.hitChildren line 93
  14. lemma OAI.SeparableQuotient.ActualSpace.TypeI.cropped_child_zero line 96
  15. lemma OAI.SeparableQuotient.ActualSpace.TypeI.cropped_child_bound line 109
  16. lemma OAI.SeparableQuotient.ActualSpace.TypeI.cropped_child_sum_bound line 116
  17. lemma OAI.SeparableQuotient.ActualSpace.TypeI.hitChildren_noncrossing line 148
  18. lemma OAI.SeparableQuotient.ActualSpace.TypeI.boundary_incidence line 159
  19. lemma OAI.SeparableQuotient.FiniteVectors.vec_sum line 174
  20. lemma OAI.SeparableQuotient.FiniteVectors.norm_sum_disjoint_le line 180
  21. lemma OAI.SeparableQuotient.FiniteVectors.norm_degree_le line 195
  22. lemma OAI.SeparableQuotient.FiniteVectors.norm_le_sum_norm line 212
  23. lemma OAI.SeparableQuotient.FiniteVectors.sum_abs_le_holder line 227
  24. abbrev OAI.SeparableQuotient.ActualSpace.TypeII.Group line 246
  25. def OAI.SeparableQuotient.ActualSpace.TypeII.groupValue line 248
  26. def OAI.SeparableQuotient.ActualSpace.TypeII.groupWeight line 251
  27. def OAI.SeparableQuotient.ActualSpace.TypeII.activeGroups line 254
  28. lemma OAI.SeparableQuotient.ActualSpace.TypeII.groupWeight_active line 257
  29. lemma OAI.SeparableQuotient.ActualSpace.TypeII.groupWeight_injOn line 264
  30. lemma OAI.SeparableQuotient.ActualSpace.TypeII.value_group_sum line 280
  31. lemma OAI.SeparableQuotient.ActualSpace.TypeII.eval_group_sum line 295
  32. lemma OAI.SeparableQuotient.ActualSpace.typeI_cropped_eval_le_l1 line 301
  33. lemma OAI.SeparableQuotient.ActualSpace.TypeII.high_weight_bound line 320