OAI/Analysis/SeparableQuotients/NormingFamilies.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SeparableQuotient.Norming.Γ line 10
  2. abbrev OAI.SeparableQuotient.Norming.Array line 11
  3. inductive OAI.SeparableQuotient.Norming.Family line 13
  4. def OAI.SeparableQuotient.Norming.Family.s line 18
  5. lemma OAI.SeparableQuotient.Norming.Family.s_ge_two line 22
  6. def OAI.SeparableQuotient.Norming.Family.q line 24
  7. def OAI.SeparableQuotient.Norming.Family.L line 26
  8. def OAI.SeparableQuotient.Norming.Family.m line 27
  9. lemma OAI.SeparableQuotient.Norming.Family.m_pos line 29
  10. def OAI.SeparableQuotient.Norming.Successive line 32

    Source documentation

    Succession refers to the full supports, in both orders in mixed mode.

    def Successive (f : Family) (x y : Array) : Prop :=
…

    Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.Array

  11. lemma OAI.SeparableQuotient.Norming.Successive.disjoint line 36
  12. structure OAI.SeparableQuotient.Norming.Crop line 42
  13. def OAI.SeparableQuotient.Norming.Crop.set line 48
  14. def OAI.SeparableQuotient.Norming.restrict line 52
  15. lemma OAI.SeparableQuotient.Norming.restrict_apply line 54
  16. structure OAI.SeparableQuotient.Norming.TypeI line 59

    Source documentation

    A specified Type I expression. Child norming membership is imposed at its construction stage, outside this data structure.

    structure TypeI (f : Family) where
…

    Mentions: OAI.SeparableQuotient.Norming.Family

  17. def OAI.SeparableQuotient.Norming.TypeI.value line 69
  18. structure OAI.SeparableQuotient.Norming.PrefixValid line 74

    Source documentation

    Exactly the finite prefix conditions, with unused raw entries ignored. Padding raw data beyond length imposes no mathematical restriction.

    structure PrefixValid (P : RawPath) (length : ℕ) : Prop where
…
  19. lemma OAI.SeparableQuotient.Norming.PrefixValid.weight_strict line 85
  20. structure OAI.SeparableQuotient.Norming.FinitePath line 97
  21. def OAI.SeparableQuotient.Norming.FinitePath.value line 108
  22. def OAI.SeparableQuotient.Norming.FinitePath.active line 110
  23. structure OAI.SeparableQuotient.Norming.TypeII line 114
  24. def OAI.SeparableQuotient.Norming.TypeII.value line 123
  25. def OAI.SeparableQuotient.Norming.stage line 127

    Source documentation

    Each stage retains previous stages and adjoins expressions whose Type I children belong to previous stages, with uncropped path data.

    def stage (base : Set Array) (f : Family) : ℕ → Set Array
  | 0 => base
  | n+1 => stage base f n ∪
      {x | ∃ e : TypeI f, e.value = x ∧ ∀ h, e.child h ∈ stage base f n} ∪
      {x | ∃ e : TypeII f, e.value = x ∧
        ∀ b i h, ((e.path b).piece i).child h ∈ stage base f n}

    Mentions: OAI.SeparableQuotient.Norming.Array, OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.TypeI, OAI.SeparableQuotient.Norming.TypeII

  26. def OAI.SeparableQuotient.Norming.pureBase line 134
  27. def OAI.SeparableQuotient.Norming.Pure line 138
  28. def OAI.SeparableQuotient.Norming.Full line 140
  29. lemma OAI.SeparableQuotient.Norming.stage_mono line 142
  30. lemma OAI.SeparableQuotient.Norming.pure_subset_full line 147
  31. lemma OAI.SeparableQuotient.Norming.coordinate_mem line 151
  32. lemma OAI.SeparableQuotient.Norming.successive_coefficient_unique line 161
  33. lemma OAI.SeparableQuotient.Norming.TypeI.coefficient_bound line 171
  34. def OAI.SeparableQuotient.Norming.FinitePath.hitIndex line 195

    Source documentation

    A coordinate meets at most one original path piece.

    def FinitePath.hitIndex {f : Family} (P : FinitePath f) (a : Γ) : Fin P.length :=
…

    Mentions: OAI.SeparableQuotient.Norming.Family, OAI.SeparableQuotient.Norming.FinitePath, OAI.SeparableQuotient.Norming.Γ

  35. lemma OAI.SeparableQuotient.Norming.FinitePath.value_at_hit line 199
  36. lemma OAI.SeparableQuotient.Norming.FinitePath.hit_weight_active line 215