OAI/Probability/FreeIsing/Critical/ResponseTimeEnergy.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.IsingObservationResponseEnergy.timeEnergyConstant line 16
  2. theorem OAI.Problem367.IsingObservationResponseEnergy.row_bound_le_time_majorant line 20
  3. theorem OAI.Problem367.IsingObservationResponseEnergy.integrable_time_majorant line 42
  4. theorem OAI.Problem367.IsingObservationResponseEnergy.integrable_response_row_time line 50
  5. theorem OAI.Problem367.IsingObservationResponseEnergy.integrable_copy_response_row_time line 77
  6. theorem OAI.Problem367.IsingObservationResponseEnergy.integral_time_majorant line 88
  7. theorem OAI.Problem367.IsingObservationResponseEnergy.lintegral_response_row_time_le line 102
  8. theorem OAI.Problem367.IsingObservationResponseEnergy.lintegral_copy_response_row_time_le line 137
  9. theorem OAI.Problem367.IsingObservationResponseEnergy.tendsto_copy_response_row_time_zero line 154