OAI/Geometry/TamingCompatibility/DifferentialForms/UnitTransversePairProduct.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.transversePairKernel_nonneg line 23
2. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.transversePairKernel_bound line 30
3. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.transversePairKernel_integrable line 62
4. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.separating_probability_transverse_product_limit line 73
5. lemma OAI.TamingCompatibility.integral_sqrt_mul_sqrt_tendsto_eventually line 99
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.separating_current_angular_transverse_limit line 137