OAI/Probability/CoordinateSweeps/Transition.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CoordinateSweeps.Grid.Holes.log_size line 16
2. theorem OAI.CoordinateSweeps.Grid.Holes.log_probability_zero line 22
3. theorem OAI.CoordinateSweeps.Grid.Holes.probability_zero_pos line 50
4. theorem OAI.CoordinateSweeps.Grid.Holes.probability_zero_eq_exp line 59
5. def OAI.CoordinateSweeps.Grid.Holes.Extends line 64

   Source comment

   Augmented holes retain the ordered first h trajectories exactly.

   def Extends {t : ℕ} (J : G.Holes (h+t)) (H : G.Holes h) : Prop :=
   …

6. def OAI.CoordinateSweeps.Grid.Holes.extraCount line 67
7. theorem OAI.CoordinateSweeps.Grid.Holes.lineCount_add line 70
8. theorem OAI.CoordinateSweeps.Grid.Holes.sum_extraCount line 83
9. theorem OAI.CoordinateSweeps.Grid.Holes.no_extra_iff line 100
10. theorem OAI.CoordinateSweeps.Grid.Holes.lineCompatible_eq_of_no_extra line 104
11. theorem OAI.CoordinateSweeps.FiniteLaw.assignments_pos_of_comparison line 136
12. theorem OAI.CoordinateSweeps.FiniteLaw.assignments_ratio_comparison line 142
13. def OAI.CoordinateSweeps.Grid.Holes.lineProb line 162
14. theorem OAI.CoordinateSweeps.Grid.Holes.lineProb_nonneg line 166
15. theorem OAI.CoordinateSweeps.Grid.Holes.uniform_lineProb_pos line 170
16. theorem OAI.CoordinateSweeps.Grid.Holes.lineProb_eq_of_no_extra line 173
17. def OAI.CoordinateSweeps.Grid.Holes.usedLine line 183
18. theorem OAI.CoordinateSweeps.Grid.Holes.sum_usedLine_le line 186
19. theorem OAI.CoordinateSweeps.Grid.Holes.lineProb_ratio_le line 198
20. theorem OAI.CoordinateSweeps.Grid.Holes.probability_prod_lineProb line 216
21. theorem OAI.CoordinateSweeps.Grid.Holes.probability_zero_prod_lineProb line 220
22. theorem OAI.CoordinateSweeps.Grid.Holes.probability_ratio_comparison line 233

    Source comment

    Only a line visited by a new path may spend the factor four. Thus the factor count is at most t*b, not the total number of stage-lines.

    theorem probability_ratio_comparison (J : G.Holes (h+t)) (H : G.Holes h)
        (he : J.Extends H) {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ 1)
        (hlo : ∀ j g, (1/2 : ℝ)*FiniteLaw.uniform _ g ≤ lineLaw (G.bits j) z hz hz' g)
        (hhi : ∀ j g, lineLaw (G.bits j) z hz hz' g ≤ 2*FiniteLaw.uniform _ g) :
        J.probability z / H.probability z ≤
          (4 : ℝ)^(t*G.b) * (J.probability 0 / H.probability 0) := by
    …

    Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform, OAI.CoordinateSweeps.lineLaw

23. theorem OAI.CoordinateSweeps.Grid.Holes.conditional_transition_bound line 267

    Source comment

    Source 03-paths (4), in the exactly equal exponential notation. The ratio is the conditional probability of the complete augmented paths.

    theorem conditional_transition_bound (J : G.Holes (h+t)) (H : G.Holes h)
        (he : J.Extends H) {z : ℝ} (hz : 0 ≤ z) (hz' : z ≤ 1)
        (hlo : ∀ j g, (1/2 : ℝ)*FiniteLaw.uniform _ g ≤ lineLaw (G.bits j) z hz hz' g)
        (hhi : ∀ j g, lineLaw (G.bits j) z hz hz' g ≤ 2*FiniteLaw.uniform _ g) :
        J.probability z / H.probability z ≤
          Real.exp (-(t : ℝ)*Real.log (G.size : ℝ) + J.cost-H.cost + Real.log 4*(t : ℝ)*G.b) := by
    …

    Mentions: OAI.CoordinateSweeps.FiniteLaw.uniform, OAI.CoordinateSweeps.lineLaw

24. def OAI.CoordinateSweeps.Grid.Holes.ValidInput line 290

    Source comment

    An injection into the actual available input slots.

    def ValidInput (H : G.Holes h) (x : Fin t → G.Slot) : Prop :=
    …

25. def OAI.CoordinateSweeps.Grid.Holes.augment line 295

    Source comment

    A feasible endpoint event augments the prescribed holes by the uniquely determined auxiliary paths. The witness is used only to verify disjointness.

    def augment (H : G.Holes h) (u v : Fin t → G.Slot) (hu : H.ValidInput u)
        (ω : G.Choices) (hω : H.Compatible ω) (hv : ∀ i, G.sweep ω (u i) = v i) :
        G.Holes (h+t) where
    …

26. theorem OAI.CoordinateSweeps.Grid.Holes.augment_old line 317
27. theorem OAI.CoordinateSweeps.Grid.Holes.augment_new line 323
28. theorem OAI.CoordinateSweeps.Grid.Holes.augment_extends line 330
29. theorem OAI.CoordinateSweeps.Grid.Holes.augment_compatible_iff line 336

    Source comment

    Exact equivalence of conditioning events, including all stage boundaries.

    theorem augment_compatible_iff (H : G.Holes h) (u v : Fin t → G.Slot) (hu : H.ValidInput u)
        (ω : G.Choices) (hω : H.Compatible ω) (hv : ∀ i, G.sweep ω (u i) = v i)
        (ν : G.Choices) :
        (H.augment u v hu ω hω hv).Compatible ν ↔
          H.Compatible ν ∧ ∀ i, G.sweep ν (u i) = v i := by
    …

    Mentions: OAI.CoordinateSweeps.Grid.Holes.Compatible

30. def OAI.CoordinateSweeps.Grid.Holes.selected line 359

    Source comment

    A canonical enumeration of a selected list of auxiliary cards.

    def selected (A : Finset (Fin k)) : Fin A.card ↪ Fin k :=
    …

31. theorem OAI.CoordinateSweeps.Grid.Holes.selected_mem line 362
32. theorem OAI.CoordinateSweeps.Grid.Holes.selected_range line 365
33. theorem OAI.CoordinateSweeps.Grid.Holes.validInput_selected line 370
34. theorem OAI.CoordinateSweeps.Grid.Holes.endpointEvent_iff_selected line 374