OAI/Analysis/KadisonKastler/ModularLogRegularization.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Uniform weighted bounds for logarithmic regularization

Multiplication by s(1-s) removes both endpoint singularities of the regularized modular logarithm. These estimates give strong convergence of its exponential on the dense range of R(1-R).

  1. def OAI.KadisonKastler.regularizedLogScalar line 18

    Source documentation

    Scalar logarithmic generator at a positive regularization scale.

    def regularizedLogScalar (ε s : ℝ) : ℝ :=
…
  2. theorem OAI.KadisonKastler.weighted_log_difference_ordered line 21
  3. theorem OAI.KadisonKastler.weighted_log_difference line 37
  4. theorem OAI.KadisonKastler.weighted_regularizedLog_difference line 50
  5. theorem OAI.KadisonKastler.imaginary_exp_difference line 77
  6. theorem OAI.KadisonKastler.weighted_modularPhase_difference line 92