OAI/Probability/BinarySweep/Model.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.BinaryCoordinateSweeps.Slot line 10

   Source documentation

   The positions of a binary deck of dimension d.

   Also declared: ComparatorChallenges/BinarySweep.lean:10 (same declaration text).

   abbrev Slot (d : ℕ) := Fin d → Bool

2. def OAI.BinaryCoordinateSweeps.coordinateLayer line 13

   Source documentation

   Independent switches on the edges parallel to one coordinate.

   Also declared: ComparatorChallenges/BinarySweep.lean:13 (same declaration text).

   def coordinateLayer (d : ℕ) (j : Fin d)
       (c : (({i : Fin d // i ≠ j} → Bool)) → Bool) : Equiv.Perm (Slot d) :=
   …

   Mentions: OAI.BinaryCoordinateSweeps.Slot

3. abbrev OAI.BinaryCoordinateSweeps.SweepCoins line 23

   Also declared: ComparatorChallenges/BinarySweep.lean:23 (same declaration text).

4. def OAI.BinaryCoordinateSweeps.binarySweep line 27

   Source documentation

   The coordinate layers are applied in increasing coordinate order.

   Also declared: ComparatorChallenges/BinarySweep.lean:27 (same declaration text).

   def binarySweep (d : ℕ) (c : SweepCoins d) : Equiv.Perm (Slot d) :=
   …

   Mentions: OAI.BinaryCoordinateSweeps.SweepCoins, OAI.BinaryCoordinateSweeps.Slot

5. def OAI.BinaryCoordinateSweeps.finiteLaw line 30

   Also declared: ComparatorChallenges/BinarySweep.lean:30 (same declaration text).

6. def OAI.BinaryCoordinateSweeps.totalVariation line 35

   Source documentation

   Half the unnormalized sum of absolute probability-mass differences.

   Also declared: ComparatorChallenges/BinarySweep.lean:35 (same declaration text).

   def totalVariation {G : Type*} [Fintype G] (p q : G → ℝ) : ℝ :=
   …

7. def OAI.BinaryCoordinateSweeps.uniformLaw line 38

   Also declared: ComparatorChallenges/BinarySweep.lean:38 (same declaration text).

8. def OAI.BinaryCoordinateSweeps.binaryLaw line 41

   Also declared: ComparatorChallenges/BinarySweep.lean:41 (same declaration text).

9. abbrev OAI.BinaryCoordinateSweeps.RepSpace line 44

   Also declared: ComparatorChallenges/BinarySweep.lean:44 (same declaration text).

10. def OAI.BinaryCoordinateSweeps.IsUnitaryRep line 46

    Also declared: ComparatorChallenges/BinarySweep.lean:46 (same declaration text).

11. def OAI.BinaryCoordinateSweeps.averageOperator line 50

    Also declared: ComparatorChallenges/BinarySweep.lean:50 (same declaration text).

12. def OAI.BinaryCoordinateSweeps.BinaryContractionTarget line 55

    Also declared: ComparatorChallenges/BinarySweep.lean:55 (same declaration text).

13. def OAI.BinaryCoordinateSweeps.realSign line 61

    Also declared: ComparatorChallenges/BinarySweep.lean:61 (same declaration text).

14. def OAI.BinaryCoordinateSweeps.convolution line 67

    Also declared: ComparatorChallenges/BinarySweep.lean:67 (same declaration text).

15. def OAI.BinaryCoordinateSweeps.pointMassOne line 69

    Also declared: ComparatorChallenges/BinarySweep.lean:69 (same declaration text).

16. def OAI.BinaryCoordinateSweeps.convolutionPower line 74

    Source documentation

    The law of independent repetitions, with the empty product at the identity.

    Also declared: ComparatorChallenges/BinarySweep.lean:74 (same declaration text).

    def convolutionPower (p : G → ℝ) : ℕ → G → ℝ
      | 0 => pointMassOne
      | n + 1 => convolution p (convolutionPower p n)
    
    end FiniteLaws

    Mentions: OAI.BinaryCoordinateSweeps.pointMassOne, OAI.BinaryCoordinateSweeps.convolution

17. def OAI.BinaryCoordinateSweeps.sweepLaw line 80

    Also declared: ComparatorChallenges/BinarySweep.lean:80 (same declaration text).

18. def OAI.BinaryCoordinateSweeps.UniformSweepMixingTarget line 84

    Source documentation

    A single number of sweeps works uniformly over deterministic initial decks.

    Also declared: ComparatorChallenges/BinarySweep.lean:84 (same declaration text).

    def UniformSweepMixingTarget : Prop :=
    …