OAI/Geometry/IsometricImmersion/Caps/EnergyCauchySchwarz.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SmoothLocal.Hyperbolic.integral_square_eq_L2_norm_square line 12
2. theorem OAI.SmoothLocal.Hyperbolic.sqrt_integral_square_eq_L2_norm line 23
3. theorem OAI.SmoothLocal.Hyperbolic.integral_product_abs_le_sqrt_squares line 28