OAI/Dynamics/SmoothObstruction/Sampling.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SmoothObstruction.SymplecticSampling.bit_cases line 11
2. lemma OAI.SmoothObstruction.SymplecticSampling.bit_one line 15
3. lemma OAI.SmoothObstruction.SymplecticSampling.bit_neg line 17
4. lemma OAI.SmoothObstruction.SymplecticSampling.add_self line 22
5. lemma OAI.SmoothObstruction.SymplecticSampling.alt_symm line 25
6. lemma OAI.SmoothObstruction.SymplecticSampling.transvection_preserves line 29
7. lemma OAI.SmoothObstruction.SymplecticSampling.transvection_moves line 40
8. lemma OAI.SmoothObstruction.SymplecticSampling.exists_pairing_one line 46
9. lemma OAI.SmoothObstruction.SymplecticSampling.common_pairing_one line 52
10. theorem OAI.SmoothObstruction.SymplecticSampling.symplectic_transitive line 66

    Source documentation

    Explicit symplectic transitivity in characteristic two, using at most two transvections. This proves the uniform one-label marginal input to the actual sequential word sampling, without assuming a symplectic-basis theorem.

    theorem symplectic_transitive {B : LinearMap.BilinForm (ZMod 2) V}
        (hB : B.IsAlt) (hnd : B.Nondegenerate) {v w : V} (hv : v ≠ 0) (hw : w ≠ 0) :
        ∃ e : V ≃ₗ[ZMod 2] V, e v = w ∧ ∀ x y, B (e x) (e y) = B x y := by
    …

