OAI/Geometry/CAT0Fillings/Gradient/Multiplier.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CAT0Fillings.ChartGeometry.gradientFunction_chain line 18
2. lemma OAI.CAT0Fillings.ChartGeometry.gradient_chain_ae line 51
3. lemma OAI.CAT0Fillings.ClosedCalculus.l2_norm_sq line 72
4. lemma OAI.CAT0Fillings.ClosedCalculus.l2_tendsto_zero_of_bound line 76
5. lemma OAI.CAT0Fillings.ClosedCalculus.memLp_smul_bounded line 95
6. def OAI.CAT0Fillings.ClosedCalculus.mulLp line 104
7. lemma OAI.CAT0Fillings.ClosedCalculus.mulLp_ae line 108
8. lemma OAI.CAT0Fillings.ClosedCalculus.mulLp_sub_bound line 112
9. lemma OAI.CAT0Fillings.ClosedCalculus.mulLp_tendsto line 121