OAI/Analysis/AffineBernstein/TubeCompactIntegral.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.AffineBernstein.integrable_joint_compact_mul line 16
  2. def OAI.AffineBernstein.tubeOpenSet line 36
  3. def OAI.AffineBernstein.tubeLift line 38
  4. lemma OAI.AffineBernstein.continuous_tubeLift line 43
  5. lemma OAI.AffineBernstein.tubeLift_mem line 49
  6. lemma OAI.AffineBernstein.integrable_tube_compact_mul line 57
  7. lemma OAI.AffineBernstein.integrable_tube_compact_sq line 66
  8. def OAI.AffineBernstein.tubeIntegral line 79

    Source comment

    The unrestricted product integral of a cutoff times a tube coefficient.
    def tubeIntegral (μ : Measure S) (M : S × E → ℝ) (σ : S → ℝ) (g : S × E → ℝ) : ℝ :=
…
  9. lemma OAI.AffineBernstein.tubeIntegral_add line 82
  10. lemma OAI.AffineBernstein.tubeIntegral_smul line 95
  11. lemma OAI.AffineBernstein.tubeIntegral_base line 105
  12. lemma OAI.AffineBernstein.tubeIntegral_angular line 115
  13. lemma OAI.AffineBernstein.tubeIntegral_congr_on line 134
  14. lemma OAI.AffineBernstein.tubeIntegral_zero line 146
  15. lemma OAI.AffineBernstein.tsupport_sq_subset line 150
  16. lemma OAI.AffineBernstein.compactSupport_sq line 154
  17. lemma OAI.AffineBernstein.integrable_tube_supported line 158
  18. lemma OAI.AffineBernstein.tubeIntegral_congr_sphere line 174
  19. lemma OAI.AffineBernstein.tubeIntegral_linearCombination line 186