OAI/Probability/InvariantIsing/Cavity/RepeatedBlockTail.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Projection-based radial tails for the physical model on repeated constrained blocks, uniformly in the number of blocks.

  1. theorem OAI.InvariantIsing.repeated_block_projection_axes_mean line 16
  2. theorem OAI.InvariantIsing.repeated_block_tail_probability line 37
  3. theorem OAI.InvariantIsing.repeated_block_tightness line 55