OAI/Analysis/SeparableQuotients/NormingOperations.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SeparableQuotient.Norming.Family.reciprocal_summable line 10
  2. lemma OAI.SeparableQuotient.Norming.TypeII.coefficient_le_one line 15
  3. lemma OAI.SeparableQuotient.Norming.TypeII.hit_weight_injective line 25
  4. lemma OAI.SeparableQuotient.Norming.TypeII.coefficient_bound line 36
  5. lemma OAI.SeparableQuotient.Norming.stage_coefficient_bound line 101
  6. lemma OAI.SeparableQuotient.Norming.pureBase_coefficient_bound line 117
  7. lemma OAI.SeparableQuotient.Norming.pure_coefficient_bound line 123
  8. lemma OAI.SeparableQuotient.Norming.full_coefficient_bound line 128
  9. lemma OAI.SeparableQuotient.Norming.restrict_support_subset line 136
  10. lemma OAI.SeparableQuotient.Norming.restrict_zero line 139
  11. lemma OAI.SeparableQuotient.Norming.restrict_smul line 141
  12. lemma OAI.SeparableQuotient.Norming.restrict_sum line 146
  13. lemma OAI.SeparableQuotient.Norming.restrict_restrict line 149
  14. def OAI.SeparableQuotient.Norming.Crop.inter line 154
  15. lemma OAI.SeparableQuotient.Norming.Crop.inter_set line 158
  16. lemma OAI.SeparableQuotient.Norming.Successive.restrict line 162
  17. lemma OAI.SeparableQuotient.Norming.TypeII.active_crop_subset line 167
  18. def OAI.SeparableQuotient.Norming.TypeII.cropped line 179

    Source documentation

    Crops of Type II expressions retain the original paths and coding.

    def TypeII.cropped {f : Family} (e : TypeII f) (A : Crop) : TypeII f where
…

    Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.TypeII, OAI.SeparableQuotient.Norming.Crop

  19. lemma OAI.SeparableQuotient.Norming.TypeII.cropped_value line 188
  20. lemma OAI.SeparableQuotient.Norming.TypeI.crop_cases line 200

    Source documentation

    The crop operation discards zero children in order.

    lemma TypeI.crop_cases {f : Family} (e : TypeI f) (A : Set Γ) :
    restrict A e.value = 0 ∨ ∃ d : TypeI f,
      d.weight = e.weight ∧ d.value = restrict A e.value ∧
      ∀ i, ∃ j, d.child i = restrict A (e.child j) := by
…

    Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.TypeI, OAI.SeparableQuotient.Norming.Γ, OAI.SeparableQuotient.Norming.restrict

  21. lemma OAI.SeparableQuotient.Norming.stage_zero line 238
  22. lemma OAI.SeparableQuotient.Norming.stage_crop line 241
  23. lemma OAI.SeparableQuotient.Norming.pureBase_zero line 263
  24. lemma OAI.SeparableQuotient.Norming.pureBase_crop line 265
  25. lemma OAI.SeparableQuotient.Norming.pure_zero line 276
  26. lemma OAI.SeparableQuotient.Norming.pure_crop line 278
  27. lemma OAI.SeparableQuotient.Norming.TypeI.zero_at line 289
  28. lemma OAI.SeparableQuotient.Norming.FinitePath.zero_at line 293
  29. lemma OAI.SeparableQuotient.Norming.TypeII.zero_at line 301
  30. lemma OAI.SeparableQuotient.Norming.stage_vanish line 310
  31. lemma OAI.SeparableQuotient.Norming.pure_vanish line 323
  32. lemma OAI.SeparableQuotient.Norming.pure_mixed_crop line 334
  33. lemma OAI.SeparableQuotient.Norming.full_zero line 343
  34. lemma OAI.SeparableQuotient.Norming.full_crop line 345
  35. lemma OAI.SeparableQuotient.Norming.Successive.neg line 365
  36. def OAI.SeparableQuotient.Norming.TypeI.neg line 370
  37. lemma OAI.SeparableQuotient.Norming.TypeI.neg_value line 380
  38. def OAI.SeparableQuotient.Norming.TypeII.neg line 384
  39. lemma OAI.SeparableQuotient.Norming.TypeII.neg_value line 392
  40. lemma OAI.SeparableQuotient.Norming.stage_neg line 396
  41. lemma OAI.SeparableQuotient.Norming.pure_neg line 408
  42. lemma OAI.SeparableQuotient.Norming.full_neg line 417