OAI/Analysis/WeakInfiniteness/Clipping.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.WeakPureInfiniteness.clipFunction line 26
  2. lemma OAI.WeakPureInfiniteness.continuous_clipFunction line 28
  3. lemma OAI.WeakPureInfiniteness.clipFunction_nonneg line 35
  4. lemma OAI.WeakPureInfiniteness.clipFunction_le_one line 39
  5. def OAI.WeakPureInfiniteness.cstarClip line 43
  6. lemma OAI.WeakPureInfiniteness.star_mul_function_square line 45
  7. lemma OAI.WeakPureInfiniteness.clip_scalar_norm line 59
  8. lemma OAI.WeakPureInfiniteness.norm_cstarClip_le line 78
  9. lemma OAI.WeakPureInfiniteness.clip_scalar_difference_bound line 88
  10. lemma OAI.WeakPureInfiniteness.sub_cstarClip line 110
  11. lemma OAI.WeakPureInfiniteness.norm_sub_cstarClip_le line 116
  12. lemma OAI.WeakPureInfiniteness.map_cstarClip line 133