OAI/Analysis/JiangSu/Comparison/CornerDivision.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectComparison.cfc_projection_zero line 15
  2. lemma OAI.DirectComparison.positiveCut_projection line 29
  3. lemma OAI.DirectComparison.cutoff_projection line 36
  4. theorem OAI.DirectComparison.proportional_subprojection line 48
  5. theorem OAI.DirectComparison.corner_symmetry line 70
  6. lemma OAI.DirectComparison.compress_selfAdjoint line 100
  7. lemma OAI.DirectComparison.compress_norm_le line 107
  8. def OAI.DirectComparison.cornerCFC line 117
  9. lemma OAI.DirectComparison.cornerCFC_eq line 121
  10. lemma OAI.DirectComparison.traceTwoNorm_real_smul line 139
  11. lemma OAI.DirectComparison.traceTwoNorm_pow_sub line 143
  12. lemma OAI.DirectComparison.compression_traceTwoNorm_sub line 165
  13. def OAI.DirectComparison.cornerPolynomialConstant line 183
  14. lemma OAI.DirectComparison.cornerPolynomialConstant_nonneg line 186
  15. lemma OAI.DirectComparison.polynomial_traceTwoNorm_sub line 190
  16. lemma OAI.DirectComparison.corner_polynomial_modulus line 206
  17. lemma OAI.DirectComparison.spectrum_subset_unit_interval line 234
  18. lemma OAI.DirectComparison.cornerCFC_approx line 244
  19. theorem OAI.DirectComparison.moving_corner_modulus line 259