OAI/Computability/MaxCut/Encoding/Bit.lean

GitHub source file

63 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.OptimalMaxCut.TreeCode.Bit line 10
2. abbrev OAI.OptimalMaxCut.TreeCode.Branch line 11
3. abbrev OAI.OptimalMaxCut.TreeCode.Table line 12
4. def OAI.OptimalMaxCut.TreeCode.Nodes line 14
5. def OAI.OptimalMaxCut.TreeCode.Leaves line 18
6. instance OAI.OptimalMaxCut.TreeCode.nodesFintype line 22
7. instance OAI.OptimalMaxCut.TreeCode.leavesFintype line 27
8. instance OAI.OptimalMaxCut.TreeCode.nodesDecidableEq line 32
9. instance OAI.OptimalMaxCut.TreeCode.leavesDecidableEq line 37
10. theorem OAI.OptimalMaxCut.TreeCode.card_leaves line 42
11. def OAI.OptimalMaxCut.TreeCode.gate line 53
12. def OAI.OptimalMaxCut.TreeCode.word line 58

    Source documentation

    The same complete 2s-ary tree code, with leaves canonically indexed by branch words instead of choosing an arbitrary bijection with Fin k.

    def word {s : ℕ} : {m : ℕ} → (Nodes s m → Table s) → (Leaves s m → Bit) → Bit
      | 0, _, x => x ()
      | _m + 1, F, x => gate (F (.inl ())) (fun gb =>
          word (fun v => F (.inr (gb, v))) (fun i => x (gb, i)))

    Mentions: OAI.OptimalMaxCut.TreeCode.Nodes, OAI.OptimalMaxCut.TreeCode.Table, OAI.OptimalMaxCut.TreeCode.Leaves, OAI.OptimalMaxCut.TreeCode.Bit, OAI.OptimalMaxCut.TreeCode.gate

