OAI/Probability/SLE/Multipoint/MultipointRegularizer.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

Parameters and the two-ended regularizer in the multipoint radius estimate, September 25 manuscript, Section 3. These bounds are uniform in all target levels; completed factors can therefore be frozen separately.

  1. def OAI.SLEExactGauge.Multipoint.q line 15
  2. def OAI.SLEExactGauge.Multipoint.eta line 17
  3. def OAI.SLEExactGauge.Multipoint.exponent line 19
  4. def OAI.SLEExactGauge.Multipoint.beta line 21
  5. lemma OAI.SLEExactGauge.Multipoint.q_pos line 23
  6. lemma OAI.SLEExactGauge.Multipoint.q_lt_one line 26
  7. lemma OAI.SLEExactGauge.Multipoint.q_lt_p line 31
  8. lemma OAI.SLEExactGauge.Multipoint.eta_pos line 36
  9. lemma OAI.SLEExactGauge.Multipoint.eta_lt_half line 39
  10. lemma OAI.SLEExactGauge.Multipoint.eta_identity line 43
  11. lemma OAI.SLEExactGauge.Multipoint.exponent_eq line 49
  12. lemma OAI.SLEExactGauge.Multipoint.exponent_pos line 59
  13. lemma OAI.SLEExactGauge.Multipoint.beta_pos line 62
  14. lemma OAI.SLEExactGauge.Multipoint.beta_le_one line 65
  15. lemma OAI.SLEExactGauge.Multipoint.twice_exponent_beta_lt line 67
  16. def OAI.SLEExactGauge.Multipoint.regulator line 75

    Source documentation

    The regulator equals one at either endpoint of an active interval.

    def regulator (β U u : ℝ) : ℝ := Real.exp (-β * min u (U - u))
  17. lemma OAI.SLEExactGauge.Multipoint.regulator_zero line 77
  18. lemma OAI.SLEExactGauge.Multipoint.regulator_end line 80
  19. lemma OAI.SLEExactGauge.Multipoint.regulator_pos line 83
  20. lemma OAI.SLEExactGauge.Multipoint.regulator_le_one line 85
  21. lemma OAI.SLEExactGauge.Multipoint.regulator_inv_power_le line 91
  22. lemma OAI.SLEExactGauge.Multipoint.pair_regulator_inv_power_le line 98
  23. lemma OAI.SLEExactGauge.Multipoint.regulator_eq_left line 107
  24. lemma OAI.SLEExactGauge.Multipoint.regulator_eq_right line 111
  25. lemma OAI.SLEExactGauge.Multipoint.regulator_reflect line 115
  26. lemma OAI.SLEExactGauge.Multipoint.regulator_continuous line 118
  27. lemma OAI.SLEExactGauge.Multipoint.integral_regulator line 123

    Source documentation

    Exact total regulator cost, independent of the length of the active clock.

    lemma integral_regulator {β U : ℝ} (hβ : 0 < β) (hU : 0 ≤ U) :
    (∫ u in (0 : ℝ)..U, regulator β U u) =
      2 / β * (1 - Real.exp (-β * U / 2)) := by
…

    Mentions: OAI.SLEExactGauge.Multipoint.regulator

  28. lemma OAI.SLEExactGauge.Multipoint.integral_regulator_le line 158
  29. def OAI.SLEExactGauge.Multipoint.interactionBudget line 165

    Source documentation

    The deterministic pair-interaction allowance obtained by shells of max uᵢ uⱼ; see the interaction integral in the manuscript.

    def interactionBudget (a c : ℝ) : ℝ :=
…
  30. lemma OAI.SLEExactGauge.Multipoint.interactionBudget_pos line 168
  31. lemma OAI.SLEExactGauge.Multipoint.interaction_shell_series line 174
  32. lemma OAI.SLEExactGauge.Multipoint.weighted_shell_sum_le line 188