OAI/Probability/FreeIsing/Estimates/LiftGram.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.lift_cross_bound_of_operator line 18
  2. theorem OAI.Problem367.lift_sum_gram_bounds line 33
  3. theorem OAI.Problem367.lift_sum_norm_lower_bound line 45
  4. theorem OAI.Problem367.lift_sum_injective line 66
  5. theorem OAI.Problem367.lift_sum_isClosed_range line 77
  6. def OAI.Problem367.liftSumL2 line 89
  7. theorem OAI.Problem367.liftSumL2_apply line 94
  8. theorem OAI.Problem367.liftSumL2_gram_bounds line 97
  9. theorem OAI.Problem367.liftSumL2_norm_lower_bound line 106
  10. theorem OAI.Problem367.norm_liftSumL2_le line 116
  11. theorem OAI.Problem367.liftSumL2_antilipschitz line 127
  12. def OAI.Problem367.liftSumL2EquivRange line 138