OAI/Probability/SLE/Multipoint/MultipointFactorBranches.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Exact first-half and second-half formulas for the active multipoint factor. The change of formula at the midpoint has no jump.

  1. def OAI.SLEExactGauge.Multipoint.logFactorClock line 15

    Source documentation

    The source clock in logarithmic capacity-two coordinates.

    def logFactorClock (κ : ℝ) (z : ℂ × ℝ) : ℝ := κ / 4 * (z.2-z.1.im)
  2. def OAI.SLEExactGauge.Multipoint.factorActivationScale line 17
  3. lemma OAI.SLEExactGauge.Multipoint.factorActivationScale_pos line 19
  4. lemma OAI.SLEExactGauge.Multipoint.first_branch_regulator line 22
  5. lemma OAI.SLEExactGauge.Multipoint.second_branch_regulator line 30
  6. lemma OAI.SLEExactGauge.Multipoint.first_branch_regulator_eq line 38
  7. lemma OAI.SLEExactGauge.Multipoint.second_branch_regulator_eq line 44
  8. lemma OAI.SLEExactGauge.Multipoint.regularizedLogFactor_normalized line 50
  9. lemma OAI.SLEExactGauge.Multipoint.first_branch_factor_eq line 69
  10. lemma OAI.SLEExactGauge.Multipoint.second_branch_factor_eq line 77
  11. lemma OAI.SLEExactGauge.Multipoint.first_branch_regulator_le_one line 85
  12. lemma OAI.SLEExactGauge.Multipoint.second_branch_regulator_le_one line 91
  13. lemma OAI.SLEExactGauge.Multipoint.first_branch_factor_pos line 98
  14. lemma OAI.SLEExactGauge.Multipoint.second_branch_factor_pos line 104
  15. lemma OAI.SLEExactGauge.Multipoint.branch_midpoint_eq line 110
  16. lemma OAI.SLEExactGauge.Multipoint.factorExponent_pos line 118
  17. lemma OAI.SLEExactGauge.Multipoint.first_branch_activation_le line 126

    Source documentation

    Activation changes the inactive factor one downward to the first smooth branch.

    lemma first_branch_activation_le (κ β a U : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (z : ℂ × ℝ) (x : ℝ) (hU : 0 ≤ U) (hu : logFactorClock κ z-a = 0) :
    factorActivationScale κ a *
      regularizedLogFactor κ (Real.exp (β*a)) (-β) z x ≤ 1 := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.logFactorClock, OAI.SLEExactGauge.Multipoint.factorActivationScale, OAI.SLEExactGauge.Multipoint.regularizedLogFactor

  18. lemma OAI.SLEExactGauge.Multipoint.second_branch_completion_jump line 135

    Source documentation

    Completion freezes at the angle-independent lower bound.

    lemma second_branch_completion_jump (κ β a U : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (z : ℂ × ℝ) (x : ℝ) (hU : 0 ≤ U) (hu : logFactorClock κ z-a = U) :
    Real.exp (greenExponent κ/2*U)/3 ≤ factorActivationScale κ a *
      regularizedLogFactor κ (Real.exp (-β*(U+a))) β z x := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.logFactorClock, OAI.SLEExactGauge.greenExponent, OAI.SLEExactGauge.Multipoint.factorActivationScale, OAI.SLEExactGauge.Multipoint.regularizedLogFactor