OAI/Analysis/LiebThirring/FieldRegularity.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLiebThirring.MatrixProof.hsSquared_nonneg line 26
  2. def OAI.SharpLiebThirring.MatrixProof.flattenCLM line 29
  3. def OAI.SharpLiebThirring.MatrixProof.unflattenCLM line 35
  4. lemma OAI.SharpLiebThirring.MatrixProof.unflatten_flatten line 42
  5. lemma OAI.SharpLiebThirring.MatrixProof.flatten_norm_sq line 45
  6. lemma OAI.SharpLiebThirring.MatrixProof.cfc_lipschitz_norm line 51
  7. lemma OAI.SharpLiebThirring.MatrixProof.mixed_left_cfc_apply line 77
  8. lemma OAI.SharpLiebThirring.MatrixProof.mixed_right_cfc_apply line 89
  9. lemma OAI.SharpLiebThirring.MatrixProof.real_star_mul_real line 101
  10. lemma OAI.SharpLiebThirring.MatrixProof.trace_cfc_product line 106
  11. lemma OAI.SharpLiebThirring.MatrixProof.trace_taylor_identity line 121
  12. lemma OAI.SharpLiebThirring.MatrixProof.trace_taylor_bound line 151
  13. lemma OAI.SharpLiebThirring.ScalarProof.primitive_lipschitz line 192
  14. lemma OAI.SharpLiebThirring.ScalarProof.scalar_trace_taylor line 202
  15. def OAI.SharpLiebThirring.ScalarProof.secondPrimitive line 219

    Source documentation

    The second scalar primitive used for the matrix trace potential.

    def secondPrimitive (σ δ y : ℝ) : ℝ := ∫ t in 0..y, regularizedPrimitive σ δ t

    Mentions: OAI.SharpLiebThirring.regularizedPrimitive

  16. lemma OAI.SharpLiebThirring.ScalarProof.secondPrimitive_hasDerivAt line 221
  17. def OAI.SharpLiebThirring.MatrixProof.hermitianInclusion line 235
  18. lemma OAI.SharpLiebThirring.MatrixProof.trace_primitive_hasFDerivAt line 241
  19. lemma OAI.SharpLiebThirring.MatrixProof.trace_secondPrimitive_hasFDerivAt line 264
  20. lemma OAI.SharpLiebThirring.ScalarProof.primitive_remainder_lipschitz line 275
  21. def OAI.SharpLiebThirring.MatrixProof.matrixNormBridge line 309
  22. lemma OAI.SharpLiebThirring.MatrixProof.matrixNormBridge_nonneg line 313
  23. lemma OAI.SharpLiebThirring.MatrixProof.cfc_remainder_eq line 315
  24. lemma OAI.SharpLiebThirring.MatrixProof.cfc_remainder_lipschitz line 331
  25. lemma OAI.SharpLiebThirring.MatrixProof.quadraticMatrix_sub line 348
  26. lemma OAI.SharpLiebThirring.MatrixProof.cfc_quadratic_lipschitz line 353
  27. lemma OAI.SharpLiebThirring.MatrixProof.pairedFieldIntegrand_lipschitz_global line 365
  28. def OAI.SharpLiebThirring.MatrixProof.quadraticRemainder line 394
  29. lemma OAI.SharpLiebThirring.MatrixProof.quadraticRemainder_lipschitz_tail line 399
  30. lemma OAI.SharpLiebThirring.MatrixProof.pairedFieldIntegrand_remainder_difference line 441
  31. lemma OAI.SharpLiebThirring.MatrixProof.pairedFieldIntegrand_lipschitz_tail line 449
  32. def OAI.SharpLiebThirring.MatrixProof.fieldLipEnvelope line 471
  33. lemma OAI.SharpLiebThirring.MatrixProof.fieldLipEnvelope_nonneg line 477
  34. lemma OAI.SharpLiebThirring.MatrixProof.integrable_fieldLipEnvelope line 486
  35. lemma OAI.SharpLiebThirring.MatrixProof.pairedFieldIntegrand_lipschitz_envelope line 494
  36. lemma OAI.SharpLiebThirring.MatrixProof.pairedFieldIntegrand_norm_on_ball line 517
  37. lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_lipschitz_bound line 530
  38. lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_locallyLipschitz line 544