MultipointYoung.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Weighted Young absorption for the pair terms in the multipoint regularized product. The constant depends on the order and SLE parameter, not the two target levels or their current clocks.

def OAI.SLEExactGauge.Multipoint.youngConstant line 12
lemma OAI.SLEExactGauge.Multipoint.youngConstant_pos line 15
lemma OAI.SLEExactGauge.Multipoint.three_factor_young line 22
theorem OAI.SLEExactGauge.Multipoint.weighted_pair_absorption line 63
Source documentation
The factor from the singular angular derivatives is absorbed with coefficient ε at both vertices and a deterministic inverse-regulator cost.
```
theorem weighted_pair_absorption {p C ε D x y z : ℝ} (hp : 0 < p)
    (hC : 0 < C) (hε : 0 < ε) (hD : 0 < D)
    (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) :
    C*D^(-1-eta p)*x^(eta p)*y^(eta p)*z^(1-2*eta p) ≤
      ε*(x+y) + youngConstant p C ε*D^(-exponent p)*z := by
…
```
Mentions: OAI.SLEExactGauge.Multipoint.eta, OAI.SLEExactGauge.Multipoint.youngConstant, OAI.SLEExactGauge.Multipoint.exponent