OAI/Dynamics/SmoothObstruction/WordEntropy.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SmoothObstruction.WordFlatten.test_flatten line 12
2. lemma OAI.SmoothObstruction.WordFlatten.count_grouped line 22
3. theorem OAI.SmoothObstruction.WordFlatten.flat_sublist line 38

   Source documentation

   W3 itself: the actual single conditioned law controls every arbitrary partial list, with a single factor two, including lists crossing groups.

   theorem flat_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*H) → Option {v : V // v ≠ 0}) :
       expect (flatLaw B hd E hE) (test m) ≤
         2 * ((2 : ℝ)^(2*K) / Fintype.card {v : V // v ≠ 0}) ^
           (univ.filter (fun r => (m r).isSome)).card := by
   …

   Mentions: OAI.SmoothObstruction.WordFlatten.flatLaw

4. def OAI.SmoothObstruction.FiniteLaw.uniform line 60
5. def OAI.SmoothObstruction.FiniteLaw.mixture line 65
6. def OAI.SmoothObstruction.FiniteLaw.TV line 72
7. def OAI.SmoothObstruction.FiniteLaw.entropy line 73
8. lemma OAI.SmoothObstruction.FiniteLaw.TV_nonneg line 75
9. lemma OAI.SmoothObstruction.FiniteLaw.TV_symm line 76
10. lemma OAI.SmoothObstruction.FiniteLaw.TV_triangle line 77
11. lemma OAI.SmoothObstruction.FiniteLaw.push_sub line 82
12. lemma OAI.SmoothObstruction.FiniteLaw.TV_push line 90
13. lemma OAI.SmoothObstruction.FiniteLaw.entropy_nonneg line 101
14. lemma OAI.SmoothObstruction.FiniteLaw.entropy_mixture line 102
15. lemma OAI.SmoothObstruction.FiniteLaw.entropy_atom_lower line 106
16. lemma OAI.SmoothObstruction.FiniteLaw.entropy_tv_lower line 119

    Source documentation

    Exactly the one-bit TV cost used in source equation (tv-entropy), expressed first in natural units.

    lemma entropy_tv_lower (P Q : Law α) {s : ℝ} (hs : TV P Q ≤ s) :
        entropy P-Real.log 2-s*Real.log (Fintype.card α) ≤ entropy Q := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.TV, OAI.SmoothObstruction.FiniteLaw.entropy

17. lemma OAI.SmoothObstruction.FiniteLaw.entropy_close_atom_lower line 133
18. theorem OAI.SmoothObstruction.FiniteLaw.entropy_good_mixture line 142

    Source documentation

    Mixtures over arbitrary parent laws retain each admissible-slot bound; only the total exceptional-slot mass is lost.

    theorem entropy_good_mixture (P : Law α) (Q : α → Law β) (E : Finset α)
        {L : ℝ} (h : ∀ a ∈ E,L ≤ entropy (Q a)) :
        (∑ a ∈ E,P.mass a)*L ≤ entropy (mixture P Q) := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.Law, OAI.SmoothObstruction.FiniteLaw.entropy, OAI.SmoothObstruction.FiniteLaw.mixture

19. def OAI.SmoothObstruction.SequentialLaw.embeddedMarks line 158
20. lemma OAI.SmoothObstruction.SequentialLaw.embeddedMarks_at line 162
21. lemma OAI.SmoothObstruction.SequentialLaw.embeddedMarks_some line 170
22. lemma OAI.SmoothObstruction.SequentialLaw.embeddedMarks_count line 182
23. lemma OAI.SmoothObstruction.SequentialLaw.embeddedMarks_test line 199
24. theorem OAI.SmoothObstruction.WordFlatten.flat_window_atom line 222

    Source documentation

    The pushed law of any distinct coordinate list has the exact W3 atom bound; the law is the recursively used single conditioned sampler.

    theorem flat_window_atom (hd : K+1 ≤ Module.finrank (ZMod 2) V) (hK : 1 ≤ K)
        (E : Finset (Fin b → Fin H → {v : V // v ≠ 0}))
        (hE : 1/2 ≤ prob (rawLaw B hd H b) E)
        (e : Fin q ↪ Fin (b*H)) (v : Fin q → {v : V // v ≠ 0}) :
        (push (flatLaw B hd E hE) (fun w => w ∘ e)).mass v ≤
          2*((2:ℝ)^(2*K)/Fintype.card {v : V // v ≠ 0})^q := by
    …

    Mentions: OAI.SmoothObstruction.WordFlatten.flatLaw

25. lemma OAI.SmoothObstruction.FiniteLaw.mass_ext line 238
26. lemma OAI.SmoothObstruction.FiniteLaw.push_comp line 241
27. lemma OAI.SmoothObstruction.FiniteLaw.push_uniform_mass line 259
28. lemma OAI.SmoothObstruction.FiniteLaw.uniform_reindex line 263
29. lemma OAI.SmoothObstruction.FiniteLaw.push_observable line 271
30. lemma OAI.SmoothObstruction.FiniteLaw.TV_empirical line 276
31. lemma OAI.SmoothObstruction.FiniteLaw.TV_grouped line 282
32. lemma OAI.SmoothObstruction.FiniteLaw.atom_entropy_formula line 303
33. lemma OAI.SmoothObstruction.FiniteLaw.window_entropy_close line 313
34. instance OAI.SmoothObstruction.WordHierarchy.levelNonempty line 326
35. instance OAI.SmoothObstruction.WordHierarchy.groupNeZero line 327
36. instance OAI.SmoothObstruction.WordHierarchy.familyNeZero line 329
37. def OAI.SmoothObstruction.WordHierarchy.conditionedLabels line 331
38. def OAI.SmoothObstruction.WordHierarchy.conditionedWindow line 333
39. def OAI.SmoothObstruction.WordHierarchy.uniformWindow line 335
40. def OAI.SmoothObstruction.WordHierarchy.parentWindow line 337
41. lemma OAI.SmoothObstruction.WordHierarchy.uniformWindow_close line 342

    Source documentation

    W3 for the actual uniform selected family, in the finite-law API.

    lemma uniformWindow_close (i : ℕ) (t : Offsets (S i)) :
        TV (uniformWindow i t) (conditionedWindow i t) ≤ 1/10000 := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.uniformWindow, OAI.SmoothObstruction.WordHierarchy.conditionedWindow

42. lemma OAI.SmoothObstruction.WordHierarchy.parentWindow_close line 353

    Source documentation

    W4 for each actual parent: uniformity is only over its slots, never an assumption on the parent-word distribution.

    lemma parentWindow_close (i : ℕ) (a : A (i+2)) (t : Offsets (S i)) :
        TV (parentWindow i a t) (uniformWindow i t) ≤ 1/10000 := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.A, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.parentWindow, OAI.SmoothObstruction.WordHierarchy.uniformWindow

43. lemma OAI.SmoothObstruction.WordHierarchy.parent_conditioned_close line 367

    Source documentation

    The two and only two approximation costs used in the manuscript.

    lemma parent_conditioned_close (i : ℕ) (a : A (i+2)) (t : Offsets (S i)) :
        TV (conditionedWindow i t) (parentWindow i a t) ≤ 2/10000 := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.A, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.conditionedWindow, OAI.SmoothObstruction.WordHierarchy.parentWindow

44. def OAI.SmoothObstruction.WordHierarchy.windowEmbedding line 375
45. def OAI.SmoothObstruction.WordHierarchy.takePrefix line 379
46. lemma OAI.SmoothObstruction.WordHierarchy.conditioned_prefix_atom line 382
47. theorem OAI.SmoothObstruction.WordHierarchy.parent_prefix_entropy line 393

    Source documentation

    A real entropy lower bound for EVERY selected parent and admissible internal offset, with fully constructed comparison law and all atom bounds.

    theorem parent_prefix_entropy (i : ℕ) (a : A (i+2)) (t : Offsets (S i))
        {r : ℕ} (hr : r ≤ D (S i)) :
        (r:ℝ)*((1-2/10000)*Real.log (Fintype.card (A i))-(2*K (S i):ℕ)*Real.log 2)-2*Real.log 2 ≤
          entropy (push (parentWindow i a t) (takePrefix hr)) := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.A, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.parentWindow, OAI.SmoothObstruction.WordHierarchy.takePrefix

48. lemma OAI.SmoothObstruction.FiniteLaw.observed_ext line 409
49. def OAI.SmoothObstruction.FiniteLaw.observed line 412
50. lemma OAI.SmoothObstruction.FiniteLaw.observed_push line 420
51. def OAI.SmoothObstruction.FiniteLaw.conditionalObserved line 444
52. lemma OAI.SmoothObstruction.FiniteLaw.conditionalObserved_mass line 457
53. theorem OAI.SmoothObstruction.FiniteLaw.observed_mixture line 475

    Source documentation

    Disintegration over a finite actual observation. Zero conditional masses are represented by a harmless uniform law and contribute exactly zero.

    theorem observed_mixture (μ : Measure X) [IsProbabilityMeasure μ]
        (f : X → α) (hf : Measurable f) (k : X → β) (hk : Measurable k)
        [Nonempty α] :
        observed μ f hf=mixture (observed μ k hk) (conditionalObserved μ f hf k hk) := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.observed, OAI.SmoothObstruction.FiniteLaw.mixture, OAI.SmoothObstruction.FiniteLaw.conditionalObserved

54. instance OAI.SmoothObstruction.WordHierarchy.stageLengthNeZero line 491
55. lemma OAI.SmoothObstruction.WordHierarchy.measurable_slot line 493
56. lemma OAI.SmoothObstruction.WordHierarchy.pack_slots line 501
57. lemma OAI.SmoothObstruction.WordHierarchy.slots_iff line 506
58. lemma OAI.SmoothObstruction.WordHierarchy.boundary_phase_zero line 510
59. lemma OAI.SmoothObstruction.WordHierarchy.boundary_slots_mass line 514
60. def OAI.SmoothObstruction.WordHierarchy.windowKey line 528
61. lemma OAI.SmoothObstruction.WordHierarchy.measurable_windowKey line 531
62. lemma OAI.SmoothObstruction.WordHierarchy.boundary_key_mass line 534
63. def OAI.SmoothObstruction.WordHierarchy.sampledWindow line 555

    Source documentation

    The actual r-child window at an internal offset of a specified parent.

    noncomputable def sampledWindow (i r : ℕ) (u : Fin (N (S i)))
        (hr : u.val+r ≤ N (S i)) (v : A (i+2)) (h : Fin (N (S (i+1)))) : Fin r → A i :=
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.A

64. def OAI.SmoothObstruction.WordHierarchy.sampledLaw line 559
65. lemma OAI.SmoothObstruction.WordHierarchy.labelList_key line 563
66. theorem OAI.SmoothObstruction.WordHierarchy.boundary_window_joint line 575

    Source documentation

    Exact disintegration at an admissible offset. Stationarity gives slot uniformity even when the parent marginal has zero or varying masses.

    theorem boundary_window_joint (μ : Measure Extension) [IsProbabilityMeasure μ]
        (hT : MeasurePreserving T μ μ) (i r : ℕ) (u : Fin (N (S i)))
        (hr : u.val+r ≤ N (S i)) (v : A (i+2)) (w : Fin r → A i) :
        (boundary μ i).real {x | windowKey i x=(v,u) ∧ labelList i r x=w} =
          (boundary μ i).real {x | windowKey i x=(v,u)}*(sampledLaw i r u hr v).mass w := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.A, OAI.SmoothObstruction.WordHierarchy.boundary, OAI.SmoothObstruction.WordHierarchy.windowKey, OAI.SmoothObstruction.WordHierarchy.labelList, OAI.SmoothObstruction.WordHierarchy.sampledLaw

67. lemma OAI.SmoothObstruction.WordHierarchy.conditional_window_eq line 616

    Source documentation

    The conditional law is the actual finite-parent sampled window law on all positive-probability fibres. No hypothesis about parent frequencies.

    lemma conditional_window_eq (μ : Measure Extension) [IsProbabilityMeasure μ]
        (hT : MeasurePreserving T μ μ) (i r : ℕ) (u : Fin (N (S i)))
        (hr : u.val+r ≤ N (S i)) (v : A (i+2))
        (hp : (boundary μ i).real {x | windowKey i x=(v,u)}≠0) :
        let : IsProbabilityMeasure (boundary μ i) := boundary_isProbability μ hT i
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.A, OAI.SmoothObstruction.WordHierarchy.boundary, OAI.SmoothObstruction.WordHierarchy.windowKey, OAI.SmoothObstruction.WordHierarchy.boundary_isProbability

68. lemma OAI.SmoothObstruction.WordHierarchy.sampledLaw_prefix line 636
69. def OAI.SmoothObstruction.WordHierarchy.windowLower line 656
70. lemma OAI.SmoothObstruction.WordHierarchy.sampled_entropy line 659
71. theorem OAI.SmoothObstruction.WordHierarchy.boundary_window_entropy line 671

    Source documentation

    The entropy of the genuine stationary aligned orbit window is bounded using the exactly uniform internal-slot law, not a selected parent law.

    theorem boundary_window_entropy (μ : Measure Extension) [IsProbabilityMeasure μ]
        (hT : MeasurePreserving T μ μ) (i r : ℕ) (hr : r ≤ D (S i)) :
        let : IsProbabilityMeasure (boundary μ i) := boundary_isProbability μ hT i
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.boundary, OAI.SmoothObstruction.WordHierarchy.boundary_isProbability

72. lemma OAI.SmoothObstruction.WordHierarchy.D_pos line 702
73. lemma OAI.SmoothObstruction.WordHierarchy.good_offset_count line 704
74. lemma OAI.SmoothObstruction.WordHierarchy.good_key_mass line 715
75. theorem OAI.SmoothObstruction.WordHierarchy.stationary_window_entropy line 741

    Source documentation

    The manuscript's explicit stationary entropy lower bound, with the exact loss from inadmissible offsets and an arbitrary invariant probability.

    theorem stationary_window_entropy (μ : Measure Extension) [IsProbabilityMeasure μ]
        (hT : MeasurePreserving T μ μ) (i r : ℕ) (hr : r ≤ D (S i)) :
        let : IsProbabilityMeasure (boundary μ i) := boundary_isProbability μ hT i
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.boundary, OAI.SmoothObstruction.WordHierarchy.boundary_isProbability

76. lemma OAI.SmoothObstruction.WordHierarchy.log_card line 757
77. lemma OAI.SmoothObstruction.WordHierarchy.K_large line 763
78. lemma OAI.SmoothObstruction.WordHierarchy.bad_offset_small line 772
79. lemma OAI.SmoothObstruction.WordHierarchy.good_offset_large line 786
80. lemma OAI.SmoothObstruction.WordHierarchy.windowLower_large line 796
81. theorem OAI.SmoothObstruction.WordHierarchy.stationary_window_entropy_996 line 818

    Source documentation

    Uniform stationary window entropy, with the manuscript's decimal constant. It is valid already at level one beyond the fixed initial level, independently of the stationary probability and independently of the window length. Entropy here uses natural logarithms, so both sides have the same conversion factor.

    theorem stationary_window_entropy_996 (μ : Measure Extension) [IsProbabilityMeasure μ]
        (hT : MeasurePreserving T μ μ) {i r : ℕ} (hi : 1 ≤ i)
        (hr : 1 ≤ r) (hrD : r ≤ D (S i)) :
        let : IsProbabilityMeasure (boundary μ i) := boundary_isProbability μ hT i
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.boundary, OAI.SmoothObstruction.WordHierarchy.boundary_isProbability

82. lemma OAI.SmoothObstruction.WordHierarchy.graph_block_room line 845
83. lemma OAI.SmoothObstruction.WordHierarchy.group_site_lt line 853
84. lemma OAI.SmoothObstruction.WordHierarchy.children_graph line 864
85. def OAI.SmoothObstruction.WordHierarchy.graphWindows line 910

    Source documentation

    The genuine two-window graph event on a boundary-started orbit.

    def graphWindows (i k : ℕ) (x : Extension) : Prop :=
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension

86. lemma OAI.SmoothObstruction.WordHierarchy.graphWindows_of_good line 915
87. lemma OAI.SmoothObstruction.WordHierarchy.boundary_slot_mass line 940
88. lemma OAI.SmoothObstruction.WordHierarchy.residue_sum line 955
89. lemma OAI.SmoothObstruction.WordHierarchy.boundary_residue_mass line 975
90. theorem OAI.SmoothObstruction.WordHierarchy.boundary_graph_probability line 1004

    Source documentation

    The two lists of the actual system pass all graph tests simultaneously except for the precise group-boundary fraction (2D-2)/H.

    theorem boundary_graph_probability (μ : Measure Extension) [IsProbabilityMeasure μ]
        (hT : MeasurePreserving T μ μ) (i k : ℕ) (hk : k ≤ K (S i)/8) :
        1-((2*2^k-2:ℕ):ℝ)/H (S i) ≤
          (boundary μ i).real {x | graphWindows i k x} := by
    …

    Mentions: OAI.SmoothObstruction.WordHierarchy.Extension, OAI.SmoothObstruction.WordHierarchy.T, OAI.SmoothObstruction.WordHierarchy.S, OAI.SmoothObstruction.WordHierarchy.boundary, OAI.SmoothObstruction.WordHierarchy.graphWindows

91. theorem OAI.SmoothObstruction.FiniteLaw.observed_integral line 1051

    Source documentation

    Every finite observable's real expectation agrees with integration in its original probability space. No conditional normalization occurs.

    theorem observed_integral (μ : Measure X) [IsProbabilityMeasure μ]
        (f : X → α) (hf : Measurable f) (g : α → ℝ) :
        (∑ a,(observed μ f hf).mass a*g a)=∫ x,g (f x) ∂μ := by
    …

    Mentions: OAI.SmoothObstruction.FiniteLaw.observed

92. theorem OAI.SmoothObstruction.FiniteLaw.integral_lower_of_event line 1066

    Source documentation

    A lower bound on a success event is a lower bound in the UNCONDITIONED law. In particular .95 mass at statistic .96 gives expectation .912.

    theorem integral_lower_of_event (μ : Measure X) [IsProbabilityMeasure μ]
        (Z : X → ℝ) (hZi : Integrable Z μ) (hZn : ∀ x,0≤Z x)
        (G : Set X) (hG : MeasurableSet G) (a b : ℝ) (ha : 0≤a)
        (hGm : b≤μ.real G) (hZG : ∀ x∈G,a≤Z x) :
        a*b≤∫ x,Z x ∂μ := by
    …