OAI/Probability/SLE/Gauge/SerpentineConformalGeometry.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A common small displaced experiment disk in normalized half-plane coordinates. Its nearby trace witnesses stay in a controlled conformal patch, and its image stays in one physical conformal-radius disk.

  1. def OAI.SLEExactGauge.Serpentine.conformalExperimentScale line 17
  2. lemma OAI.SLEExactGauge.Serpentine.conformalExperimentScale_bounds line 19
  3. lemma OAI.SLEExactGauge.Serpentine.experiment_patch_subset_compact line 28
  4. lemma OAI.SLEExactGauge.Serpentine.displaced_experiment_dist line 41
  5. lemma OAI.SLEExactGauge.Serpentine.displaced_experiment_subset_patch line 48
  6. lemma OAI.SLEExactGauge.Serpentine.displaced_experiment_near_patch line 53
  7. lemma OAI.SLEExactGauge.Serpentine.conformal_experiment_mesh_cutoff line 64

    Source documentation

    Converting any positive deterministic parameter cutoff into a cutoff proportional to the physical conformal radius.

    lemma conformal_experiment_mesh_cutoff {C a q v : ℝ}
    (hC : 0 < C) (ha : 0 < a) (hq : 0 < q) (w : ℂ) (hwi : w.im ≤ 1)
    (hv : v < (C * q / 2) * (2 * w.im * a)) :
    v / (C * a) < q := by
…
  8. theorem OAI.SLEExactGauge.Serpentine.conformal_experiment_image_subset line 72
  9. theorem OAI.SLEExactGauge.Serpentine.conformal_experiment_restricted_transfer line 99
  10. theorem OAI.SLEExactGauge.Serpentine.uniform_conformal_experiment_restricted_transfer line 142