OAI/Geometry/TamingCompatibility/Concentration/RadialDefectFinite.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.unitRadialDefect_zero_of_radius line 19
2. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.smoothUnitDefect_tendsto line 28
3. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.singularDefect_integrable_of_bounds line 46