OAI/Analysis/KadisonKastler/GraphCutScalarBounds.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Scalar functions for the separated graph cuts

  1. def OAI.KadisonKastler.graphHighInverseScalar line 12

    Source documentation

    The inverse of the complementary graph resolvent, clipped at the cut.

    def graphHighInverseScalar (c r s : ℝ) : ℝ :=
…
  2. theorem OAI.KadisonKastler.graphHighInverseScalar_nonneg line 15
  3. theorem OAI.KadisonKastler.graphHighInverseScalar_bound line 22
  4. theorem OAI.KadisonKastler.graphHighInverseScalar_continuousOn line 34
  5. theorem OAI.KadisonKastler.graphHighInverseScalar_cut_identity line 40
  6. theorem OAI.KadisonKastler.graphScale_exp_square line 57
  7. theorem OAI.KadisonKastler.graphHighInverse_bound_exp line 62