OAI/Geometry/TamingCompatibility/DifferentialForms/HermitianCorrectedLower.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.logForm line 24
2. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.sqrtForm line 33
3. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.cutoff_one_near line 42
4. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.logForm_trace_lower line 50
5. lemma OAI.TamingCompatibility.GeometricHilbert.Hermitian.sqrtForm_trace_lower line 97
6. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.logSource line 161
7. def OAI.TamingCompatibility.GeometricHilbert.Hermitian.sqrtSource line 170