OAI/Analysis/JiangSu/Comparison/FamilyExactLocalSupply.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.FamilyComparison.exact_local_projection line 19
  2. theorem OAI.FamilyComparison.proportional_subprojection line 88
  3. theorem OAI.FamilyComparison.corner_symmetry line 106
  4. def OAI.FamilyComparison.smallHat line 134
  5. def OAI.FamilyComparison.wideHat line 135
  6. lemma OAI.FamilyComparison.smallHat_cont line 136
  7. lemma OAI.FamilyComparison.wideHat_cont line 137
  8. lemma OAI.FamilyComparison.smallHat_bounds line 138
  9. lemma OAI.FamilyComparison.wideHat_bounds line 142
  10. lemma OAI.FamilyComparison.smallHat_supported line 144
  11. lemma OAI.FamilyComparison.wideHat_supported line 150
  12. lemma OAI.FamilyComparison.corner_smallHat_lower line 156
  13. lemma OAI.FamilyComparison.real_smul_mono_nonneg line 174
  14. lemma OAI.FamilyComparison.good_column_projection line 183
  15. theorem OAI.FamilyComparison.orthogonal_insertion line 212