11. def OAI.SmoothObstruction.SymplecticSampling.nonzeroKerEquiv line 85
12. lemma OAI.SmoothObstruction.SymplecticSampling.card_nonzero_ker line 98
13. theorem OAI.SmoothObstruction.SymplecticSampling.common_kernel_lower line 106

    Source documentation

    At most k linear equations remove at most k binary dimensions, even when they are dependent. The zero vector is then removed exactly once.

    theorem common_kernel_lower {k : ℕ} (f : V →ₗ[ZMod 2] (Fin k → ZMod 2)) :
        2 ^ (Module.finrank (ZMod 2) V - k) ≤
          Fintype.card {v : V // v ≠ 0 ∧ f v = 0} + 1 := by
    …

14. theorem OAI.SmoothObstruction.SymplecticSampling.common_kernel_choices line 120

    Source documentation

    The quantitative bound actually used in source (word-choices), with the original nonzero alphabet and dependent equations allowed.

    theorem common_kernel_choices {k : ℕ} (f : V →ₗ[ZMod 2] (Fin k → ZMod 2))
        (hk : 1 ≤ k) (hd : k + 1 ≤ Module.finrank (ZMod 2) V) :
        Fintype.card {v : V // v ≠ 0} ≤
          2 ^ (2 * k) * Fintype.card {v : V // v ≠ 0 ∧ f v = 0} := by
    …

15. def OAI.SmoothObstruction.SymplecticSampling.allowed line 143

    Source documentation

    The exact nonzero choices, not an independent-equations approximation.

    noncomputable def allowed {k : ℕ} (u : Fin k → V) : Finset {v : V // v ≠ 0} :=
    …

16. def OAI.SmoothObstruction.SymplecticSampling.equationMap line 146
17. lemma OAI.SmoothObstruction.SymplecticSampling.mem_allowed line 149
18. lemma OAI.SmoothObstruction.SymplecticSampling.allowed_card line 154
19. lemma OAI.SmoothObstruction.SymplecticSampling.allowed_nonempty line 167
20. def OAI.SmoothObstruction.SymplecticSampling.kernel line 177

    Source documentation

    Uniform sampling among all allowed nonzero labels.

    noncomputable def kernel {k : ℕ} (u : Fin k → V) (v : {v : V // v ≠ 0}) : ℝ :=
    …

21. lemma OAI.SmoothObstruction.SymplecticSampling.kernel_nonneg line 180
22. lemma OAI.SmoothObstruction.SymplecticSampling.kernel_sum line 185
23. lemma OAI.SmoothObstruction.SymplecticSampling.kernel_upper line 193
24. def OAI.SmoothObstruction.SymplecticSampling.nonzeroEquiv line 213
25. lemma OAI.SmoothObstruction.SymplecticSampling.allowed_equivariant line 220
26. lemma OAI.SmoothObstruction.SymplecticSampling.allowed_card_equivariant line 225
27. lemma OAI.SmoothObstruction.SymplecticSampling.kernel_equivariant line 233
28. def OAI.SmoothObstruction.SequentialLaw.weight line 248

    Source documentation

    A finite left-to-right sampling law. The kernel at time k may depend on all k preceding labels; no independence inside a group is assumed.

    def weight (K : (k : ℕ) → (Fin k → A) → A → ℝ) : (n : ℕ) → (Fin n → A) → ℝ
      | 0, _ => 1
      | n + 1, w => weight K n (Fin.init w) * K n (Fin.init w) (w (Fin.last n))

29. lemma OAI.SmoothObstruction.SequentialLaw.weight_zero line 252
30. lemma OAI.SmoothObstruction.SequentialLaw.weight_snoc line 255
31. lemma OAI.SmoothObstruction.SequentialLaw.weight_nonneg line 260
32. lemma OAI.SmoothObstruction.SequentialLaw.snoc_equiv_apply line 268
33. lemma OAI.SmoothObstruction.SequentialLaw.sum_weight line 271
34. def OAI.SmoothObstruction.SequentialLaw.mark line 285
35. def OAI.SmoothObstruction.SequentialLaw.test line 290
36. lemma OAI.SmoothObstruction.SequentialLaw.mark_nonneg line 294
37. lemma OAI.SmoothObstruction.SequentialLaw.test_nonneg line 300
38. lemma OAI.SmoothObstruction.SequentialLaw.test_snoc line 304
39. lemma OAI.SmoothObstruction.SequentialLaw.sum_test_succ line 311
40. theorem OAI.SmoothObstruction.SequentialLaw.cylinder_bound line 329

    Source documentation

    Any list of specified coordinates has probability at most the product of the pointwise conditional upper bounds. Unspecified labels are integrated out, exactly as in (word-raw-sublist).

    theorem cylinder_bound {K : (k : ℕ) → (Fin k → A) → A → ℝ} {ζ : ℝ}
        (h0 : ∀ k w a, 0 ≤ K k w a) (h1 : ∀ k w, ∑ a, K k w a = 1)
        (hζ : 0 ≤ ζ) (hK : ∀ k w a, K k w a ≤ ζ) :
        ∀ n (m : Fin n → Option A), (∑ w, weight K n w * test m w) ≤
          ∏ i, (if (m i).isSome then ζ else 1) := by
    …

    Mentions: OAI.SmoothObstruction.SequentialLaw.weight, OAI.SmoothObstruction.SequentialLaw.test

41. lemma OAI.SmoothObstruction.SequentialLaw.weight_equivariant line 357
42. lemma OAI.SmoothObstruction.SequentialLaw.test_eq_indicator line 369
43. lemma OAI.SmoothObstruction.SequentialLaw.test_upper_pow line 377
44. def OAI.SmoothObstruction.SequentialLaw.marginal line 387

    Source documentation

    The unconditioned one-coordinate law; the complete path is summed out.

    def marginal (K : (k : ℕ) → (Fin k → A) → A → ℝ) {n : ℕ} (i : Fin n) (a : A) : ℝ :=
    …

45. lemma OAI.SmoothObstruction.SequentialLaw.sum_marginal line 390
46. lemma OAI.SmoothObstruction.SequentialLaw.marginal_equivariant line 398
47. theorem OAI.SmoothObstruction.SequentialLaw.uniform_marginal line 411

    Source documentation

    Equivariance under a transitive collection of label permutations gives exactly uniform marginals, despite arbitrary dependencies between positions.

    theorem uniform_marginal [Nonempty A]
        {K : (k : ℕ) → (Fin k → A) → A → ℝ}
        (h1 : ∀ k w, ∑ a, K k w a = 1)
        (htrans : ∀ a b : A, ∃ e : A ≃ A, e a = b ∧
          ∀ k w x, K k (e ∘ w) (e x) = K k w x)
        {n : ℕ} (i : Fin n) (a : A) : marginal K i a = 1 / Fintype.card A := by
    …

    Mentions: OAI.SmoothObstruction.SequentialLaw.marginal

48. def OAI.SmoothObstruction.GroupSampler.previous line 438

    Source documentation

    At time t, at most K earlier positions are constrained. None represents an absent constraint, whose equation is identically zero.

    def previous (back : (t : ℕ) → Fin K → Option (Fin t))
        (t : ℕ) (w : Fin t → {v : V // v ≠ 0}) (j : Fin K) : V :=
    …

49. def OAI.SmoothObstruction.GroupSampler.step line 442
50. lemma OAI.SmoothObstruction.GroupSampler.step_sum line 446
51. lemma OAI.SmoothObstruction.GroupSampler.previous_equivariant line 451
52. lemma OAI.SmoothObstruction.GroupSampler.step_equivariant line 457
53. theorem OAI.SmoothObstruction.GroupSampler.uniform_position line 466

    Source documentation

    The actual sequential sampling has exactly uniform one-position laws. This is not a product law inside a group.

    theorem uniform_position (hB : B.IsAlt) (hnd : B.Nondegenerate)
        (back : (t : ℕ) → Fin K → Option (Fin t))
        (hd : K + 1 ≤ Module.finrank (ZMod 2) V)
        {n : ℕ} (i : Fin n) (a : {v : V // v ≠ 0}) :
        marginal (step B back) i a = 1 / Fintype.card {v : V // v ≠ 0} := by
    …

    Mentions: OAI.SmoothObstruction.GroupSampler.step

54. theorem OAI.SmoothObstruction.GroupSampler.raw_sublist line 479

    Source documentation

    All sublist probabilities have the source bound, even though prior constraints can be linearly dependent and unobserved labels are integrated out.

    theorem raw_sublist (back : (t : ℕ) → Fin K → Option (Fin t))
        (hK : 1 ≤ K) (hd : K + 1 ≤ Module.finrank (ZMod 2) V)
        (n : ℕ) (m : Fin n → Option {v : V // v ≠ 0}) :
        (∑ w, weight (step B back) n w * test m w) ≤
          ((2 : ℝ) ^ (2 * K) / Fintype.card {v : V // v ≠ 0}) ^
            (univ.filter (fun i => (m i).isSome)).card := by
    …

    Mentions: OAI.SmoothObstruction.GroupSampler.step

55. lemma OAI.SmoothObstruction.GroupSampler.step_positive_constraint line 491
56. theorem OAI.SmoothObstruction.GroupSampler.supported_constraints line 502

    Source documentation

    Positively weighted paths satisfy every prescribed relation.

    theorem supported_constraints (back : (t : ℕ) → Fin K → Option (Fin t)) :
        ∀ n (w : Fin n → {v : V // v ≠ 0}), 0 < weight (step B back) n w →
          ∀ (t : Fin n) (j : Fin K) (r : Fin t.val), back t.val j = some r →
            B (w ⟨r.val, lt_trans r.isLt t.isLt⟩).val (w t).val = 0 := by
    …

    Mentions: OAI.SmoothObstruction.GroupSampler.step