OAI/Analysis/FourierLLogL/Procedure/Fork.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.FourierLLogL.Dyadic.Procedure.Scene.weight line 17

    Source documentation

    Absolute mass in the common top grid

    def weight (s : Scene M) := s.here.len * s.mass

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Scene

  2. def OAI.FourierLLogL.Dyadic.Procedure.Scene.insideW line 18
  3. def OAI.FourierLLogL.Dyadic.Procedure.Scene.weightE line 20
  4. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.mass_actor line 23
  5. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.actor_weight line 33
  6. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.Ex_weight line 39
  7. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.weight_pos line 44
  8. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.actor_reset line 47
  9. lemma OAI.FourierLLogL.Dyadic.Procedure.Scene.actor_out line 48
  10. structure OAI.FourierLLogL.Dyadic.Procedure.Fork line 53

    Source documentation

    Binary choices, left/right normalized.

    structure Fork (M : ℕ) where
…
  11. def OAI.FourierLLogL.Dyadic.Procedure.Fork.probs line 60
  12. structure OAI.FourierLLogL.Dyadic.Procedure.Fork.TrueLaw line 63

    Source documentation

    Include balance even to a zero-mass destination.

    structure TrueLaw (q : Fork M) : Prop where
…

    Mentions: OAI.FourierLLogL.Dyadic.Procedure.Fork

  13. def OAI.FourierLLogL.Dyadic.Procedure.Fork.step line 68
  14. def OAI.FourierLLogL.Dyadic.Procedure.Fork.toss line 73
  15. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.step_true line 78
  16. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.toss_true line 96
  17. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.balance line 116
  18. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.local_law line 124
  19. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.expect_bit line 130
  20. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.true_mass line 139
  21. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.branch_pos line 143
  22. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.step_mass line 151
  23. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.toss_mass line 157
  24. lemma OAI.FourierLLogL.Dyadic.Procedure.Fork.success_prob line 167