OAI/Computability/MaxCut/Encoding/BitPairWeightQ.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.OptimalMaxCut.LongCode.bitPairWeightQ line 12
2. def OAI.OptimalMaxCut.LongCode.corrAverageQ line 15
3. theorem OAI.OptimalMaxCut.LongCode.bitPairWeightQ_cast line 20
4. theorem OAI.OptimalMaxCut.LongCode.corrAverageQ_cast line 23
5. theorem OAI.OptimalMaxCut.LongCode.corrAverageQ_const line 30
6. theorem OAI.OptimalMaxCut.LongCode.corrAverageQ_nonneg line 34
7. theorem OAI.OptimalMaxCut.LongCode.corrAverageQ_sum line 44
8. def OAI.OptimalMaxCut.LongCode.jointLaw line 51

   Source documentation

   The joint law of all paired cube inputs, with actual rational point masses.

   def jointLaw (t : ℚ) (ht : t ∈ Set.Icc (-1 : ℚ) 1) (n : ℕ) : Law (Cube (Fin n) × Cube (Fin n)) where
   …

   Mentions: OAI.OptimalMaxCut.LongCode.Law

9. theorem OAI.OptimalMaxCut.LongCode.jointLaw_average line 58
10. def OAI.OptimalMaxCut.LongCode.Law.bind line 75

    Source documentation

    Finite conditional sampling; both the law and all output masses are rational.

    def bind (p : Law I) (q : I → Law J) : Law (I × J) where
    …

    Mentions: OAI.OptimalMaxCut.LongCode.Law

11. theorem OAI.OptimalMaxCut.LongCode.Law.bind_average line 82
12. theorem OAI.OptimalMaxCut.LongCode.Law.corrAverage_avg line 86
13. def OAI.OptimalMaxCut.LongCode.Game.sampleLaw line 98

    Source documentation

    Every atom records exactly the finite random choices made by the long-code Max-Cut test. In particular no real random numbers occur in the construction.

    def sampleLaw (G : Game X Y E q) (t : ℚ) (ht : t ∈ Set.Icc (-1 : ℚ) 1) :
        Law (Y × (E × (E × (Cube (Fin q) × Cube (Fin q))))) :=
    …

    Mentions: OAI.OptimalMaxCut.LongCode.Game, OAI.OptimalMaxCut.LongCode.Law

14. def OAI.OptimalMaxCut.LongCode.Game.queries line 104

    Source documentation

    The two actual graph vertices queried at each test atom.

    def queries (G : Game X Y E q)
        (a : Y × (E × (E × (Cube (Fin q) × Cube (Fin q))))) :
        (X × Cube (Fin q)) × (X × Cube (Fin q)) :=
    …

    Mentions: OAI.OptimalMaxCut.LongCode.Game

15. theorem OAI.OptimalMaxCut.LongCode.Game.testCut_expanded line 110
16. theorem OAI.OptimalMaxCut.LongCode.Game.testCut_sampleLaw line 128

    Source documentation

    The analytic test value is exactly the expectation over explicit rational atoms. This identity will be used to aggregate a genuine finite graph.

     theorem testCut_sampleLaw (G : Game X Y E q) (t : ℚ) (ht : t ∈ Set.Icc (-1 : ℚ) 1)
        (f : X → Cube (Fin q) → ℝ) :
        G.testCut t f = (G.sampleLaw t ht).avg (fun a =>
          (1 - f (G.queries a).1.1 (G.queries a).1.2 *
            f (G.queries a).2.1 (G.queries a).2.2) / 2) := by
    …

    Mentions: OAI.OptimalMaxCut.LongCode.Game