OAI/Combinatorics/BooleanFunctions/MomentTransfer.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SquareRootDegree.MomentTransfer.compact_test_tendsto line 14

    Source documentation

    Only compact continuous test functions are passed through weak convergence.

    theorem compact_test_tendsto {Ω : ℕ → Type*} [∀ n, MeasurableSpace (Ω n)]
    (P : ∀ n, Measure (Ω n)) [∀ n, IsProbabilityMeasure (P n)]
    (T : ∀ n, Ω n → ℝ) (hT : TendstoInDistribution T atTop (fun x : ℝ => x) P (gaussianReal 0 1))
    (f : ℝ → ℝ) (hf : Continuous f) (hc : HasCompactSupport f) :
    Tendsto (fun n => ∫ x, f (T n x) ∂P n) atTop (𝓝 (∫ x, f x ∂gaussianReal 0 1)) := by
…
  2. def OAI.SquareRootDegree.MomentTransfer.moments line 29
  3. def OAI.SquareRootDegree.MomentTransfer.means line 35
  4. def OAI.SquareRootDegree.MomentTransfer.vars line 36
  5. def OAI.SquareRootDegree.MomentTransfer.gain line 38
  6. theorem OAI.SquareRootDegree.MomentTransfer.gain_tendsto line 43
  7. theorem OAI.SquareRootDegree.MomentTransfer.hat_le_one line 63
  8. theorem OAI.SquareRootDegree.MomentTransfer.hat_moment_integrable line 68
  9. theorem OAI.SquareRootDegree.MomentTransfer.weight_moment_eq line 77
  10. theorem OAI.SquareRootDegree.MomentTransfer.gaussian_pow_integrable line 95
  11. theorem OAI.SquareRootDegree.MomentTransfer.leaf_moments_tendsto line 104
  12. theorem OAI.SquareRootDegree.MomentTransfer.selector_moments_tendsto line 114
  13. theorem OAI.SquareRootDegree.MomentTransfer.weight_le_one line 135
  14. theorem OAI.SquareRootDegree.MomentTransfer.gaussian_selector_integrable line 141
  15. theorem OAI.SquareRootDegree.MomentTransfer.quadratic_moment_formula line 149
  16. def OAI.SquareRootDegree.MomentTransfer.gaussianLeafMoments line 160
  17. def OAI.SquareRootDegree.MomentTransfer.gaussianSelectorMoments line 161
  18. theorem OAI.SquareRootDegree.MomentTransfer.gaussianLeaf_zero line 163
  19. theorem OAI.SquareRootDegree.MomentTransfer.gaussianLeaf_mean line 165
  20. theorem OAI.SquareRootDegree.MomentTransfer.gaussianLeaf_var line 168
  21. theorem OAI.SquareRootDegree.MomentTransfer.gaussianGain_eq line 174
  22. theorem OAI.SquareRootDegree.MomentTransfer.gaussianGain_pos line 202
  23. def OAI.SquareRootDegree.MomentTransfer.eta line 206
  24. theorem OAI.SquareRootDegree.MomentTransfer.eta_pos line 208
  25. theorem OAI.SquareRootDegree.MomentTransfer.eventually_positive_gain line 210