OAI/Geometry/Convex/GeneralMahler/ParamMoment.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

§02 continuity of the Gaussian polynomial moments of P.

  1. theorem OAI.GeneralMahler.continuous_normal_integral line 13

    Source comment

    generic dominated parameter expectation
    theorem continuous_normal_integral {X F : Type*} [TopologicalSpace X] [FirstCountableTopology X] [NormedAddCommGroup F]
    [NormedSpace ℝ F] {f : X → Rn m → F} {g : Rn m→ℝ} (hg : Integrable g (normal m))
    (hm : ∀ x, AEStronglyMeasurable (f x) (normal m)) (he : ∀ x y, ‖f x y‖ ≤ g y)
    (hf : ∀ y, Continuous fun x=>f x y) : Continuous (fun x=>∫ y, f x y ∂normal m) :=
…

    Mentions: OAI.GeneralMahler.Rn, OAI.GeneralMahler.normal

  2. lemma OAI.GeneralMahler.continuous_matrix_op line 20
  3. lemma OAI.GeneralMahler.Param.rootNorm line 30
  4. theorem OAI.GeneralMahler.Param.S_action line 33
  5. theorem OAI.GeneralMahler.Param.iS_action line 40
  6. theorem OAI.GeneralMahler.Param.XT_cont line 51
  7. theorem OAI.GeneralMahler.Param.XT_bound line 59
  8. theorem OAI.GeneralMahler.Param.weighted_P_cont line 76