OAI/Probability/CoordinateSweeps/Conditioning.lean

GitHub source file

113 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CoordinateSweeps.Grid.concat line 31

   Source comment

   Concatenation of the *ordered* coordinate sequences.

   def concat (A B : Grid) : Grid where
   …

   Mentions: OAI.CoordinateSweeps.Grid

2. lemma OAI.CoordinateSweeps.Grid.concat_bits_left line 36
3. lemma OAI.CoordinateSweeps.Grid.concat_bits_right line 38
4. def OAI.CoordinateSweeps.Grid.splitSlots line 42

   Source comment

   Literal Cartesian identification for the split, retaining all bit labels.

   def splitSlots (A B : Grid) : (concat A B).Slot ≃ A.Slot × B.Slot :=
   …

   Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Slot

5. lemma OAI.CoordinateSweeps.Grid.splitSlots_left line 49
6. lemma OAI.CoordinateSweeps.Grid.splitSlots_right line 54
7. lemma OAI.CoordinateSweeps.Grid.concat_size line 59
8. lemma OAI.CoordinateSweeps.Grid.concat_allowed line 64
9. def OAI.CoordinateSweeps.finDeleteLeft line 82

   Source comment

   Deleting a head coordinate commutes with the literal Fin concatenation.

   def finDeleteLeft {m n : ℕ} (i : Fin m) :
       ({j : Fin m // j ≠ i} ⊕ Fin n) ≃ {j : Fin (m+n) // j ≠ Fin.castAdd n i} where
   …

10. lemma OAI.CoordinateSweeps.finDeleteLeft_inl line 97
11. lemma OAI.CoordinateSweeps.finDeleteLeft_inr line 99
12. def OAI.CoordinateSweeps.finDeleteRight line 103

    Source comment

    Deleting a tail coordinate, in the same original head-then-tail order.

    def finDeleteRight {m n : ℕ} (i : Fin n) :
        (Fin m ⊕ {j : Fin n // j ≠ i}) ≃ {j : Fin (m+n) // j ≠ Fin.natAdd m i} where
    …

13. lemma OAI.CoordinateSweeps.finDeleteRight_inl line 118
14. lemma OAI.CoordinateSweeps.finDeleteRight_inr line 120
15. def OAI.CoordinateSweeps.Grid.rowLines line 128

    Source comment

    Row line chart: the other head coordinates and the fixed tail row label.

    def rowLines (A B : Grid) (i : Fin A.b) :
        (A.Line i × B.Slot) ≃ (concat A B).Line (Fin.castAdd B.b i) :=
    …

    Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Line

16. def OAI.CoordinateSweeps.Grid.columnLines line 142

    Source comment

    Column line chart: the fixed head label and the other tail coordinates.

    def columnLines (A B : Grid) (i : Fin B.b) :
        (A.Slot × B.Line i) ≃ (concat A B).Line (Fin.natAdd A.b i) :=
    …

    Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Line

17. lemma OAI.CoordinateSweeps.Grid.rowLines_evaluation line 155
18. lemma OAI.CoordinateSweeps.Grid.columnLines_evaluation line 164
19. def OAI.CoordinateSweeps.Grid.leftCube line 177
20. def OAI.CoordinateSweeps.Grid.rightCube line 180
21. def OAI.CoordinateSweeps.Grid.prefixFiber line 184
22. def OAI.CoordinateSweeps.Grid.suffixFiber line 190
23. def OAI.CoordinateSweeps.Grid.choicesSplit line 197

    Source comment

    Exact two-part choice-space equivalence, not just an equality in law.

    def choicesSplit (A B : Grid) : (concat A B).Choices ≃
        ((B.Slot → A.Choices) × (A.Slot → B.Choices)) :=
    …

    Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Choices

24. def OAI.CoordinateSweeps.Grid.rowChoices line 210
25. def OAI.CoordinateSweeps.Grid.columnChoices line 212
26. lemma OAI.CoordinateSweeps.Grid.rowChoices_apply line 215
27. lemma OAI.CoordinateSweeps.Grid.columnChoices_apply line 220
28. lemma OAI.CoordinateSweeps.Grid.rowLines_at_slot line 229
29. lemma OAI.CoordinateSweeps.Grid.columnLines_at_slot line 235
30. theorem OAI.CoordinateSweeps.Grid.stage_split_left line 242

    Source comment

    A head stage really acts by independent row stages in the Cartesian chart.

    theorem stage_split_left (A B : Grid) (ω : (concat A B).Choices) (i : Fin A.b)
        (x : (concat A B).Slot) :
        splitSlots A B ((concat A B).stage ω (Fin.castAdd B.b i) x)=
          (A.stage (rowChoices A B ω (splitSlots A B x).2) i (splitSlots A B x).1,
            (splitSlots A B x).2) := by
    …

    Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Choices, OAI.CoordinateSweeps.Grid.Slot, OAI.CoordinateSweeps.Grid.splitSlots, OAI.CoordinateSweeps.Grid.stage, OAI.CoordinateSweeps.Grid.rowChoices

31. theorem OAI.CoordinateSweeps.Grid.stage_split_right line 265

    Source comment

    A tail stage really acts by independent column stages.

    theorem stage_split_right (A B : Grid) (ω : (concat A B).Choices) (i : Fin B.b)
        (x : (concat A B).Slot) :
        splitSlots A B ((concat A B).stage ω (Fin.natAdd A.b i) x)=
          ((splitSlots A B x).1,B.stage (columnChoices A B ω (splitSlots A B x).1) i (splitSlots A B x).2) := by
    …

    Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Choices, OAI.CoordinateSweeps.Grid.Slot, OAI.CoordinateSweeps.Grid.splitSlots, OAI.CoordinateSweeps.Grid.stage, OAI.CoordinateSweeps.Grid.columnChoices

32. lemma OAI.CoordinateSweeps.Grid.boundary_split_prefix line 290
33. lemma OAI.CoordinateSweeps.Grid.boundary_split_suffix line 305
34. theorem OAI.CoordinateSweeps.Grid.sweep_split line 323

    Source comment

    Actual ordered permutation factorization: row sweeps, then column sweeps.

    theorem sweep_split (A B : Grid) (ω : (concat A B).Choices) (x : (concat A B).Slot) :
        splitSlots A B ((concat A B).sweep ω x)=
          (A.sweep (rowChoices A B ω (splitSlots A B x).2) (splitSlots A B x).1,
           B.sweep (columnChoices A B ω
             (A.sweep (rowChoices A B ω (splitSlots A B x).2) (splitSlots A B x).1))
             (splitSlots A B x).2) :=
    …

    Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Choices, OAI.CoordinateSweeps.Grid.Slot, OAI.CoordinateSweeps.Grid.splitSlots, OAI.CoordinateSweeps.Grid.sweep, OAI.CoordinateSweeps.Grid.rowChoices, OAI.CoordinateSweeps.Grid.columnChoices

35. def OAI.CoordinateSweeps.Grid.prefixTime line 335
36. def OAI.CoordinateSweeps.Grid.suffixTime line 337
37. def OAI.CoordinateSweeps.Grid.Holes.rowOf line 343
38. def OAI.CoordinateSweeps.Grid.Holes.columnOf line 344
39. lemma OAI.CoordinateSweeps.Grid.Holes.row_constant line 346
40. lemma OAI.CoordinateSweeps.Grid.Holes.column_constant line 354
41. abbrev OAI.CoordinateSweeps.Grid.Holes.RowCard line 364
42. abbrev OAI.CoordinateSweeps.Grid.Holes.ColumnCard line 365
43. def OAI.CoordinateSweeps.Grid.Holes.rowCount line 366
44. def OAI.CoordinateSweeps.Grid.Holes.columnCount line 367
45. def OAI.CoordinateSweeps.Grid.Holes.rowCards line 368
46. def OAI.CoordinateSweeps.Grid.Holes.columnCards line 369
47. def OAI.CoordinateSweeps.Grid.Holes.rowHoles line 372

    Source comment

    All holes in one actual row, with the inherited ordered trajectories.

    def rowHoles (y : B.Slot) : A.Holes (H.rowCount y) where
    …

48. def OAI.CoordinateSweeps.Grid.Holes.columnHoles line 394

    Source comment

    All holes in one junction column, with the inherited tail trajectories.

    def columnHoles (x : A.Slot) : B.Holes (H.columnCount x) where
    …

49. lemma OAI.CoordinateSweeps.Grid.Holes.sum_rowCount line 417
50. lemma OAI.CoordinateSweeps.Grid.Holes.sum_columnCount line 421
51. lemma OAI.CoordinateSweeps.Grid.Holes.row_step_iff line 432
52. lemma OAI.CoordinateSweeps.Grid.Holes.column_step_iff line 446
53. theorem OAI.CoordinateSweeps.Grid.Holes.compatible_split line 461

    Source comment

    The trajectory event is exactly the product of all child trajectory events.

    theorem compatible_split (ω : (concat A B).Choices) :
        H.Compatible ω ↔
          (∀ y : B.Slot, (H.rowHoles y).Compatible (rowChoices A B ω y)) ∧
          (∀ x : A.Slot, (H.columnHoles x).Compatible (columnChoices A B ω x)) := by
    …

    Mentions: OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Choices, OAI.CoordinateSweeps.Grid.Holes.Compatible, OAI.CoordinateSweeps.Grid.rowChoices, OAI.CoordinateSweeps.Grid.columnChoices

54. def OAI.CoordinateSweeps.Grid.rawLineWeight line 524

    Source comment

    The literal real line mass, without changing any conditioning.

    def rawLineWeight (k : ℕ) (z : ℝ) (σ : Equiv.Perm (Cube k)) : ℝ :=
    …

    Mentions: OAI.CoordinateSweeps.Cube

55. lemma OAI.CoordinateSweeps.Grid.rawLineWeight_cast line 527
56. lemma OAI.CoordinateSweeps.Grid.prefix_weight line 532
57. lemma OAI.CoordinateSweeps.Grid.suffix_weight line 545
58. theorem OAI.CoordinateSweeps.Grid.choiceWeight_split line 559

    Source comment

    Complete independent choice mass factors into literal row and column masses.

    theorem choiceWeight_split (A B : Grid) (ω : (concat A B).Choices) (z : ℝ) :
        (concat A B).choiceWeight z ω =
          (∏ y : B.Slot, A.choiceWeight z (rowChoices A B ω y))*
          (∏ x : A.Slot, B.choiceWeight z (columnChoices A B ω x)) := by
    …

    Mentions: OAI.CoordinateSweeps.Grid, OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Choices, OAI.CoordinateSweeps.Grid.choiceWeight, OAI.CoordinateSweeps.Grid.rowChoices, OAI.CoordinateSweeps.Grid.columnChoices

59. def OAI.CoordinateSweeps.Grid.Holes.splitCompatibleChoices line 592
60. lemma OAI.CoordinateSweeps.Grid.Holes.splitCompatibleChoices_weight line 623
61. theorem OAI.CoordinateSweeps.Grid.Holes.probability_split line 638

    Source comment

    Exact product of all child path-event probabilities, for the real law.

    theorem probability_split (z : ℝ) :
        H.probability z=(∏ y, (H.rowHoles y).probability z)*(∏ x, (H.columnHoles x).probability z) := by
    …

    Mentions: OAI.CoordinateSweeps.Grid.Holes.probability

62. theorem OAI.CoordinateSweeps.Grid.Holes.conditionalWeight_split line 656

    Source comment

    Literal normalized conditional mass factors; no trajectory is reweighted.

    theorem conditionalWeight_split (z : ℝ) (ω : {ω : (concat A B).Choices // H.Compatible ω}) :
        (concat A B).choiceWeight z ω.val/H.probability z=
          (∏ y, A.choiceWeight z (rowChoices A B ω.val y)/(H.rowHoles y).probability z)*
          (∏ x, B.choiceWeight z (columnChoices A B ω.val x)/(H.columnHoles x).probability z) := by
    …

    Mentions: OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Choices, OAI.CoordinateSweeps.Grid.choiceWeight, OAI.CoordinateSweeps.Grid.rowChoices, OAI.CoordinateSweeps.Grid.Holes.probability, OAI.CoordinateSweeps.Grid.columnChoices

63. abbrev OAI.CoordinateSweeps.Marked.Free line 668
64. def OAI.CoordinateSweeps.Marked.freeEquiv line 670
65. lemma OAI.CoordinateSweeps.Marked.freeEquiv_apply line 681
66. def OAI.CoordinateSweeps.Marked.fix line 684
67. def OAI.CoordinateSweeps.Marked.freePerm line 693
68. def OAI.CoordinateSweeps.Marked.freePermEquiv line 699

    Source comment

    The honest symmetric group on the unmarked sites, including empty sets.

    def freePermEquiv (x : I → X) : fix x ≃* Equiv.Perm (Free x) where
    …

    Mentions: OAI.CoordinateSweeps.Marked.fix, OAI.CoordinateSweeps.Marked.Free

69. lemma OAI.CoordinateSweeps.Marked.card_free line 722
70. theorem OAI.CoordinateSweeps.Grid.card_slot line 734
71. abbrev OAI.CoordinateSweeps.Grid.Holes.FreeAt line 739
72. def OAI.CoordinateSweeps.Grid.Holes.freeBoundary line 741
73. lemma OAI.CoordinateSweeps.Grid.Holes.card_freeAt line 745
74. def OAI.CoordinateSweeps.Grid.Holes.stabilizerFreeEquiv line 754

    Source comment

    Literal target stabilizer isomorphism, not an assumed representation switch.

    def stabilizerFreeEquiv (H : G.Holes h) : H.stabilizer ≃* Equiv.Perm (H.FreeAt 0) :=
    …

75. lemma OAI.CoordinateSweeps.Grid.Holes.stabilizerFreeEquiv_apply line 757
76. def OAI.CoordinateSweeps.Grid.rowSweep line 765
77. def OAI.CoordinateSweeps.Grid.columnSweep line 768
78. lemma OAI.CoordinateSweeps.Grid.rowSweep_apply line 772
79. lemma OAI.CoordinateSweeps.Grid.columnSweep_apply line 779
80. theorem OAI.CoordinateSweeps.Grid.sweep_eq_column_mul_row line 787
81. theorem OAI.CoordinateSweeps.Grid.rowSweep_eq_boundary line 798
82. abbrev OAI.CoordinateSweeps.Grid.Holes.RowChoices line 808
83. abbrev OAI.CoordinateSweeps.Grid.Holes.ColumnChoices line 809
84. def OAI.CoordinateSweeps.Grid.Holes.refPair line 811
85. def OAI.CoordinateSweeps.Grid.Holes.rowAction line 814
86. def OAI.CoordinateSweeps.Grid.Holes.columnAction line 815
87. lemma OAI.CoordinateSweeps.Grid.Holes.split_choice_sweep line 817
88. lemma OAI.CoordinateSweeps.Grid.Holes.rowAction_marked line 825
89. lemma OAI.CoordinateSweeps.Grid.Holes.columnAction_marked line 836
90. abbrev OAI.CoordinateSweeps.Grid.Holes.JunctionFix line 848
91. def OAI.CoordinateSweeps.Grid.Holes.rowResidual line 850
92. def OAI.CoordinateSweeps.Grid.Holes.columnResidual line 856
93. def OAI.CoordinateSweeps.Grid.Holes.junctionEquiv line 869

    Source comment

    Move the target's reference identification to the actual junction layer.

    def junctionEquiv (hf : H.Feasible) : H.stabilizer ≃* H.JunctionFix where
    …

94. lemma OAI.CoordinateSweeps.Grid.Holes.sweep_refPair line 899
95. lemma OAI.CoordinateSweeps.Grid.Holes.junction_residual line 903
96. instance OAI.CoordinateSweeps.Grid.Holes.rowChoicesFintype line 917
97. instance OAI.CoordinateSweeps.Grid.Holes.columnChoicesFintype line 922
98. def OAI.CoordinateSweeps.Grid.Holes.rowAverage line 928

    Source comment

    Arbitrary matrix representations may be used: the equality is at the law level.

    def rowAverage {n : Type*} [Fintype n] [DecidableEq n] (hf : H.Feasible) (z : ℝ)
        (τ : H.JunctionFix →* Matrix n n ℂ) : Matrix n n ℂ :=
    …

99. def OAI.CoordinateSweeps.Grid.Holes.columnAverage line 933
100. theorem OAI.CoordinateSweeps.Grid.Holes.junction_average_split line 940

     Source comment

     Exact factorization of the faithful conditional matrix average at the junction.

     theorem junction_average_split {n : Type*} [Fintype n] [DecidableEq n]
         (hf : H.Feasible) (z : ℝ) (τ : H.JunctionFix →* Matrix n n ℂ) :
         (∑ ω : {ω : (concat A B).Choices // H.Compatible ω},
           (((concat A B).choiceWeight z ω.val/H.probability z : ℝ) : ℂ) •
             τ (H.junctionEquiv hf (H.residual hf ω)))=
           H.columnAverage hf z τ*H.rowAverage hf z τ := by
     …

     Mentions: OAI.CoordinateSweeps.Grid.concat, OAI.CoordinateSweeps.Grid.Choices, OAI.CoordinateSweeps.Grid.choiceWeight

101. def OAI.CoordinateSweeps.Grid.Holes.conditionalAverage line 980

     Source comment

     Average of the remaining random bijection, conditioned on the entire paths, not only endpoints. The reference affects only unitary identifications.

     Also declared: ComparatorChallenges/CoordinateSweeps.lean:213 (same declaration text).

     def conditionalAverage (H : G.Holes h) (hf : H.Feasible) (z : ℝ)
         (ρ : UnitaryIrrep H.stabilizer) : Matrix (Fin ρ.dimension) (Fin ρ.dimension) ℂ :=
     …

     Mentions: OAI.CoordinateSweeps.UnitaryIrrep

102. theorem OAI.CoordinateSweeps.Grid.Holes.probability_pos line 986
103. theorem OAI.CoordinateSweeps.Grid.Holes.conditionalAverage_eq_sum line 995
104. theorem OAI.CoordinateSweeps.Grid.Holes.conditionalAverage_norm_le line 1004
105. theorem OAI.CoordinateSweeps.Grid.Holes.conditionalMoment_nonneg line 1017
106. theorem OAI.CoordinateSweeps.Grid.Holes.conditionalMoment_le_dimension line 1022
107. def OAI.CoordinateSweeps.a line 1035

     Source comment

     Source constants a=1/100, c0=e0=a/100.

     Also declared: ComparatorChallenges/CoordinateSweeps.lean:221 (same declaration text).

     def a : ℝ := 1 / 100

108. def OAI.CoordinateSweeps.c0 line 1036

     Also declared: ComparatorChallenges/CoordinateSweeps.lean:222 (same declaration text).

109. def OAI.CoordinateSweeps.e0 line 1037

     Also declared: ComparatorChallenges/CoordinateSweeps.lean:223 (same declaration text).

110. def OAI.CoordinateSweeps.c line 1038

     Also declared: ComparatorChallenges/CoordinateSweeps.lean:224 (same declaration text).

111. def OAI.CoordinateSweeps.e line 1039

     Also declared: ComparatorChallenges/CoordinateSweeps.lean:225 (same declaration text).

112. def OAI.CoordinateSweeps.logMoment line 1042

     Source comment

     Natural logarithm with the manuscript's log zero = minus infinity.

     Also declared: ComparatorChallenges/CoordinateSweeps.lean:228 (same declaration text).

     def logMoment (t : ℝ) : EReal := if t = 0 then ⊥ else (Real.log t : EReal)

113. def OAI.CoordinateSweeps.ConditionalMain line 1046

     Source comment

     Faithful conditional main target; R=2^r. The harmless strengthening z_*≤1/2 makes the probability-law range explicit.

     Also declared: ComparatorChallenges/CoordinateSweeps.lean:230 (same declaration text).

     def ConditionalMain : Prop :=
     …