ContactFlowTime.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The inside-letter flow parameter at the inward contact pivot

theorem OAI.PolycyclicRecognition.contact_flow_time_bound line 12

Source documentation

Conjugating an allowed neighboring step back through the scalar contact dilation leaves only an exponential error proportional to δ.

theorem contact_flow_time_bound (r s δ c η t : ℝ)
    (ht : |t| ≤ Real.exp (((1 + δ) * s + η) * r)) :
    |t * Real.exp (-((1 - (c + 1) * δ) * s * r))| ≤
      Real.exp ((((c + 2) * s) * δ + η) * r) := by
…

theorem OAI.PolycyclicRecognition.contact_flow_time_reconstruction line 23

Source documentation

Applying the contact dilation recovers the original neighboring step.

theorem contact_flow_time_reconstruction (r s δ c t : ℝ) :
    (t * Real.exp (-((1 - (c + 1) * δ) * s * r))) *
      Real.exp ((1 - (c + 1) * δ) * s * r) = t := by
…