OAI/Probability/SLE/Gauge/SerpentineArrayEmbedding.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Global normal coordinates for the actual finite serpentine array. Every parameter belongs to a straight or circular piece, and the only possible normal-band contacts are the prescribed common end sections.

  1. def OAI.SLEExactGauge.Serpentine.arrayEnd line 15
  2. lemma OAI.SLEExactGauge.Serpentine.array_pieces line 17
  3. lemma OAI.SLEExactGauge.Serpentine.normalized_width line 61
  4. lemma OAI.SLEExactGauge.Serpentine.normalized_spacing line 66
  5. lemma OAI.SLEExactGauge.Serpentine.normalized_radius line 69
  6. lemma OAI.SLEExactGauge.Serpentine.normal_straight_eq line 72
  7. lemma OAI.SLEExactGauge.Serpentine.normal_circular_eq line 81
  8. lemma OAI.SLEExactGauge.Serpentine.straight_height_bound line 100
  9. lemma OAI.SLEExactGauge.Serpentine.circular_angle_bound line 105
  10. lemma OAI.SLEExactGauge.Serpentine.turn_column_time line 109
  11. theorem OAI.SLEExactGauge.Serpentine.array_normal_injective line 137

    Source documentation

    Normal coordinates over the complete finite array are injective, including the endpoints shared by adjacent straight and circular pieces.

    theorem array_normal_injective {m : ℕ} (hm : 0 < m) (last : ℕ) :
    InjOn (normalRibbon (arraySpine m last) (arrayTangent m last))
      {z : ℂ | z.re ∈ Icc (0 : ℝ) (arrayEnd m last) ∧ |z.im| ≤ 1} := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.normalRibbon, OAI.SLEExactGauge.Serpentine.arraySpine, OAI.SLEExactGauge.Serpentine.arrayTangent, OAI.SLEExactGauge.Serpentine.arrayEnd