OAI/Combinatorics/PlanarL1/SecondaryStep.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PlanarL1.Columns.Model.BData.isOrdinary line 15
  2. def OAI.PlanarL1.Columns.Model.BData.comparison line 19
  3. def OAI.PlanarL1.Columns.Model.BData.offset line 25
  4. def OAI.PlanarL1.Columns.Model.BData.orientation line 29
  5. lemma OAI.PlanarL1.Columns.Model.BData.orientation_unit line 33
  6. lemma OAI.PlanarL1.Columns.Model.BData.comparison_convert line 38
  7. def OAI.PlanarL1.Columns.Model.OrdinaryData.conversion line 53

    Source documentation

    The affine conversion constants, without manufacturing a point source.

    noncomputable def conversion (M : Model (k+1)) (c η : ℝ) (hη : |η|=1) : OrdinaryData M where
…

    Mentions: OAI.PlanarL1.Columns.Model, OAI.PlanarL1.Columns.Model.OrdinaryData

  8. def OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.secondaryChart line 68

    Source documentation

    Exact shallow-secondary ordinary chart: c+η(pc+R/20−Q_F).

    noncomputable def secondaryChart (A : R.AtomSource a) (c η : ℝ) (hη : |η|=1)
    (p : M.Point J root → ℝ) (α : Noise (n := k+1)) (pc radius : ℝ) : OrdinaryData M :=
…

    Mentions: OAI.PlanarL1.Columns.Model.Point.RadialTree.Noise, OAI.PlanarL1.Columns.Model.Point.RadialTree.radius, OAI.PlanarL1.Columns.Model.OrdinaryData

  9. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.AtomSource.secondaryChart_value line 73
  10. def OAI.PlanarL1.Columns.Model.Point.RadialTree.secondaryChart line 84
  11. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.secondaryChart_value line 89
  12. lemma OAI.PlanarL1.Columns.Model.Point.RadialTree.secondaryChart_contains line 103
  13. def OAI.PlanarL1.Columns.Model.OrderedData.secondaryInstall line 116

    Source documentation

    The source ordered-support branch, including the old affine chart conversion. The auxiliary field is zero and the circular order reverses exactly when η is negative.

    noncomputable def secondaryInstall {I : Set ℝ} (hI : IsClosed I) (hc : I.OrdConnected)
    (L : M.Field I 1) (a b : Fin (k+1)) (ho : L.OrderedFrom a b)
    (c η pc radius α : ℝ) (_hη : |η|=1) : OrderedData M :=
…

    Mentions: OAI.PlanarL1.Columns.Model.OrderedData

  14. lemma OAI.PlanarL1.Columns.Model.OrderedData.secondaryInstall_value line 121
  15. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.namedReplacement_cases line 142
  16. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.namedReplacement_bound line 153
  17. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.namedReplacement_congr_zero line 163
  18. def OAI.PlanarL1.Columns.Model.SecondaryCell.choose line 177
  19. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.choose_spec line 188
  20. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.choose_none line 203
  21. lemma OAI.PlanarL1.Columns.Model.SecondaryCell.choose_switch line 212
  22. lemma OAI.PlanarL1.Columns.Model.BState.represents_named line 236
  23. structure OAI.PlanarL1.Columns.Model.BState.SecondaryStep line 246

    Source documentation

    One kept group's literal secondary clipping. Only the geometric admission, seed and eligibility data enter; every new chart below is constructed from the winning formula, not postulated.

    structure SecondaryStep (S : BState M κ lam Ω μ) (J : Set ℝ) (root : Fin (k+1)) where
…

    Mentions: OAI.PlanarL1.Columns.Model.BState

  24. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.data line 290
  25. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.comparison line 291
  26. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.old line 292
  27. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.supportValue line 293
  28. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.old_lipschitz line 295
  29. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.support_lipschitz line 297
  30. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.compact_band line 300
  31. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.old_agreement line 302
  32. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.patch line 318
  33. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.input line 327
  34. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.replacement line 328
  35. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.named line 330
  36. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.shield line 332
  37. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.shieldConstant line 334
  38. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.shield_lipschitz line 337
  39. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.orderedChart line 351
  40. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.newData line 355
  41. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.newLabels line 361
  42. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.choose line 366
  43. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.patch_inside line 369
  44. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.chosen_description line 379
  45. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.unchosen line 469
  46. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.choose_switch line 498
  47. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.apply line 504

    Source documentation

    Actual one-group secondary installation with old identifiers retained and fresh ordinary, ordered, and rebased height chart data supplied by their formulas.

    noncomputable def apply [SFinite μ] : BState M κ lam (Ω × Bool) (μ.prod Threshold.fair) :=
…

    Mentions: OAI.PlanarL1.Columns.Model.BState, OAI.PlanarL1.Threshold.fair

  48. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.apply_sets line 511
  49. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.point_old line 526
  50. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.replacement_lipschitz line 531
  51. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.replacement_frontier line 535
  52. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullReplacement line 554

    Source documentation

    The literal clamped proposal, extended by the old comparison on the rest of the old band. This is the extension whose finite maximum is required for simultaneous overlapping secondary groups.

    noncomputable def fullReplacement (i : Fin (k+1)) (H : U.data.band) : ℝ :=
…
  53. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullReplacement_inside line 559
  54. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullReplacement_outside line 563
  55. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullReplacement_ge line 567
  56. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullReplacement_vertical line 574
  57. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullReplacement_switch line 613
  58. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullField line 627
  59. def OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullNamed line 644
  60. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullNamed_value line 649
  61. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullNamed_switch line 656
  62. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullNamed_zero line 668
  63. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullNamed_choice line 690
  64. lemma OAI.PlanarL1.Columns.Model.BState.SecondaryStep.fullReplacement_scaled_vertical line 714