13. inductive OAI.OptimalMaxCut.TreeCode.Slice line 63
14. def OAI.OptimalMaxCut.TreeCode.onSlice line 68

    Source documentation

    Membership in the slice, for a tree of any total depth.

    def onSlice {s : ℕ} : {j m : ℕ} → Slice s j → Nodes s m → Bool
      | _, 0, _, v => nomatch v
      | 0, _ + 1, .root, .inl _ => true
      | 0, _ + 1, .root, .inr _ => false
      | _ + 1, _ + 1, .next _ _, .inl _ => false
      | _ + 1, _ + 1, .next g child, .inr ((g', b), v) =>
          if g' = g then onSlice (child b) v else false
    
    /-- Negate exactly the whole tables on the fixed slice, and no other table. -/

    Mentions: OAI.OptimalMaxCut.TreeCode.Slice, OAI.OptimalMaxCut.TreeCode.Nodes

15. def OAI.OptimalMaxCut.TreeCode.flipTables line 77

    Source documentation

    Negate exactly the whole tables on the fixed slice, and no other table.

    def flipTables {s j m : ℕ} (S : Slice s j) (F : Nodes s m → Table s) :
        Nodes s m → Table s := fun v z => F v z + if onSlice S v then 1 else 0

    Mentions: OAI.OptimalMaxCut.TreeCode.Slice, OAI.OptimalMaxCut.TreeCode.Nodes, OAI.OptimalMaxCut.TreeCode.Table, OAI.OptimalMaxCut.TreeCode.onSlice

16. theorem OAI.OptimalMaxCut.TreeCode.bit_add_self line 80
17. theorem OAI.OptimalMaxCut.TreeCode.bit_one_add_one line 84
18. theorem OAI.OptimalMaxCut.TreeCode.gate_pair_flip line 88

    Source documentation

    Simultaneously multiplying the two children in pair g by -1 leaves all inputs to the gate table fixed and multiplies its prefactor by -1.

    theorem gate_pair_flip {s : ℕ} (F : Table s) (Z : Branch s → Bit) (g : Fin s) :
        gate F (fun gb => Z gb + if gb.1 = g then 1 else 0) = gate F Z + 1 := by
    …

    Mentions: OAI.OptimalMaxCut.TreeCode.Table, OAI.OptimalMaxCut.TreeCode.Branch, OAI.OptimalMaxCut.TreeCode.Bit, OAI.OptimalMaxCut.TreeCode.gate

19. theorem OAI.OptimalMaxCut.TreeCode.word_flipTables line 108
20. theorem OAI.OptimalMaxCut.TreeCode.bit_cases line 156
21. def OAI.OptimalMaxCut.TreeCode.sign line 161
22. theorem OAI.OptimalMaxCut.TreeCode.sign_zero line 163
23. theorem OAI.OptimalMaxCut.TreeCode.sign_one line 164
24. theorem OAI.OptimalMaxCut.TreeCode.sign_add line 166
25. theorem OAI.OptimalMaxCut.TreeCode.sign_sq line 170
26. theorem OAI.OptimalMaxCut.TreeCode.sign_add_one line 173
27. theorem OAI.OptimalMaxCut.TreeCode.sign_sum line 177
28. theorem OAI.OptimalMaxCut.TreeCode.gate_sign line 186

    Source documentation

    The implemented gate is EXACTLY equation (gate-rule), not a replacement operator with only the same symmetry.

     theorem gate_sign {s : ℕ} (F : Table s) (Z : Branch s → Bit) :
        sign (gate F Z) =
          (∏ g, sign (Z (g, false))) * sign (F (fun g => Z (g, false) + Z (g, true))) := by
    …

    Mentions: OAI.OptimalMaxCut.TreeCode.Table, OAI.OptimalMaxCut.TreeCode.Branch, OAI.OptimalMaxCut.TreeCode.Bit, OAI.OptimalMaxCut.TreeCode.sign, OAI.OptimalMaxCut.TreeCode.gate

29. def OAI.OptimalMaxCut.TreeCode.labelWord line 193
30. theorem OAI.OptimalMaxCut.TreeCode.labelWord_flipTables line 196
31. def OAI.OptimalMaxCut.TreeCode.Odd line 202
32. theorem OAI.OptimalMaxCut.TreeCode.code_flipTables line 205
33. abbrev OAI.OptimalMaxCut.TreeCode.SliceNode line 212
34. abbrev OAI.OptimalMaxCut.TreeCode.SliceTables line 215
35. def OAI.OptimalMaxCut.TreeCode.fillTables line 219

    Source documentation

    Fill the slice with independently supplied complete Boolean tables, leaving all outside tables at their fixed values.

    def fillTables {s j m : ℕ} (S : Slice s j) (outside : Nodes s m → Table s)
        (inside : SliceTables (m := m) S) : Nodes s m → Table s :=
    …

    Mentions: OAI.OptimalMaxCut.TreeCode.Slice, OAI.OptimalMaxCut.TreeCode.Nodes, OAI.OptimalMaxCut.TreeCode.Table, OAI.OptimalMaxCut.TreeCode.SliceTables

36. def OAI.OptimalMaxCut.TreeCode.insideFlip line 224

    Source documentation

    The measure-preserving simultaneous negation of all slice-entry signs.

    def insideFlip {s j m : ℕ} (S : Slice s j) :
        SliceTables (m := m) S ≃ SliceTables (m := m) S where
    …

    Mentions: OAI.OptimalMaxCut.TreeCode.Slice, OAI.OptimalMaxCut.TreeCode.SliceTables

37. theorem OAI.OptimalMaxCut.TreeCode.fillTables_insideFlip line 231
38. theorem OAI.OptimalMaxCut.TreeCode.conditional_code_mean_zero line 242

    Source documentation

    The precise conditional balancing assertion used in extraction Step 1. Rows, all outside tables, and the fixed slice are arbitrary and NOT averaged. Only independent uniform slice bits are averaged.

     theorem conditional_code_mean_zero {A : Type*} {s j m : ℕ} (S : Slice s j)
        (hjm : j < m) (outside : Nodes s m → Table s) (R : Leaves s m → A → Bit)
        (φ : (A → Bit) → ℝ) (hφ : Odd φ) :
        (𝔼 inside : SliceTables (m := m) S, φ (labelWord (fillTables S outside inside) R)) = 0 := by
    …

    Mentions: OAI.OptimalMaxCut.TreeCode.Slice, OAI.OptimalMaxCut.TreeCode.Nodes, OAI.OptimalMaxCut.TreeCode.Table, OAI.OptimalMaxCut.TreeCode.Leaves, OAI.OptimalMaxCut.TreeCode.Bit, OAI.OptimalMaxCut.TreeCode.Odd, OAI.OptimalMaxCut.TreeCode.SliceTables, OAI.OptimalMaxCut.TreeCode.labelWord, OAI.OptimalMaxCut.TreeCode.fillTables

39. def OAI.OptimalMaxCut.TreeCode.rowKernel line 267

    Source documentation

    Exactly retain the old whole row with probability r, otherwise draw an independent uniform whole row. This is not independent noise on its bits.

    noncomputable def rowKernel (r : ℝ) (x y : H) : ℝ :=
    …

40. theorem OAI.OptimalMaxCut.TreeCode.rowKernel_nonneg line 270
41. theorem OAI.OptimalMaxCut.TreeCode.rowKernel_sum line 277
42. theorem OAI.OptimalMaxCut.TreeCode.rowKernel_symm line 285
43. def OAI.OptimalMaxCut.TreeCode.rowsKernel line 288
44. theorem OAI.OptimalMaxCut.TreeCode.rowsKernel_nonneg line 292
45. theorem OAI.OptimalMaxCut.TreeCode.rowsKernel_sum line 296
46. def OAI.OptimalMaxCut.TreeCode.rowSmoothing line 301
47. theorem OAI.OptimalMaxCut.TreeCode.rowSmoothing_range line 304
48. theorem OAI.OptimalMaxCut.TreeCode.conditional_smoothed_code_mean_zero line 323

    Source documentation

    Exact conditional balancing survives whole-row resampling, with fixed rows/outside tables/slice. No probabilistic averaging of those contexts is used.

     theorem conditional_smoothed_code_mean_zero {A H : Type*} [Fintype H]
        [DecidableEq H] [Nonempty H] {s j m : ℕ} (S : Slice s j) (hjm : j < m)
        (outside : Nodes s m → Table s) (evalRow : H → A → Bit) (r : ℝ)
        (R : Leaves s m → H) (φ : (A → Bit) → ℝ) (hφ : Odd φ) :
        (𝔼 inside : SliceTables (m := m) S,
    …

    Mentions: OAI.OptimalMaxCut.TreeCode.Slice, OAI.OptimalMaxCut.TreeCode.Nodes, OAI.OptimalMaxCut.TreeCode.Table, OAI.OptimalMaxCut.TreeCode.Bit, OAI.OptimalMaxCut.TreeCode.Leaves, OAI.OptimalMaxCut.TreeCode.Odd, OAI.OptimalMaxCut.TreeCode.SliceTables

49. def OAI.OptimalMaxCut.TreeCode.character line 342

    Source documentation

    Probability-normalized finite Walsh transform, expressed in the same sign-bit coordinates as the tree.

    def character (q x : I → Bit) : ℝ := ∏ i, sign (q i * x i)

    Mentions: OAI.OptimalMaxCut.TreeCode.Bit, OAI.OptimalMaxCut.TreeCode.sign

50. theorem OAI.OptimalMaxCut.TreeCode.bit_character_orthogonality line 344
51. theorem OAI.OptimalMaxCut.TreeCode.character_symm line 353
52. theorem OAI.OptimalMaxCut.TreeCode.character_sum_orthogonality line 356
53. def OAI.OptimalMaxCut.TreeCode.bitCoefficient line 371
54. theorem OAI.OptimalMaxCut.TreeCode.bitWalsh_inversion line 374
55. theorem OAI.OptimalMaxCut.TreeCode.gate_expansion line 393
56. theorem OAI.OptimalMaxCut.TreeCode.rowSmoothing_one line 416
57. theorem OAI.OptimalMaxCut.TreeCode.rowSmoothing_sum line 422
58. theorem OAI.OptimalMaxCut.TreeCode.rowSmoothing_smul line 429
59. theorem OAI.OptimalMaxCut.TreeCode.rowSmoothing_tensor line 438

    Source documentation

    Independence of whole-row resampling across disjoint complete subtrees.

     theorem rowSmoothing_tensor (r : ℝ) (f : I → (J → H) → ℝ) (R : I × J → H) :
        rowSmoothing r (fun x => ∏ i, f i (fun j => x (i, j))) R =
          ∏ i, rowSmoothing r (f i) (fun j => R (i, j)) := by
    …

    Mentions: OAI.OptimalMaxCut.TreeCode.rowSmoothing

60. theorem OAI.OptimalMaxCut.TreeCode.rowSmoothing_pairs line 454

    Source documentation

    A tensor product with one chosen member of each ordered pair. The unused subtrees are integrated with total mass exactly one.

     theorem rowSmoothing_pairs {s : ℕ} (r : ℝ) (b : Fin s → Bool)
        (f : Branch s → (J → H) → ℝ) (R : Branch s × J → H) :
        rowSmoothing r (fun x => ∏ g, f (g, b g) (fun j => x ((g, b g), j))) R =
          ∏ g, rowSmoothing r (f (g, b g)) (fun j => R ((g, b g), j)) := by
    …

    Mentions: OAI.OptimalMaxCut.TreeCode.Branch, OAI.OptimalMaxCut.TreeCode.rowSmoothing

61. theorem OAI.OptimalMaxCut.TreeCode.sum_sign line 475
62. theorem OAI.OptimalMaxCut.TreeCode.rowKernel_sign line 481
63. theorem OAI.OptimalMaxCut.TreeCode.word_leaf_smoothing line 487