MultipointBrownianCoefficient.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The Brownian cross coefficient in the regularized multipoint product, including the singular powers when p < 1.

def OAI.SLEExactGauge.Multipoint.angularCoefficientConstant line 13
lemma OAI.SLEExactGauge.Multipoint.angularCoefficientConstant_pos line 15
lemma OAI.SLEExactGauge.Multipoint.velocity_power_identity line 20
lemma OAI.SLEExactGauge.Multipoint.pair_velocity_power_identity line 26

theorem OAI.SLEExactGauge.Multipoint.angular_pair_absorption line 36

Source documentation

The magnitude of one Brownian cross term is absorbed at its two endpoints, leaving exactly the inverse-regulator interaction cost.

theorem angular_pair_absorption {p δi δj θi θj vi vj ε : ℝ}
    (hp : 0 < p) (hδi : 0 < δi) (hδi1 : δi ≤ 1)
    (hδj : 0 < δj) (hδj1 : δj ≤ 1)
    (hθi : 0 < Real.sin θi) (hθj : 0 < Real.sin θj)
    (hvi : 0 < vi) (hvj : 0 < vj) (hε : 0 < ε) :
    (|angularFactorFirst p δi θi| / angularFactor p δi θi * vi) *
      (|angularFactorFirst p δj θj| / angularFactor p δj θj * vj) ≤
    ε*(damping p δi θi*vi^2+damping p δj θj*vj^2) +
      youngConstant p (angularCoefficientConstant p ^ 2) ε *
        (δi*δj)^(-exponent p)*(vi*vj) := by
…

Mentions: OAI.SLEExactGauge.Multipoint.angularFactorFirst, OAI.SLEExactGauge.Multipoint.angularFactor, OAI.SLEExactGauge.Multipoint.damping, OAI.SLEExactGauge.Multipoint.youngConstant, OAI.SLEExactGauge.Multipoint.angularCoefficientConstant, OAI.SLEExactGauge.Multipoint.exponent