OAI/MeasureTheory/DyadicAvoidance/ConcreteLabelMeasures.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem310.ConcreteLabels.bitLaw line 14

    Source documentation

    The actual terminal-bit law used at parameter p.

    def bitLaw (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : Measure Bool :=
…
  2. instance OAI.Problem310.ConcreteLabels.bitLaw_probability line 17
  3. theorem OAI.Problem310.ConcreteLabels.bitLaw_true line 22
  4. theorem OAI.Problem310.ConcreteLabels.bitLaw_false line 27
  5. def OAI.Problem310.ConcreteLabels.fairLaw line 34

    Source documentation

    The actual fair law for selector table entries.

    def fairLaw : Measure Bool := bitLaw (1 / 2) (by norm_num) (by norm_num)

    Mentions: OAI.Problem310.ConcreteLabels.bitLaw

  6. instance OAI.Problem310.ConcreteLabels.fairLaw_probability line 36
  7. theorem OAI.Problem310.ConcreteLabels.fairLaw_singleton line 40
  8. def OAI.Problem310.ConcreteLabels.selectorLaw line 47

    Source documentation

    A finite table of independent fair selectors.

    def selectorLaw (S : Type u_S) [Fintype S] : Measure (S → Bool) :=
…
  9. instance OAI.Problem310.ConcreteLabels.selectorLaw_probability line 50
  10. def OAI.Problem310.ConcreteLabels.terminalLaw line 56

    Source documentation

    A finite table of independent Bernoulli terminal entries.

    def terminalLaw (T : Type u_T) [Fintype T] (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) :
    Measure (T → Bool) := Measure.pi fun _ => bitLaw p hp0 hp1

    Mentions: OAI.Problem310.ConcreteLabels.bitLaw

  11. instance OAI.Problem310.ConcreteLabels.terminalLaw_probability line 59
  12. def OAI.Problem310.ConcreteLabels.outcomeLaw line 66

    Source documentation

    Complete finite selector/terminal outcome law, with independent tables.

    def outcomeLaw (S : Type u_S) (T : Type u_T) [Fintype S] [Fintype T]
    (p : ℝ) (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : Measure ((S → Bool) × (T → Bool)) :=
…
  13. instance OAI.Problem310.ConcreteLabels.outcomeLaw_probability line 70
  14. theorem OAI.Problem310.ConcreteLabels.selectorLaw_singleton line 76
  15. theorem OAI.Problem310.ConcreteLabels.selectorLaw_singleton_pos line 80
  16. theorem OAI.Problem310.ConcreteLabels.selectorLaw_pos_of_nonempty line 86

    Source documentation

    Every center-exposure pattern that actually occurs has positive selector mass.

    theorem selectorLaw_pos_of_nonempty (S : Type u_S) [Fintype S]
    {A : Set (S → Bool)} (hA : A.Nonempty) : 0 < selectorLaw S A := by
…

    Mentions: OAI.Problem310.ConcreteLabels.selectorLaw

  17. theorem OAI.Problem310.ConcreteLabels.terminalLaw_singleton line 92
  18. theorem OAI.Problem310.ConcreteLabels.terminalLaw_singleton_pos line 101
  19. theorem OAI.Problem310.ConcreteLabels.outcomeLaw_singleton line 110
  20. theorem OAI.Problem310.ConcreteLabels.outcomeLaw_singleton_pos line 118