OAI/Geometry/TamingCompatibility/Hodge/HodgeGammaLinearTransfer.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.KernelTransfer.sandwich line 16
2. lemma OAI.TamingCompatibility.KernelTransfer.sandwich_apply line 22
3. lemma OAI.TamingCompatibility.KernelTransfer.sandwich_integrable line 26
4. lemma OAI.TamingCompatibility.KernelTransfer.integral_sandwich line 31
5. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingCoordinate_gamma_integrable line 52
6. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingPatch_gamma_integrable line 69
7. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.partitionLeading_gamma_integrable line 91
8. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingMatrix_gamma_integrable line 100
9. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.leadingMatrix_gamma line 112
10. lemma OAI.TamingCompatibility.ManifoldKernelExtension.push_smul line 141
11. lemma OAI.TamingCompatibility.ManifoldKernelExtension.push_integrable line 148
12. lemma OAI.TamingCompatibility.ManifoldKernelExtension.integral_push line 157
13. def OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gammaPartitionLeading line 174
14. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gammaPartitionLeading_apply line 178
15. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.gammaPartitionLeading_support line 203
16. lemma OAI.TamingCompatibility.GeometricHilbert.GeometricNormalCharts.globalLeading_gamma_sum line 221