OAI/Analysis/LiebThirring/FieldPrimitive.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpLiebThirring.MatrixProof.traceGradientMap line 33
2. lemma OAI.SharpLiebThirring.MatrixProof.traceGradientMap_apply line 45
3. def OAI.SharpLiebThirring.MatrixProof.traceGradientNorm line 48
4. lemma OAI.SharpLiebThirring.MatrixProof.traceGradientNorm_nonneg line 50
5. lemma OAI.SharpLiebThirring.MatrixProof.traceGradientMap_bound line 53
6. def OAI.SharpLiebThirring.MatrixProof.quadraticSelfAdjoint line 58
7. lemma OAI.SharpLiebThirring.MatrixProof.quadraticSelfAdjoint_coe line 62
8. lemma OAI.SharpLiebThirring.MatrixProof.quadraticSelfAdjoint_hasFDerivAt line 67
9. def OAI.SharpLiebThirring.MatrixProof.pairedTracePotential line 75

   Source documentation

   Paired trace potential. At s=0 the assigned value is immaterial to its integral.

   def pairedTracePotential (σ δ : ℝ) (C : selfAdjoint (Matrix n n ℂ))
       (B : selfAdjoint (Matrix n n ℂ)) (s : ℝ) : ℝ :=
   …

10. lemma OAI.SharpLiebThirring.MatrixProof.pairedTracePotential_zero line 81
11. lemma OAI.SharpLiebThirring.MatrixProof.pairedTracePotential_hasFDerivAt line 85
12. lemma OAI.SharpLiebThirring.MatrixProof.measurable_pairedTracePotential line 127
13. def OAI.SharpLiebThirring.MatrixProof.fieldGradientEnvelope line 143
14. lemma OAI.SharpLiebThirring.MatrixProof.integrable_fieldGradientEnvelope line 147
15. lemma OAI.SharpLiebThirring.MatrixProof.fieldGradientEnvelope_bound line 153
16. lemma OAI.SharpLiebThirring.MatrixProof.pairedTracePotential_bound line 164
17. lemma OAI.SharpLiebThirring.MatrixProof.integrable_pairedTracePotential line 175
18. def OAI.SharpLiebThirring.MatrixProof.hermitianPotential line 182
19. lemma OAI.SharpLiebThirring.MatrixProof.hermitianPotential_hasFDerivAt line 185
20. lemma OAI.SharpLiebThirring.MatrixProof.hermitianPotential_zero line 226
21. lemma OAI.SharpLiebThirring.MatrixProof.hermitianPotential_radial_hasDerivAt line 230
22. lemma OAI.SharpLiebThirring.MatrixProof.hermitianPotential_radial line 238
23. lemma OAI.SharpLiebThirring.MatrixProof.radial_trace_hasFDerivAt line 262

    Source documentation

    The potential is a genuine trace primitive, not a radial definition whose derivative has been assumed.

    lemma radial_trace_hasFDerivAt {σ δ : ℝ} (hσ : σ < 1) (hδ : 0 < δ)
        (C B : selfAdjoint (Matrix n n ℂ)) :
        HasFDerivAt (fun B : selfAdjoint (Matrix n n ℂ) ↦
          -(∫ t in (0 : ℝ)..1, (trace ((B : Matrix n n ℂ) * hermitianField σ δ C (t • B))).re))
          (-traceGradientMap (hermitianField σ δ C B)) B := by
    …

    Mentions: OAI.SharpLiebThirring.MatrixProof.hermitianField, OAI.SharpLiebThirring.MatrixProof.traceGradientMap

24. def OAI.SharpLiebThirring.MatrixProof.realHermitianComplexify line 279
25. lemma OAI.SharpLiebThirring.MatrixProof.realHermitianComplexify_coe line 282
26. lemma OAI.SharpLiebThirring.MatrixProof.realHermitianComplexify_continuous line 285
27. lemma OAI.SharpLiebThirring.MatrixProof.matrixField_eq_realPart line 288
28. lemma OAI.SharpLiebThirring.MatrixProof.matrixField_continuous line 294