OAI/Probability/SLE/Gauge/SerpentineParameters.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SLEExactGauge.Serpentine.fitHeight line 14
2. def OAI.SLEExactGauge.Serpentine.fitRadius line 16
3. def OAI.SLEExactGauge.Serpentine.fitX line 18
4. def OAI.SLEExactGauge.Serpentine.fitY line 21
5. def OAI.SLEExactGauge.Serpentine.fitEntryBound line 24
6. lemma OAI.SLEExactGauge.Serpentine.fit_width_pos line 26
7. lemma OAI.SLEExactGauge.Serpentine.fit_width_eq line 30
8. lemma OAI.SLEExactGauge.Serpentine.fit_width_mul line 35
9. lemma OAI.SLEExactGauge.Serpentine.fitX_eq line 41
10. lemma OAI.SLEExactGauge.Serpentine.fitY_eq line 50
11. lemma OAI.SLEExactGauge.Serpentine.fitX_lower line 59
12. lemma OAI.SLEExactGauge.Serpentine.fitY_lower line 65
13. lemma OAI.SLEExactGauge.Serpentine.fitX_upper line 71
14. lemma OAI.SLEExactGauge.Serpentine.fitY_upper line 80
15. theorem OAI.SLEExactGauge.Serpentine.fit_parameters line 91

    Source documentation

    The fixed numerical parameters satisfy all proved global embedding and local ribbon estimates, with ample strict separation.

    theorem fit_parameters {s : ℝ} (hs : 0 < s) (w : ℂ) (hw : s ≤ w.im)
        {m : ℕ} (hm : 0 < m) :
        50 ≤ fitRadius m ∧ 2 * fitRadius m < fitX s w m ∧
          fitHeight m + 2 * fitRadius m + 1 + 300 * m < fitY s w m ∧
          4 ≤ fitHeight m := by
    …

    Mentions: OAI.SLEExactGauge.Serpentine.fitRadius, OAI.SLEExactGauge.Serpentine.fitX, OAI.SLEExactGauge.Serpentine.fitHeight, OAI.SLEExactGauge.Serpentine.fitY

16. lemma OAI.SLEExactGauge.Serpentine.fitEntryBound_pos line 106
17. lemma OAI.SLEExactGauge.Serpentine.connectorEntry_eq line 110
18. lemma OAI.SLEExactGauge.Serpentine.fit_entry_upper line 115
19. lemma OAI.SLEExactGauge.Serpentine.fit_entry_lower line 126
20. lemma OAI.SLEExactGauge.Serpentine.fit_completion_quadratic line 136