OAI/Probability/SLE/Multipoint/MultipointAngular.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

The angular generator calculation for the regularized factors of the fixed-order multipoint radius estimate. The angular clock has generator (1/2)∂² + ((1-p)/2) cot(θ) ∂, with p = 4a-1.

  1. def OAI.SLEExactGauge.Multipoint.sinePower line 14
  2. def OAI.SLEExactGauge.Multipoint.sinePowerFirst line 16
  3. def OAI.SLEExactGauge.Multipoint.sinePowerSecond line 18
  4. lemma OAI.SLEExactGauge.Multipoint.sinePower_hasDerivAt line 21
  5. lemma OAI.SLEExactGauge.Multipoint.sinePowerFirst_hasDerivAt line 27
  6. def OAI.SLEExactGauge.Multipoint.sineGenerator line 43
  7. lemma OAI.SLEExactGauge.Multipoint.sineGenerator_eq line 46
  8. lemma OAI.SLEExactGauge.Multipoint.sineGenerator_eigen line 59
  9. def OAI.SLEExactGauge.Multipoint.angularFactor line 65
  10. def OAI.SLEExactGauge.Multipoint.damping line 67
  11. def OAI.SLEExactGauge.Multipoint.negativeDrift line 69
  12. def OAI.SLEExactGauge.Multipoint.driftAllowance line 71
  13. lemma OAI.SLEExactGauge.Multipoint.negativeDrift_pos line 73
  14. lemma OAI.SLEExactGauge.Multipoint.driftAllowance_pos line 76
  15. lemma OAI.SLEExactGauge.Multipoint.angularFactor_pos line 82
  16. lemma OAI.SLEExactGauge.Multipoint.regularized_generator line 88

    Source documentation

    Exact algebraic drift before estimating its negative singular term.

    lemma regularized_generator {p δ σ θ : ℝ} (hθ : 0 < Real.sin θ) :
    sineGenerator p p θ + δ*sineGenerator p (q p) θ +
      (p/2)*angularFactor p δ θ + δ*σ*(1+sinePower (q p) θ) =
    δ*(p/2 + (p-q p)*(1+q p)/2*sinePower (q p) θ -
      negativeDrift p*sinePower (q p-2) θ + σ*(1+sinePower (q p) θ)) := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.sineGenerator, OAI.SLEExactGauge.Multipoint.q, OAI.SLEExactGauge.Multipoint.angularFactor, OAI.SLEExactGauge.Multipoint.sinePower, OAI.SLEExactGauge.Multipoint.negativeDrift

  17. lemma OAI.SLEExactGauge.Multipoint.regularized_bracket_le line 97
  18. lemma OAI.SLEExactGauge.Multipoint.angularFactor_ge_delta line 113
  19. lemma OAI.SLEExactGauge.Multipoint.angularFactor_le_three line 120
  20. lemma OAI.SLEExactGauge.Multipoint.angularFactor_endpoint_bounds line 129
  21. def OAI.SLEExactGauge.Multipoint.angularFactorFirst line 134
  22. lemma OAI.SLEExactGauge.Multipoint.angularFactor_hasDerivAt line 137
  23. lemma OAI.SLEExactGauge.Multipoint.angularFactorFirst_bound line 143
  24. lemma OAI.SLEExactGauge.Multipoint.normalized_angularFactorFirst_bound line 168

    Source documentation

    The singular angular derivative is controlled by the damping term. The exponent is chosen so that eta * (q - 2) = q - 1.

    lemma normalized_angularFactorFirst_bound {p δ θ : ℝ} (hp : 0 < p)
    (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hθ : 0 < Real.sin θ) :
    |angularFactorFirst p δ θ| / angularFactor p δ θ ≤
      (p+q p)*3^(eta p)*δ^(-1-eta p)*(damping p δ θ)^(eta p) := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.angularFactorFirst, OAI.SLEExactGauge.Multipoint.angularFactor, OAI.SLEExactGauge.Multipoint.q, OAI.SLEExactGauge.Multipoint.eta, OAI.SLEExactGauge.Multipoint.damping

  25. def OAI.SLEExactGauge.Multipoint.driftThreshold line 205
  26. lemma OAI.SLEExactGauge.Multipoint.driftThreshold_pos line 208
  27. lemma OAI.SLEExactGauge.Multipoint.driftThreshold_lt_one line 212
  28. lemma OAI.SLEExactGauge.Multipoint.driftThreshold_identity line 225
  29. lemma OAI.SLEExactGauge.Multipoint.regularized_drift_bound line 238

    Source documentation

    The negative singular part absorbs the bounded drift at small angles; away from the endpoints the denominator supplies a fixed lower bound.

    lemma regularized_drift_bound {p δ σ θ : ℝ} (hp : 0 < p)
    (hδ : 0 < δ) (hσ : σ ≤ 1) (hθ : 0 < Real.sin θ) :
    δ / angularFactor p δ θ *
      (p/2 + (p-q p)*(1+q p)/2*sinePower (q p) θ -
        negativeDrift p*sinePower (q p-2) θ + σ*(1+sinePower (q p) θ)) ≤
    (driftAllowance p * driftThreshold p ^ (-p))*δ -
      (negativeDrift p/2)*damping p δ θ := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.angularFactor, OAI.SLEExactGauge.Multipoint.q, OAI.SLEExactGauge.Multipoint.sinePower, OAI.SLEExactGauge.Multipoint.negativeDrift, OAI.SLEExactGauge.Multipoint.driftAllowance, OAI.SLEExactGauge.Multipoint.driftThreshold, OAI.SLEExactGauge.Multipoint.damping