OAI/Analysis/AncientFlat/Weighted/WeightedRescaling.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FlatWeighted.radius line 10
2. lemma OAI.FlatWeighted.one_le_radius line 12
3. lemma OAI.FlatWeighted.radius_pos line 16
4. lemma OAI.FlatWeighted.norm_le_radius line 18
5. lemma OAI.FlatWeighted.sigma_scale line 22
6. def OAI.FlatWeighted.scaledSource line 27
7. lemma OAI.FlatWeighted.scaledSource_eq_pullback line 29
8. lemma OAI.FlatWeighted.YBound.scaled_pointwise line 34
9. lemma OAI.FlatWeighted.normalizedSource_eq_scaled line 43