OAI/Probability/SLE/Mass/GridMassOverlap.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Summing physical grid-cell masses costs only the fixed overlap constant, independently of the radius and of the containing compact set.

  1. lemma OAI.SLEExactGauge.grid_indicator_sum_le line 14
  2. lemma OAI.SLEExactGauge.grid_mass_sum_le line 40