OAI/Analysis/JiangSu/DimensionFunctions/FiniteSpectralIntegralBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.Pureness.positive_cut_zero_of_norm_le line 17
  2. lemma OAI.Pureness.positive_projection_cut_zero line 29
  3. lemma OAI.Pureness.positive_halfline_indicator_integral line 42
  4. theorem OAI.Pureness.finiteSpectralIntegral_le line 49
  5. theorem OAI.Pureness.finiteSpectralIntegral_ne_top line 66
  6. theorem OAI.Pureness.finiteSpectralIntegral_projection line 73
  7. theorem OAI.Pureness.finiteDimensionDistribution_mono line 97
  8. theorem OAI.Pureness.finiteSpectralIntegral_monotone line 106
  9. def OAI.Pureness.finiteContinuousDimension line 121
  10. lemma OAI.Pureness.finiteContinuousDimension_monotone line 125
  11. lemma OAI.Pureness.positiveMap_continuousNNReal_add line 134
  12. lemma OAI.Pureness.finiteContinuousDimension_add_le line 142
  13. lemma OAI.Pureness.finiteContinuousDimension_add_orthogonal line 150
  14. lemma OAI.Pureness.finiteContinuousDimension_support_mono line 159
  15. lemma OAI.Pureness.finiteContinuousDimension_cuts line 169