OAI/Probability/GammaPassage/EndpointMesh.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Integer endpoint subdivision for Lemma gr:variable-endpoints. Floors use Euclidean division by a positive mesh, including at negative columns.

  1. def OAI.GammaFPP.CrossingBridge.meshFloor line 10
  2. lemma OAI.GammaFPP.CrossingBridge.meshFloor_bounds line 12
  3. lemma OAI.GammaFPP.CrossingBridge.meshFloor_dvd line 20
  4. lemma OAI.GammaFPP.CrossingBridge.meshFloor_of_dvd line 23
  5. lemma OAI.GammaFPP.CrossingBridge.meshFloor_greatest line 26
  6. lemma OAI.GammaFPP.CrossingBridge.meshFloor_refinement line 32
  7. theorem OAI.GammaFPP.CrossingBridge.meshFloor_refinement_count line 40

    Source documentation

    Each finer-level block has at most fifteen intervals; a bound of sixteen also accommodates the initial full coarse interval.

    theorem meshFloor_refinement_count (x d D : ℤ) (hd : 0 < d) (hD : 0 < D)
    (hdD : d ∣ D) (hratio : D ≤ 16*d) :
    ∃ n : ℕ, n < 16 ∧ meshFloor x D+(n : ℤ)*d=meshFloor x d := by
…

    Mentions: OAI.GammaFPP.CrossingBridge.meshFloor

  8. def OAI.GammaFPP.CrossingBridge.endpointColumn line 53
  9. lemma OAI.GammaFPP.CrossingBridge.endpointColumn_last line 55
  10. lemma OAI.GammaFPP.CrossingBridge.endpointColumn_step line 59
  11. lemma OAI.GammaFPP.CrossingBridge.gridMesh_dvd_of_le line 65
  12. lemma OAI.GammaFPP.CrossingBridge.endpointColumn_mono line 70
  13. def OAI.GammaFPP.CrossingBridge.entranceColumn line 76
  14. def OAI.GammaFPP.CrossingBridge.exitColumn line 78
  15. lemma OAI.GammaFPP.CrossingBridge.entranceColumn_span line 80
  16. lemma OAI.GammaFPP.CrossingBridge.exitColumn_span line 87
  17. lemma OAI.GammaFPP.CrossingBridge.entranceColumn_dvd line 94
  18. lemma OAI.GammaFPP.CrossingBridge.exitColumn_dvd line 97