OAI/Analysis/SeparableQuotients/PathCoding.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SeparableQuotient.PathCoding.position line 14

   Source documentation

   Position of a coordinate in an ordered finite closure; no ordinal label is stored in the code.

   def position (s : Finset Γ) (x : Γ) : ℕ := (s.filter (· < x)).card

2. lemma OAI.SeparableQuotient.PathCoding.position_strictMonoOn line 16
3. lemma OAI.SeparableQuotient.PathCoding.position_inj line 29
4. lemma OAI.SeparableQuotient.PathCoding.position_align line 33
5. def OAI.SeparableQuotient.PathCoding.arrayCode line 52

   Source documentation

   A zero-filled rational array recorded by order positions, including zero values.

   def arrayCode (s : Finset Γ) (f : Γ →₀ ℚ) : Finset (ℕ × ℚ) :=
   …

6. lemma OAI.SeparableQuotient.PathCoding.arrayCode_match line 55
7. lemma OAI.SeparableQuotient.PathCoding.position_alignment line 64

   Source documentation

   Position alignment from equal compressed arrays and a shared initial segment.

   lemma position_alignment {s t : Finset Γ} {a : Γ} {f g : Γ →₀ ℚ}
       (hst : s.filter (· ≤ a) = t.filter (· ≤ a))
       (hf : f.support ⊆ s) (hg : g.support ⊆ t)
       (hfa : ∀ x ∈ f.support, x < a)
       (hcode : arrayCode s f = arrayCode t g) : f = g := by
   …

   Mentions: OAI.SeparableQuotient.PathCoding.arrayCode

8. lemma OAI.SeparableQuotient.PathCoding.closure_position_alignment line 95
9. abbrev OAI.SeparableQuotient.PathCoding.Code line 109
10. def OAI.SeparableQuotient.PathCoding.codeBound line 111
11. lemma OAI.SeparableQuotient.PathCoding.metadata_le_codeBound line 115
12. def OAI.SeparableQuotient.PathCoding.sigma line 126

    Source documentation

    An injective code greater than every entry of its final metadata.

    noncomputable def sigma (c : Code) : ℕ := Nat.pair (Encodable.encode c) (codeBound c + 1)

    Mentions: OAI.SeparableQuotient.PathCoding.Code, OAI.SeparableQuotient.PathCoding.codeBound

13. lemma OAI.SeparableQuotient.PathCoding.sigma_injective line 128
14. lemma OAI.SeparableQuotient.PathCoding.codeBound_lt_sigma line 132
15. structure OAI.SeparableQuotient.PathCoding.RawPath line 139

    Source documentation

    Raw infinite path data, retaining the actual rational pieces, declared weights and metadata. Nonzero pieces are included here to define the prefix endpoint without arbitrary defaults. Type-I membership is not needed for the combinatorial rigidity theorem.

    @[ext] structure RawPath where
    …

16. def OAI.SeparableQuotient.PathCoding.RawPath.support line 147
17. lemma OAI.SeparableQuotient.PathCoding.RawPath.mem_support_iff line 150
18. lemma OAI.SeparableQuotient.PathCoding.RawPath.piece_support_subset line 155
19. lemma OAI.SeparableQuotient.PathCoding.RawPath.support_nonempty line 160
20. def OAI.SeparableQuotient.PathCoding.RawPath.endpoint line 164
21. lemma OAI.SeparableQuotient.PathCoding.RawPath.endpoint_mem line 167
22. lemma OAI.SeparableQuotient.PathCoding.RawPath.le_endpoint line 170
23. def OAI.SeparableQuotient.PathCoding.RawPath.closure line 173
24. def OAI.SeparableQuotient.PathCoding.RawPath.code line 176
25. lemma OAI.SeparableQuotient.PathCoding.RawPath.code_length line 180
26. lemma OAI.SeparableQuotient.PathCoding.RawPath.code_eq_length line 183
27. lemma OAI.SeparableQuotient.PathCoding.RawPath.code_eq_at line 187
28. lemma OAI.SeparableQuotient.PathCoding.RawPath.metadata_le_codeBound line 195
29. structure OAI.SeparableQuotient.PathCoding.RawPath.Admissible line 202

    Source documentation

    Exact support, succession, weight and metadata conditions of a path. The Type-I construction contributes only additional restrictions, not needed below.

    structure Admissible (P : RawPath) : Prop where
    …

    Mentions: OAI.SeparableQuotient.PathCoding.RawPath

30. lemma OAI.SeparableQuotient.PathCoding.RawPath.Admissible.support_subset_closure line 213
31. lemma OAI.SeparableQuotient.PathCoding.RawPath.Admissible.piece_support_subset_closure line 219
32. lemma OAI.SeparableQuotient.PathCoding.RawPath.Admissible.weight_strict line 223
33. lemma OAI.SeparableQuotient.PathCoding.RawPath.Admissible.large_matching_prefix line 237
34. def OAI.SeparableQuotient.PathCoding.RawPath.SupportBelow line 257

    Source documentation

    The support of P is order-cofinal below that of Q.

    def SupportBelow (P Q : RawPath) : Prop :=
    …

    Mentions: OAI.SeparableQuotient.PathCoding.RawPath

35. lemma OAI.SeparableQuotient.PathCoding.RawPath.supportBelow_total line 261
36. lemma OAI.SeparableQuotient.PathCoding.RawPath.Admissible.eq_of_infinite_shared_weights_of_supportBelow line 271
37. lemma OAI.SeparableQuotient.PathCoding.RawPath.Admissible.eq_of_infinite_shared_weights line 309

    Source documentation

    Distinct admissible paths have only finitely many shared weights.

    lemma Admissible.eq_of_infinite_shared_weights {P Q : RawPath}
        (hP : P.Admissible) (hQ : Q.Admissible)
        (hinf : (Set.range P.weight ∩ Set.range Q.weight).Infinite) : P = Q := by
    …

    Mentions: OAI.SeparableQuotient.PathCoding.RawPath

38. lemma OAI.SeparableQuotient.PathCoding.RawPath.Admissible.shared_weights_finite line 317
39. lemma OAI.SeparableQuotient.PathCoding.RawPath.Admissible.disjoint_weight_tails line 330

    Source documentation

    A common finite deletion makes the weights of a finite collection of pairwise distinct paths disjoint. This is the combinatorial input to the Type-II tail estimate and the quotient-space path map.

    lemma Admissible.disjoint_weight_tails {ι : Type*} [Fintype ι] (P : ι → RawPath)
        (hP : ∀ i, (P i).Admissible) (hinj : Function.Injective P) :
        ∃ N : ℕ, Pairwise (fun i j => Disjoint
          (Set.range (fun n => (P i).weight (n+N)))
          (Set.range (fun n => (P j).weight (n+N)))) := by
    …

    Mentions: OAI.SeparableQuotient.PathCoding.RawPath, OAI.SeparableQuotient.PathCoding.RawPath.Admissible