OAI/Combinatorics/PlanarL1/StepSuccess.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Parameters.successGain line 9
  2. lemma OAI.PlanarL1.Parameters.successGain_pos line 11
  3. lemma OAI.PlanarL1.Parameters.successGain_cutoff line 15
  4. lemma OAI.PlanarL1.Parameters.successGain_certificate line 16
  5. lemma OAI.PlanarL1.Parameters.successGain_main line 18
  6. lemma OAI.PlanarL1.Parameters.successGain_secondary line 20
  7. lemma OAI.PlanarL1.Parameters.successGain_increment line 22
  8. def OAI.PlanarL1.Parameters.successChance line 24
  9. lemma OAI.PlanarL1.Parameters.successChance_pos line 25
  10. lemma OAI.PlanarL1.Columns.Model.CoupledState.unchanged_success line 45
  11. lemma OAI.PlanarL1.Columns.Model.CoupledState.modes_unchanged line 49
  12. lemma OAI.PlanarL1.Columns.Model.CoupledState.modes_main line 57
  13. lemma OAI.PlanarL1.Columns.Model.CoupledState.modes_secondary line 69
  14. lemma OAI.PlanarL1.Columns.Model.CoupledState.modes_increment line 81
  15. lemma OAI.PlanarL1.Columns.Model.CoupledState.interior_success line 127
  16. lemma OAI.PlanarL1.Columns.Model.CoupledState.step_success line 180

    Source documentation

    Quantitative success of the actual coupled four-mode step. All randomness and surviving groups are sampled by the construction itself.

    lemma step_success (hmany : 10000 ≤ m) : successChance≤
    (S.step ht hgap v hv hm).prob (fun z => z.Successful v successGain x y) := by
…