OAI/Probability/SLE/Geometry/RoundedConnectorGeometry.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Uniform local geometry of the actual rounded connector.

  1. lemma OAI.SLEExactGauge.Serpentine.shifted_lipschitz line 14
  2. lemma OAI.SLEExactGauge.Serpentine.lowConnectorTangent_lipschitz line 20
  3. lemma OAI.SLEExactGauge.Serpentine.lowConnector_initial line 41
  4. lemma OAI.SLEExactGauge.Serpentine.lowConnector_normal_patch_bounds line 51
  5. lemma OAI.SLEExactGauge.Serpentine.quarterTangent_nonneg line 70
  6. lemma OAI.SLEExactGauge.Serpentine.lowConnectorTangent_nonneg line 85
  7. lemma OAI.SLEExactGauge.Serpentine.lowConnector_taxicab_speed line 115
  8. lemma OAI.SLEExactGauge.Serpentine.lowConnector_chord_bound line 125
  9. theorem OAI.SLEExactGauge.Serpentine.lowConnector_normal_injective line 159

    Source documentation

    The normal ribbon around the whole low connector is embedded.

    theorem lowConnector_normal_injective {H r X : ℝ} (hr : 50 ≤ r) (hX : 2 * r < X) :
    InjOn (normalRibbon (lowConnector H r X) (lowConnectorTangent H r X))
      {z : ℂ | 0 ≤ z.re ∧ |z.im| ≤ 1} := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.normalRibbon, OAI.SLEExactGauge.Serpentine.lowConnector, OAI.SLEExactGauge.Serpentine.lowConnectorTangent