OAI/Probability/SLE/Mass/MassGridCutoffs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Compact spatial test functions adapted to the mass grid. A fixed compact cutoff keeps every enlarged grid cell inside the open half-plane.

  1. lemma OAI.SLEExactGauge.Multipoint.exists_unit_compact_test_cutoff line 15
  2. def OAI.SLEExactGauge.Multipoint.massGridBump line 22
  3. def OAI.SLEExactGauge.Multipoint.massGridCutoff line 25
  4. lemma OAI.SLEExactGauge.Multipoint.massGridBump_bounds line 28
  5. lemma OAI.SLEExactGauge.Multipoint.massGridBump_eq_one line 32
  6. lemma OAI.SLEExactGauge.Multipoint.massGridBump_eq_zero line 37
  7. lemma OAI.SLEExactGauge.Multipoint.massGridCutoff_bounds line 44
  8. lemma OAI.SLEExactGauge.Multipoint.massGridCutoff_eq_one line 51
  9. lemma OAI.SLEExactGauge.Multipoint.massGridCutoff_support line 57
  10. lemma OAI.SLEExactGauge.Multipoint.massGridCutoff_common_support line 69
  11. lemma OAI.SLEExactGauge.Multipoint.massGridCutoff_sum_bound line 81