OAI/Probability/UnimodularPercolation/Deformation/FiniteScale.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Deformed susceptibility, finite-scale estimates and the Riccati contradiction.

  1. theorem OAI.Percolation.deformed_move_of_walk line 22
  2. theorem OAI.Percolation.deformedSusceptibility_delete_interior line 53
  3. theorem OAI.Percolation.selected_retained_product_lower line 68
  4. theorem OAI.Percolation.averagedDeformedSusceptibility_nonneg line 122
  5. theorem OAI.Percolation.deformedKernel_symm line 129
  6. theorem OAI.Percolation.deformed_row_le_root_sum line 137
  7. theorem OAI.Percolation.deformed_norm_le_root_sum line 159
  8. theorem OAI.Percolation.deformed_root_sum_retained line 181
  9. theorem OAI.Percolation.selected_average_lower line 216
  10. theorem OAI.Percolation.riccati_retention_bound line 243
  11. theorem OAI.Percolation.exists_finite_scale_obstruction line 290