OAI/Analysis/KadisonKastler/SmoothingHeightSequence.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Positive smoothing heights tending to the boundary

  1. def OAI.KadisonKastler.smoothingHeight line 14
  2. theorem OAI.KadisonKastler.smoothingHeight_pos line 16
  3. theorem OAI.KadisonKastler.smoothingHeight_le line 19
  4. theorem OAI.KadisonKastler.smoothingHeight_tendsto line 25
  5. theorem OAI.KadisonKastler.poissonBoundaryApprox_smoothingHeight_tendsto line 33
  6. theorem OAI.KadisonKastler.poissonBoundaryApprox_star_smoothingHeight_tendsto line 41
  7. theorem OAI.KadisonKastler.norm_poissonBoundaryApprox_smoothingHeight_le_two line 50