OAI/Probability/FreeIsing/Critical/GlobalEndgame.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.eq_zero_of_ae_small_critical_large_osgood line 12
  2. theorem OAI.Problem367.endpoint_sums_bounded_scale_reduction line 34
  3. structure OAI.Problem367.CriticalSpatialEndpointBounds line 71
  4. theorem OAI.Problem367.inv_le_inv_mul_sqrt line 80
  5. theorem OAI.Problem367.CriticalSpatialEndpointBounds.small_time line 87
  6. def OAI.Problem367.criticalLateCoefficient line 103
  7. theorem OAI.Problem367.CriticalSpatialEndpointBounds.late_time line 107
  8. theorem OAI.Problem367.eq_zero_of_ae_critical_spatial_endpoint_bounds line 133