OAI/Combinatorics/KMedian/Projection/Norm.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.MixedNorm.sq line 15
2. def OAI.MetricKMedian.PCP.MixedNorm.inner line 16
3. def OAI.MetricKMedian.PCP.MixedNorm.norm line 17
4. lemma OAI.MetricKMedian.PCP.MixedNorm.sq_nonneg line 18
5. lemma OAI.MetricKMedian.PCP.MixedNorm.norm_nonneg line 20
6. lemma OAI.MetricKMedian.PCP.MixedNorm.norm_sq line 21
7. lemma OAI.MetricKMedian.PCP.MixedNorm.inner_sq_le line 25
8. lemma OAI.MetricKMedian.PCP.MixedNorm.inner_le_norm line 36
9. lemma OAI.MetricKMedian.PCP.MixedNorm.sq_add line 43
10. lemma OAI.MetricKMedian.PCP.MixedNorm.norm_add line 50
11. lemma OAI.MetricKMedian.PCP.MixedNorm.norm_le_of_sq line 58
12. lemma OAI.MetricKMedian.PCP.MixedNorm.difference_bound line 63