OAI/Analysis/LiebThirring/FieldFlow.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.ODEProof.radialCutoff line 27

   Source documentation

   A radial auxiliary cutoff; its lack of smoothness is harmless because only Lipschitz regularity is needed for the flow and barriers.

   def radialCutoff {E : Type u158} [NormedAddCommGroup E] (R : ℝ) (x : E) : ℝ :=
   …

2. lemma OAI.SharpLiebThirring.ODEProof.radialCutoff_nonneg line 30
3. lemma OAI.SharpLiebThirring.ODEProof.radialCutoff_le_one line 32
4. lemma OAI.SharpLiebThirring.ODEProof.radialCutoff_eq_one line 34
5. lemma OAI.SharpLiebThirring.ODEProof.radialCutoff_eq_zero line 38
6. lemma OAI.SharpLiebThirring.ODEProof.radialCutoff_lipschitz line 42
7. lemma OAI.SharpLiebThirring.ODEProof.bounded_lipschitz_radial_cutoff line 51
8. lemma OAI.SharpLiebThirring.MatrixFlow.cfc_isolated_row line 127
9. def OAI.SharpLiebThirring.MatrixFlow.sourceField line 169
10. lemma OAI.SharpLiebThirring.MatrixFlow.sourceField_locallyLipschitz line 172
11. def OAI.SharpLiebThirring.MatrixFlow.complexUnitary line 193
12. lemma OAI.SharpLiebThirring.MatrixFlow.complexify_conj line 197
13. lemma OAI.SharpLiebThirring.MatrixFlow.complexify_symConj line 204
14. lemma OAI.SharpLiebThirring.MatrixFlow.sourceField_equivariant line 213
15. def OAI.SharpLiebThirring.MatrixFlow.matrixEntry line 232
16. lemma OAI.SharpLiebThirring.MatrixFlow.matrixEntry_apply line 235
17. lemma OAI.SharpLiebThirring.MatrixFlow.matrixField_tendsto line 237
18. lemma OAI.SharpLiebThirring.MatrixFlow.matrixField_isolated_coordinate line 250
19. def OAI.SharpLiebThirring.MatrixFlow.scalarDiag line 284
20. lemma OAI.SharpLiebThirring.MatrixFlow.coordinate_mu_locallyLipschitz line 296