OAI/Probability/FreeIsing/Energy/NormalizedInfiniteTimeEnergy.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Problem367.NormalizedInfiniteTimeEnergy.observation line 18
  2. def OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow line 22
  3. def OAI.Problem367.NormalizedInfiniteTimeEnergy.infiniteRow line 27
  4. lemma OAI.Problem367.NormalizedInfiniteTimeEnergy.measurable_observation line 33
  5. lemma OAI.Problem367.NormalizedInfiniteTimeEnergy.measurable_finiteRow line 45
  6. lemma OAI.Problem367.NormalizedInfiniteTimeEnergy.measurable_infiniteRow line 58
  7. lemma OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_eq_normalizedCovariance line 66
  8. lemma OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_eq_zero line 82
  9. lemma OAI.Problem367.NormalizedInfiniteTimeEnergy.tsum_finiteRow_sq line 89
  10. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.finiteRow_tendsto_ae line 104
  11. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.lintegral_infiniteRow_le_of_finite line 128
  12. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.lintegral_infiniteRow_le line 168
  13. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.row_energy_integrable line 211
  14. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.ae_path_row_energy_integrable line 236
  15. theorem OAI.Problem367.NormalizedInfiniteTimeEnergy.integral_mean_row_energy_le line 254