OAI/Analysis/AncientFlat/Weighted/WeightedScaling.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.FlatWeighted.scale line 12
2. def OAI.FlatWeighted.scaleValue line 13
3. lemma OAI.FlatWeighted.scale_time_neg line 14
4. lemma OAI.FlatWeighted.sigma_scale_general line 18
5. lemma OAI.FlatWeighted.scale_chart line 27
6. lemma OAI.FlatWeighted.localDomain_scale line 35
7. lemma OAI.FlatWeighted.pullback_scale line 39
8. lemma OAI.FlatWeighted.YBound.scale line 45
9. lemma OAI.FlatWeighted.pdist_unchart line 51
10. lemma OAI.FlatWeighted.unchart_mem_of_near line 59