OAI/Analysis/LiebThirring/FieldLimit.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpLiebThirring.ScalarProof.symmetric_shift_boundary line 23
  2. lemma OAI.SharpLiebThirring.ScalarProof.symmetric_shift_norm_le line 44
  3. lemma OAI.SharpLiebThirring.ScalarProof.symmetric_shift_tendsto_zero line 64
  4. lemma OAI.SharpLiebThirring.ScalarProof.primitive_quadratic_hasDerivAt line 83
  5. lemma OAI.SharpLiebThirring.ScalarProof.primitive_quadratic_deriv_tendsto line 91
  6. lemma OAI.SharpLiebThirring.ScalarProof.primitive_symmetric_shift_zero line 124
  7. lemma OAI.SharpLiebThirring.ScalarProof.primitive_shift_limit line 132

    Source documentation

    The symmetric shift identity, with exactly the cutoff used in the field.

    lemma primitive_shift_limit {σ δ : ℝ} (hσ : σ < 1) (hδ : 0 < δ) (z b : ℝ) :
    Tendsto (fun R : ℝ ↦ fieldNormalization σ * ∫ s in -R..R,
      regularizedPrimitive σ δ ((s - b) ^ 2 + z) - regularizedPrimitive σ δ (s ^ 2))
      atTop (𝓝 (scalarMu σ δ z)) := by
…

    Mentions: OAI.SharpLiebThirring.fieldNormalization, OAI.SharpLiebThirring.regularizedPrimitive, OAI.SharpLiebThirring.scalarMu

  8. lemma OAI.SharpLiebThirring.ScalarProof.derivative_lipschitz_on_positive line 161
  9. lemma OAI.SharpLiebThirring.ScalarProof.primitive_taylor_bound line 185
  10. lemma OAI.SharpLiebThirring.MatrixProof.cfc_scalar_add line 225
  11. lemma OAI.SharpLiebThirring.MatrixProof.spectrum_abs_le_matrix_norm line 233
  12. lemma OAI.SharpLiebThirring.MatrixProof.primitive_cfc_taylor_bound line 242
  13. lemma OAI.SharpLiebThirring.MatrixProof.quadratic_taylor_weight line 277
  14. lemma OAI.SharpLiebThirring.MatrixProof.quadratic_derivative_weight line 303
  15. def OAI.SharpLiebThirring.MatrixProof.quadraticMatrix line 313
  16. def OAI.SharpLiebThirring.MatrixProof.pairedFieldIntegrand line 316
  17. lemma OAI.SharpLiebThirring.MatrixProof.pairedFieldIntegrand_even line 321
  18. lemma OAI.SharpLiebThirring.MatrixProof.quadraticMatrix_hermitian line 327
  19. lemma OAI.SharpLiebThirring.MatrixProof.perturbed_norm_le line 332
  20. lemma OAI.SharpLiebThirring.MatrixProof.pairedFieldIntegrand_bound line 339
  21. lemma OAI.SharpLiebThirring.MatrixProof.continuous_quadratic_cfc line 396
  22. lemma OAI.SharpLiebThirring.MatrixProof.continuous_pairedFieldIntegrand line 404
  23. lemma OAI.SharpLiebThirring.MatrixProof.integrable_pairedFieldIntegrand line 413
  24. def OAI.SharpLiebThirring.MatrixProof.fieldIntegrand line 429
  25. def OAI.SharpLiebThirring.MatrixProof.hermitianField line 433
  26. lemma OAI.SharpLiebThirring.MatrixProof.continuous_fieldIntegrand line 436
  27. lemma OAI.SharpLiebThirring.MatrixProof.cutoff_paired_identity line 442
  28. lemma OAI.SharpLiebThirring.MatrixProof.hermitianField_cutoff_limit line 462