OAI/Analysis/ProductSpaces/ScalarBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.IndependentProducts.gaussianTail_nonneg line 14
  2. lemma OAI.IndependentProducts.gaussianTail_le_one line 16
  3. lemma OAI.IndependentProducts.gaussianTail_antitone line 19
  4. lemma OAI.IndependentProducts.gaussianTail_pos line 23
  5. lemma OAI.IndependentProducts.integrable_gaussian_abs_excess line 35
  6. lemma OAI.IndependentProducts.excessConstant_pos line 40
  7. lemma OAI.IndependentProducts.gaussian_integral_sq line 54
  8. lemma OAI.IndependentProducts.gaussian_integral_fourth line 59
  9. lemma OAI.IndependentProducts.integral_mul_sq_le line 101
  10. lemma OAI.IndependentProducts.second_moment_tail_bound line 125

    Source documentation

    A second-moment lower bound on the probability of exceeding half the mean.

    lemma second_moment_tail_bound (V : Ω → ℝ) (hV : MemLp V 2 μ)
    (hVmeas : Measurable V) (hpos : ∀ ω, 0 ≤ V ω)
    (a b : ℝ) (ha : 0 ≤ a) (hb : a < b) (hmean : b ≤ ∫ ω, V ω ∂μ) :
    (b - a) ^ 2 ≤ (∫ ω, V ω ^ 2 ∂μ) * μ.real {ω | a ≤ V ω} := by
…
  11. def OAI.IndependentProducts.gaussianRotate line 167

    Source documentation

    Polarization on one independent standard Gaussian pair.

    def gaussianRotate (z : ℝ × ℝ) : ℝ × ℝ :=
…
  12. lemma OAI.IndependentProducts.gaussianRotate_measurable line 170
  13. lemma OAI.IndependentProducts.measurePreserving_gaussianRotate line 172
  14. lemma OAI.IndependentProducts.gaussian_polarization line 237
  15. lemma OAI.IndependentProducts.map_gaussian_finset_sum line 249
  16. lemma OAI.IndependentProducts.map_gaussian_weighted_sum line 263