measurableSet_fundamentalCone — Mathlib

English

The fundamental cone is a measurable subset of the mixed space with respect to the natural product measure.

Русский

Фундаментальный конус является измеримой подмножество смешанного пространства относительно естественной произведенной меры.

LaTeX

$$$\text{MeasurableSet}(\text{fundamentalCone}(K)).$$$

Lean4

theorem measurableSet_fundamentalCone : MeasurableSet (fundamentalCone K) := by
  classical
  refine MeasurableSet.diff ?_ ?_
  · unfold logMap
    refine
      MeasurableSet.preimage (ZSpan.fundamentalDomain_measurableSet _) <|
        measurable_pi_iff.mpr fun w ↦ measurable_const.mul ?_
    exact
      (continuous_normAtPlace _).measurable.log.sub <|
        (mixedEmbedding.continuous_norm _).measurable.log.mul measurable_const
  · exact measurableSet_eq_fun (mixedEmbedding.continuous_norm K).measurable measurable_const

Похожие утверждения