OAI/Probability/SLE/Gauge/PrescribedCellNormalization.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The lower-bound grid uses doubled cell radii around each sampled point. These identities match its threshold with the exact gauge weights.

  1. lemma OAI.SLEExactGauge.Multipoint.cell_subset_ball_at_member line 15
  2. lemma OAI.SLEExactGauge.Multipoint.prescribed_lower_threshold line 26
  3. lemma OAI.SLEExactGauge.Multipoint.prescribed_lower_radius line 34