OAI/Probability/SLE/Multipoint/MultipointInteraction.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The interaction of two active points in the September 25 manuscript, equation mp:interaction-derivative. Centering by a common real driver does not change the kernel, so differentiability of that driver is not needed for the ordinary Loewner-path calculation.

  1. def OAI.SLEExactGauge.Multipoint.interaction line 16
  2. lemma OAI.SLEExactGauge.Multipoint.interaction_eq line 18
  3. lemma OAI.SLEExactGauge.Multipoint.interaction_nonneg line 21
  4. lemma OAI.SLEExactGauge.Multipoint.interaction_center line 24
  5. lemma OAI.SLEExactGauge.Multipoint.interaction_velocity_algebra line 34

    Source documentation

    The real-part identity behind the interaction derivative.

    lemma interaction_velocity_algebra (a : ℝ) (z w : ℂ) :
    (-(a : ℂ) / (z * conj w) + (a : ℂ) / (z * w)).re =
      -2 * a * (z.im / ‖z‖ ^ 2) * (w.im / ‖w‖ ^ 2) := by
…
  6. lemma OAI.SLEExactGauge.Multipoint.interaction_difference_algebra line 42
  7. theorem OAI.SLEExactGauge.Multipoint.interaction_hasDerivWithinAt line 70

    Source documentation

    Two differentiable paths with a common real drift have the source's interaction derivative; the common drift cancels in both differences.

    theorem interaction_hasDerivWithinAt
    {f g : ℝ → ℂ} {S : Set ℝ} {t a b : ℝ}
    (hf : HasDerivWithinAt f ((a : ℂ) / f t + (b : ℂ)) S t)
    (hg : HasDerivWithinAt g ((a : ℂ) / g t + (b : ℂ)) S t)
    (hfi : 0 < (f t).im) (hgi : 0 < (g t).im) (hne : f t ≠ g t) :
    HasDerivWithinAt (fun s => interaction (f s) (g s))
      (-2 * a * ((f t).im / ‖f t‖ ^ 2) * ((g t).im / ‖g t‖ ^ 2)) S t := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.interaction

  8. theorem OAI.SLEExactGauge.Multipoint.interaction_hasDerivAt line 98
  9. theorem OAI.SLEExactGauge.Multipoint.centered_interaction_hasDerivWithinAt line 110

    Source documentation

    The driver can be any real function here: only the two uncentered Loewner paths are differentiated.

    theorem centered_interaction_hasDerivWithinAt
    {f g : ℝ → ℂ} (U : ℝ → ℝ) {S : Set ℝ} {t a : ℝ}
    (hf : HasDerivWithinAt f ((a : ℂ) / (f t - (U t : ℂ))) S t)
    (hg : HasDerivWithinAt g ((a : ℂ) / (g t - (U t : ℂ))) S t)
    (hfi : 0 < (f t).im) (hgi : 0 < (g t).im) (hne : f t ≠ g t) :
    HasDerivWithinAt
      (fun s => interaction (f s - (U s : ℂ)) (g s - (U s : ℂ)))
      (-2 * a * ((f t).im / ‖f t - (U t : ℂ)‖ ^ 2) *
        ((g t).im / ‖g t - (U t : ℂ)‖ ^ 2)) S t := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.interaction

  10. theorem OAI.SLEExactGauge.Multipoint.centered_interaction_hasDerivAt line 142