OAI/Geometry/IsometricImmersion/Energy/FiniteProductL2.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Analytic.finite_product_one_factor_bound line 14
2. theorem OAI.SmoothLocal.Analytic.finite_product_eLpNorm_two line 28
3. theorem OAI.SmoothLocal.Analytic.finite_product_eLpNorm_two_of_aestronglyMeasurable line 44
4. theorem OAI.SmoothLocal.Analytic.finite_product_memLp_two line 69