MultipointLogFactor.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Smooth logarithmic-coordinate monomials for the multipoint factors. The three monomials in each regularized factor have this form.

def OAI.SLEExactGauge.Multipoint.logFactor line 14
lemma OAI.SLEExactGauge.Multipoint.logFactor_pos line 17
lemma OAI.SLEExactGauge.Multipoint.logFactor_contDiff line 20
lemma OAI.SLEExactGauge.Multipoint.logFactor_spatial_derivative line 34
lemma OAI.SLEExactGauge.Multipoint.logFactor_spatial_second line 49
lemma OAI.SLEExactGauge.Multipoint.logFactor_directional line 78

theorem OAI.SLEExactGauge.Multipoint.logFactor_physical_generator line 117

Source documentation

The source angular generator in actual capacity-two coordinates.

theorem logFactor_physical_generator (κ c r : ℝ) (hκ : 0 < κ)
    (q : ℂ × ℝ) (x : ℝ) :
    (fderiv ℝ (fun q => logFactor κ c r q x) q)
        (physicalLogLoewnerField (Real.sqrt κ*x) q) +
      (1/2 : ℝ)*iteratedDeriv 2 (logFactor κ c r q) x =
    logFactor κ c r q x * κ *
      ((r*(r-greenExponent κ)/2)*(q.1.re-Real.sqrt κ*x)^2+
        (c-r/2)*Real.exp (2*q.1.im)) / (greenLogNormSq κ q x)^2 := by
…

Mentions: OAI.SLEExactGauge.Multipoint.q, OAI.SLEExactGauge.Multipoint.logFactor, OAI.SLEExactGauge.physicalLogLoewnerField, OAI.SLEExactGauge.greenExponent, OAI.SLEExactGauge.greenLogNormSq