OAI/Probability/InvariantIsing/Cavity/OffsetProductProjection.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Projection moments for the last block with a fixed initial remainder.

  1. theorem OAI.InvariantIsing.offset_product_projection_mean_le line 12
  2. theorem OAI.InvariantIsing.offset_product_last_axes_mean line 46