OAI/Dynamics/SmoothObstruction/WordLaw.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SmoothObstruction.WordLaw.lagBack line 15

   Source documentation

   The literal dyadic predecessor schedule of W1, padded by absent equations up to K slots. Groups restart this schedule at zero.

   def lagBack (K t : ℕ) (j : Fin K) : Option (Fin t) :=
   …

2. lemma OAI.SmoothObstruction.WordLaw.lagBack_eq line 20
3. def OAI.SmoothObstruction.WordLaw.groupLaw line 29
4. def OAI.SmoothObstruction.WordLaw.rawLaw line 35
5. lemma OAI.SmoothObstruction.WordLaw.group_relations line 39
6. lemma OAI.SmoothObstruction.WordLaw.raw_relations line 50
7. lemma OAI.SmoothObstruction.WordLaw.group_label line 63
8. def OAI.SmoothObstruction.WordLaw.empirical line 73

   Source documentation

   Empirical probability vector formed from a single group.

   noncomputable def empirical (f : {v : V // v ≠ 0} → C)
       (w : Fin H → {v : V // v ≠ 0}) (c : C) : ℝ :=
   …

9. lemma OAI.SmoothObstruction.WordLaw.empirical_nonneg line 78
10. lemma OAI.SmoothObstruction.WordLaw.empirical_total line 84
11. lemma OAI.SmoothObstruction.WordLaw.group_observable line 91
12. lemma OAI.SmoothObstruction.WordLaw.group_mean line 108
13. theorem OAI.SmoothObstruction.WordLaw.raw_empirical_tv line 121

    Source documentation

    The first source use of the probability-vector estimate: it averages groups, not falsely independent positions within a group.

    theorem raw_empirical_tv (hB : B.IsAlt) (hnd : B.Nondegenerate)
        (hd : K + 1 ≤ Module.finrank (ZMod 2) V) (hH : 0 < H) (hq : 0 < q)
        (f : {v : V // v ≠ 0} → C) :
        expect (rawLaw B hd H q) (fun w => (1 / 2 : ℝ) * ∑ c,
          |(∑ b, empirical f (w b) c) / q -
            (∑ a : {v : V // v ≠ 0}, if f a = c then (1 : ℝ) else 0) /
              Fintype.card {v : V // v ≠ 0}|) ≤
          (1 / 2 : ℝ) * Real.sqrt (Fintype.card C / q) := by
    …

    Mentions: OAI.SmoothObstruction.WordLaw.rawLaw, OAI.SmoothObstruction.WordLaw.empirical

14. theorem OAI.SmoothObstruction.WordLaw.raw_sublist_groups line 138

    Source documentation

    A specified arbitrary sublist, across any number of groups. The exponent is the exact number of specified coordinates, not the size of its span.

    theorem raw_sublist_groups (hd : K + 1 ≤ Module.finrank (ZMod 2) V) (hK : 1 ≤ K)
        (m : Fin q → Fin H → Option {v : V // v ≠ 0}) :
        FiniteLaw.expect (rawLaw B hd H q) (fun w => ∏ b, test (m b) (w b)) ≤
          ((2 : ℝ) ^ (2 * K) / Fintype.card {v : V // v ≠ 0}) ^
            (∑ b, (univ.filter (fun r => (m b r).isSome)).card) := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.expect, OAI.SmoothObstruction.WordLaw.rawLaw

15. theorem OAI.SmoothObstruction.WordLaw.conditioned_sublist line 154

    Source documentation

    All actual conditioned laws pay the factor two once for the whole word.

    theorem conditioned_sublist (hd : K + 1 ≤ Module.finrank (ZMod 2) V) (hK : 1 ≤ K)
        (E : Finset (Fin q → Fin H → {v : V // v ≠ 0}))
        (hE : 1 / 2 ≤ prob (rawLaw B hd H q) E)
        (m : Fin q → Fin H → Option {v : V // v ≠ 0}) :
        FiniteLaw.expect (condition (rawLaw B hd H q) E (by change 0 < prob _ E; linarith))
          (fun w => ∏ b, test (m b) (w b)) ≤
          2 * ((2 : ℝ) ^ (2 * K) / Fintype.card {v : V // v ≠ 0}) ^
            (∑ b, (univ.filter (fun r => (m b r).isSome)).card) := by
    …

    Mentions: OAI.SmoothObstruction.WordLaw.rawLaw, OAI.SmoothObstruction.FiniteLaw.expect

16. def OAI.SmoothObstruction.WordLaw.tvFromUniformObservable line 166
17. theorem OAI.SmoothObstruction.WordLaw.approximation_event line 174

    Source documentation

    A concrete, nonempty conditioning event enforcing the per-word condition simultaneously for all the earlier-level windows.

    theorem approximation_event {I : Type*} [Fintype I]
        (hB : B.IsAlt) (hnd : B.Nondegenerate)
        (hd : K + 1 ≤ Module.finrank (ZMod 2) V) (hH : 0 < H) (hq : 0 < q)
        (f : I → {v : V // v ≠ 0} → C) {θ : ℝ} (hθ : 0 < θ)
        (hbudget : (Fintype.card I : ℝ) *
          ((1 / 2 : ℝ) * Real.sqrt (Fintype.card C / q)) / θ ≤ 1 / 2) :
        1 / 2 ≤ prob (rawLaw B hd H q)
          (univ.filter (fun w => ∀ i, tvFromUniformObservable (f i) w ≤ θ)) := by
    …

    Mentions: OAI.SmoothObstruction.WordLaw.rawLaw, OAI.SmoothObstruction.WordLaw.tvFromUniformObservable

18. lemma OAI.SmoothObstruction.FiniteLaw.product_injective_moment line 197
19. lemma OAI.SmoothObstruction.FiniteLaw.product_restriction line 222
20. lemma OAI.SmoothObstruction.FiniteLaw.product_restriction_expect line 237
21. lemma OAI.SmoothObstruction.FiniteLaw.prob_card_bound line 251
22. lemma OAI.SmoothObstruction.FiniteLaw.product_mass_upper line 258
23. lemma OAI.SmoothObstruction.MatchingCount.increasing_count line 273

    Source documentation

    Equalities oriented to a distinct later variable determine the removed coordinates uniquely from those left free. This is the acyclic comparison count, without an assumption of independence between equality events.

    lemma increasing_count {n : ℕ} (f g : I → Fin n)
        (hfg : ∀ i, f i < g i) (hg : Function.Injective g) :
        Nat.card {w : Fin n → A // ∀ i, w (f i) = w (g i)} ≤
          Fintype.card A ^ (n - Fintype.card I) := by
    …

24. theorem OAI.SmoothObstruction.MatchingCount.matching_count line 310

    Source documentation

    For a comparison with two injective endpoint lists and no tautological loops, at least half the equality constraints can be oriented to distinct later variables. This includes parallel edges and all repeated-word cases.

    theorem matching_count {n : ℕ} (f g : I → Fin n)
        (hf : Function.Injective f) (hg : Function.Injective g) (hne : ∀ i, f i ≠ g i) :
        Nat.card {w : Fin n → A // ∀ i, w (f i) = w (g i)} ≤
          Fintype.card A ^ (n - (Fintype.card I + 1) / 2) := by
    …

25. theorem OAI.SmoothObstruction.MatchingCount.matching_count_finite line 362

    Source documentation

    The comparison count in an arbitrary finite ambient coordinate set, including several complete sampled words and repeated sample-list indices.

    theorem matching_count_finite (f g : I → W)
        (hf : Function.Injective f) (hg : Function.Injective g) (hne : ∀ i, f i ≠ g i) :
        Nat.card {w : W → A // ∀ i, w (f i) = w (g i)} ≤
          Fintype.card A ^ (Fintype.card W - (Fintype.card I + 1) / 2) := by
    …

26. theorem OAI.SmoothObstruction.MatchingCount.comparison_probability line 380

    Source documentation

    Cardinality to probability: the reference comparison estimate, valid for any nonnegative finite law with a pointwise full-list bound.

    theorem comparison_probability [DecidableEq W] [DecidableEq A]
        (P : FiniteLaw.Law (W → A)) {c : ℝ} (hc0 : 0 ≤ c) (hc : ∀ w, P.mass w ≤ c)
        (f g : I → W) (hf : Function.Injective f) (hg : Function.Injective g)
        (hne : ∀ i, f i ≠ g i) :
        FiniteLaw.prob P (univ.filter (fun w => ∀ i, w (f i) = w (g i))) ≤
          (Fintype.card A : ℝ) ^ (Fintype.card W - (Fintype.card I + 1) / 2) * c := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.prob

27. lemma OAI.SmoothObstruction.FiniteLaw.prob_mono line 400
28. lemma OAI.SmoothObstruction.FiniteLaw.sampled_matching_probability line 408

    Source documentation

    Actual independent complete-list sampling, with arbitrary repeated uses of list indices in the comparison endpoints. The index injection counts each independently sampled word once and all unused sampled words are integrated.

    lemma sampled_matching_probability (P : I → Law (R → A)) (e : J → I)
        (he : Function.Injective e) (f g : R → J × R)
        (hf : Function.Injective f) (hg : Function.Injective g) (hne : ∀ r, f r ≠ g r)
        (s : Finset R) {c : ℝ} (hc : 0 ≤ c) (hP : ∀ j w, (P (e j)).mass w ≤ c) :
        prob (product P) (univ.filter (fun x => ∀ r ∈ s,
          x (e (f r).1) (f r).2 = x (e (g r).1) (g r).2)) ≤
          (Fintype.card A : ℝ) ^ (Fintype.card J * Fintype.card R - (s.card + 1) / 2) *
            c ^ Fintype.card J := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.prob, OAI.SmoothObstruction.FiniteLaw.product

29. lemma OAI.SmoothObstruction.FiniteLaw.sampled_bad_comparison line 449

    Source documentation

    Union over specified matching-position sets. No label independence inside a sampled word is assumed.

    lemma sampled_bad_comparison (P : I → Law (R → A)) (e : J → I)
        (he : Function.Injective e) (f g : R → J × R)
        (hf : Function.Injective f) (hg : Function.Injective g) (hne : ∀ r, f r ≠ g r)
        (a : ℕ) {c : ℝ} (hc : 0 ≤ c) (hP : ∀ j w, (P (e j)).mass w ≤ c) :
        prob (product P) (univ.filter (fun x => a ≤ (univ.filter (fun r =>
          x (e (f r).1) (f r).2 = x (e (g r).1) (g r).2)).card)) ≤
          (2 : ℝ) ^ Fintype.card R *
            (Fintype.card A : ℝ) ^ (Fintype.card J * Fintype.card R - (a + 1) / 2) *
            c ^ Fintype.card J := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.prob, OAI.SmoothObstruction.FiniteLaw.product

30. lemma OAI.SmoothObstruction.FiniteLaw.comparison_cost line 502

    Source documentation

    Exact simplification of the sampled comparison cost. The one-time conditioning doubles each of at most three word laws, costing eight, not a factor per selected label.

    lemma comparison_cost {L U : ℝ} (hL : 1 ≤ L) (hU : 1 ≤ U)
        {N j a : ℕ} (hj : 1 ≤ j) (hj' : j ≤ 3) (ha : a ≤ N) :
        (2 : ℝ) ^ N * L ^ (j * N - (a + 1) / 2) *
          (2 * (U / L) ^ N) ^ j ≤
          8 * 2 ^ N * U ^ (3 * N) * L ^ (-(a : ℝ) / 2) := by
    …