OAI/Combinatorics/EditApproximation/Refinement/PhysicalLocalOnlineKeys.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

Online random streams have bounded physical keys. The embedding of the complete representative table is used only in the proof of the law; the local program requests the scale and rounded center directly.

  1. theorem OAI.EditApproximation.physicalScaleIndex_get line 21
  2. def OAI.EditApproximation.physicalOnlineRawKey line 31
  3. theorem OAI.EditApproximation.physicalOnlineRawKey_injective line 39
  4. def OAI.EditApproximation.physicalLocalOnlineBandG line 53
  5. theorem OAI.EditApproximation.physicalLocalOnlineBandG_positive line 59
  6. theorem OAI.EditApproximation.physicalLocalOnlineBandG_on_key line 64
  7. def OAI.EditApproximation.physicalLocalOnlineMass line 80
  8. instance OAI.EditApproximation.physicalLocalOnlineMass_nezero line 85
  9. theorem OAI.EditApproximation.physicalLocalOnlineMass_on_key line 91
  10. abbrev OAI.EditApproximation.PhysicalLocalOnlineDraw line 104
  11. def OAI.EditApproximation.physicalLocalOnlineDrawLaw line 108
  12. theorem OAI.EditApproximation.physicalLocalOnlineDrawLaw_restrict line 116

    Source documentation

    The bounded-key independent arrays restrict to the original online coordinates with exactly their prescribed finite uniform laws.

    theorem physicalLocalOnlineDrawLaw_restrict (R T exponent H : ℕ) (tau : ℚ)
    (hsize : source.length + target.length ≤ N) (hP : 66 ≤ P) (hF : 1 ≤ F) (hA : 1 ≤ A)
    (hseed : ∀ state, stateEditCost (physicalSource source state.1) target state.2 ≤ U state ∧
      (U state : ℚ) ≤ A * stateEditCost (physicalSource source state.1) target state.2) :
    (physicalLocalOnlineDrawLaw source target U N P F A R T exponent H tau).map
      (fun draw (key : PhysicalOnlineKey source target U N P F A) t =>
        Fin.cast (physicalLocalOnlineMass_on_key source target U N P F A T exponent H tau
          hsize hP hF hA hseed key)
          (draw (physicalOnlineRawKey source target U N P F A key) t)) =
      Measure.pi (fun key : PhysicalOnlineKey source target U N P F A =>
        Measure.pi (fun _ : Fin R => (PMF.uniformOfFintype (Fin (optimizerTriangularMass
          (physicalProgramBandK source target U N P F A T exponent H tau key.1 key.2)))).toMeasure)) := by
…

    Mentions: OAI.EditApproximation.stateEditCost, OAI.EditApproximation.physicalSource, OAI.EditApproximation.physicalLocalOnlineDrawLaw, OAI.EditApproximation.PhysicalOnlineKey, OAI.EditApproximation.physicalLocalOnlineMass_on_key, OAI.EditApproximation.physicalOnlineRawKey, OAI.EditApproximation.optimizerTriangularMass, OAI.EditApproximation.physicalProgramBandK