OAI/Combinatorics/PlanarL1/SelectedGain.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.PlanarL1.Columns.Model.BData.comparison_distance line 13
2. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.gain_of_suppression line 63
3. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.admitted_probability line 84
4. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.componentOf line 113
5. def OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.endpoint line 116
6. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.endpoint_mem line 123
7. lemma OAI.PlanarL1.Columns.Model.SecondaryGeometry.Group.endpoint_admitted line 127
8. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.bvalue_transport line 151
9. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.groupOf_index line 157
10. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.groupOf_lower line 158
11. def OAI.PlanarL1.Columns.Model.RetainedSelection.selectedComponent line 160
12. def OAI.PlanarL1.Columns.Model.RetainedSelection.selectedPoint line 162
13. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.selectedPoint_column line 165
14. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.selectedPoint_height line 166
15. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.selectedPoint_mem line 167
16. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.selectedPoint_plateau line 171
17. def OAI.PlanarL1.Columns.Model.RetainedSelection.blockFor line 185
18. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.selected_admitted_probability line 200
19. def OAI.PlanarL1.Columns.Model.BData.normalizedIncrement line 250
20. lemma OAI.PlanarL1.Columns.Model.BData.normalizedIncrement_coordinates line 254
21. def OAI.PlanarL1.Columns.Model.IncrementStep.update line 268
22. lemma OAI.PlanarL1.Columns.Model.IncrementStep.names line 274
23. lemma OAI.PlanarL1.Columns.Model.IncrementStep.separation_lower line 277
24. lemma OAI.PlanarL1.Columns.Model.IncrementStep.favorable_sign line 310

    Source documentation

    The actual simultaneous append of every old ordered history has at least one favorable value of the common identifier's fair coin.

    lemma favorable_sign : ∃ e : Bool, ∀ sign : Fin (S.count+1) → Bool, sign a=e →
        kappaB*lambda*R/50≤(update A S hist hcross hrec sign).sets.separation
          x.column x.height y.column y.height := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.IncrementStep.update

25. lemma OAI.PlanarL1.Columns.Model.IncrementStep.success_probability line 338
26. def OAI.PlanarL1.Columns.Model.RetainedSelection.ofWitness line 365
27. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.ordered_of_rejected line 373
28. theorem OAI.PlanarL1.Columns.Model.RetainedSelection.transverse_of_rejected line 390

    Source documentation

    The two actual retained endpoint groups, rather than hypothetical seeds, force transverse values in their actual common old ordered chart.

    theorem transverse_of_rejected
        (hwp : ¬(group A SA SB v hv (groupOf A SA SB v hv w)).Admitted true
          (selectedComponent A SA SB v hv w) (selectedPoint A SA SB v hv w))
        (hwn : ¬(group A SA SB v hv (groupOf A SA SB v hv w)).Admitted false
          (selectedComponent A SA SB v hv w) (selectedPoint A SA SB v hv w))
        (hzp : ¬(group A SA SB v hv (groupOf A SA SB v hv z)).Admitted true
          (selectedComponent A SA SB v hv z) (selectedPoint A SA SB v hv z))
        (hzn : ¬(group A SA SB v hv (groupOf A SA SB v hv z)).Admitted false
          (selectedComponent A SA SB v hv z) (selectedPoint A SA SB v hv z)) :
        ∃ (D : OrderedData M) (_hD : SB.chart (indexB A SB v w.val)=.ordered D)
          (x y : M.Point D.band (v w.val).column),
          x.column=(v w.val).column ∧ x.height=(v w.val).height ∧
    …

    Mentions: OAI.PlanarL1.Columns.Model.RetainedSelection.group, OAI.PlanarL1.Columns.Model.RetainedSelection.groupOf, OAI.PlanarL1.Columns.Model.RetainedSelection.selectedComponent, OAI.PlanarL1.Columns.Model.RetainedSelection.selectedPoint, OAI.PlanarL1.Columns.Model.OrderedData

29. lemma OAI.PlanarL1.Columns.Model.RetainedSelection.rejected_increment_probability line 475

    Source documentation

    Both actual endpoint rejections force success of the genuine simultaneous history increment with one favorable independent fair identifier coin.

    lemma rejected_increment_probability
        (hwp : ¬(group A SA SB v hv (groupOf A SA SB v hv w)).Admitted true
          (selectedComponent A SA SB v hv w) (selectedPoint A SA SB v hv w))
        (hwn : ¬(group A SA SB v hv (groupOf A SA SB v hv w)).Admitted false
          (selectedComponent A SA SB v hv w) (selectedPoint A SA SB v hv w))
        (hzp : ¬(group A SA SB v hv (groupOf A SA SB v hv z)).Admitted true
          (selectedComponent A SA SB v hv z) (selectedPoint A SA SB v hv z))
        (hzn : ¬(group A SA SB v hv (groupOf A SA SB v hv z)).Admitted false
          (selectedComponent A SA SB v hv z) (selectedPoint A SA SB v hv z)) :
        1/2≤FiniteRandom.prob (fun sign : Fin (SB.count+1) → Bool =>
          kappaB*lambda*R/50≤(IncrementStep.update A SB hist hcross hrec sign).sets.separation
            (v w.val).column (v w.val).height (v z.val).column (v z.val).height) := by
    …

    Mentions: OAI.PlanarL1.Columns.Model.RetainedSelection.group, OAI.PlanarL1.Columns.Model.RetainedSelection.groupOf, OAI.PlanarL1.Columns.Model.RetainedSelection.selectedComponent, OAI.PlanarL1.Columns.Model.RetainedSelection.selectedPoint, OAI.PlanarL1.FiniteRandom.prob, OAI.PlanarL1.Columns.Model.IncrementStep.update

30. lemma OAI.PlanarL1.Columns.Model.SetSystem.separation_comm line 508
31. def OAI.PlanarL1.Parameters.secondaryChance line 517
32. lemma OAI.PlanarL1.Parameters.secondaryChance_pos line 518
33. lemma OAI.PlanarL1.Parameters.secondaryChance_le_quarter line 519
34. lemma OAI.PlanarL1.Columns.Model.PairGeometry.retained_alternative line 548