OAI/Probability/SLE/Geometry/MarkedWitnessReflection.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The actual capacity witness and marked sine angle transform exactly under reflection; no law comparison is needed for the geometric angle bound.

  1. lemma OAI.SLEExactGauge.Serpentine.mirrored_centered_value line 15
  2. lemma OAI.SLEExactGauge.Serpentine.mirrored_centered_sine line 19
  3. lemma OAI.SLEExactGauge.Serpentine.mirrored_marked_sine line 24
  4. lemma OAI.SLEExactGauge.Serpentine.mirrored_front_freshness line 30
  5. lemma OAI.SLEExactGauge.Serpentine.mirrored_ball_surviving_iff line 36
  6. theorem OAI.SLEExactGauge.Serpentine.marked_witness_reflection line 54

    Source documentation

    Every item required by the marked-angle application is reflected with the same capacity time and the negated continuous driver.

    theorem marked_witness_reflection
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U) (T : ℝ≥0)
    (hfresh : ∀ S : ℝ≥0, S < T → γ T ∈ survivingDomain γ S) (w : ℂ) :
    IsCapacityTwoWitness (fun t => -U t) (loewnerMirror ∘ γ)
      (fun t z => loewnerMirror (G t (loewnerMirror z)))
      (fun t z => loewnerMirror (F t (loewnerMirror z))) ∧
    Continuous (fun t => -U t) ∧
    (∀ S : ℝ≥0, S < T → (loewnerMirror ∘ γ) T ∈ survivingDomain (loewnerMirror ∘ γ) S) ∧
    (loewnerMirror (G T (loewnerMirror (loewnerMirror w))) - ((-U T : ℝ) : ℂ)).im /
      ‖loewnerMirror (G T (loewnerMirror (loewnerMirror w))) - ((-U T : ℝ) : ℂ)‖ =
      (G T w - (U T : ℂ)).im / ‖G T w - (U T : ℂ)‖ :=
…

    Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.survivingDomain, OAI.SLEExactGauge.loewnerMirror