OAI/Probability/FreeIsing/Gaussian/TreeResponseRootEnergy.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.GaussianTreeResponseNaturality.finiteRow_fieldEquiv line 15
  2. theorem OAI.Problem367.GaussianTreeResponseNaturality.tsum_finiteRow_sq_fieldEquiv line 31
  3. theorem OAI.Problem367.GaussianTreeResponseNaturality.integral_finiteRow_energy_relabel line 41
  4. theorem OAI.Problem367.GaussianTreeResponseNaturality.integral_finiteRow_tail_relabel line 55
  5. theorem OAI.Problem367.GaussianTreeResponseNaturality.integrable_finiteRow_sq_anyroot line 78
  6. theorem OAI.Problem367.GaussianTreeResponseNaturality.integral_finiteRow_energy_le_anyroot line 99
  7. theorem OAI.Problem367.GaussianTreeResponseNaturality.integral_finiteRow_energy_tail_le_anyroot line 123
  8. theorem OAI.Problem367.GaussianTreeResponseNaturality.norm_finiteRow_le_distance line 151
  9. theorem OAI.Problem367.GaussianTreeResponseNaturality.finiteRow_energy_le_of_strict line 165
  10. theorem OAI.Problem367.GaussianTreeResponseNaturality.finiteRow_energy_tail_le_of_strict line 183
  11. theorem OAI.Problem367.GaussianTreeResponseNaturality.integrable_finiteRow_energy_of_strict line 209