OAI/Probability/FreeIsing/Energy/EnergyLimit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.hasSum_of_uniform_energy_tails line 12
  2. theorem OAI.Problem367.uniform_energy_tails_of_two_stage_bound line 43
  3. theorem OAI.Problem367.norm_sq_residual_of_testing line 63
  4. theorem OAI.Problem367.tendsto_of_testing_and_energy line 69
  5. theorem OAI.Problem367.norm_sq_sum_of_pairwise_orthogonal line 83
  6. theorem OAI.Problem367.hasSum_of_orthogonal_testing_and_energy line 98
  7. theorem OAI.Problem367.hasSum_of_uniform_energy_tails_and_testing line 111