volume_interior_eq_volume_closure

English

The volume of the interior of normLeOne(K) equals the volume of its closure.

Русский

Объем внутренности normLeOne(K) равен объему его замыкания.

LaTeX

$$$\\operatorname{vol}(\\operatorname{interior}(\\operatorname{normLeOne}(K))) = \\operatorname{vol}(\\operatorname{closure}(\\operatorname{normLeOne}(K))).$$$

Lean4

theorem volume_interior_eq_volume_closure : volume (interior (normLeOne K)) = volume (closure (normLeOne K)) :=
  by
  have h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K) :=
    (isCompact_compactSet K).measurableSet.preimage (continuous_normAtAllPlaces K).measurable
  have h₂ : MeasurableSet (normAtAllPlaces ⁻¹' (expMapBasis '' interior (paramSet K))) :=
    by
    refine MeasurableSet.preimage ?_ (continuous_normAtAllPlaces K).measurable
    refine
      MeasurableSet.image_of_continuousOn_injOn ?_ (continuous_expMapBasis K).continuousOn
        (injective_expMapBasis K).injOn
    exact measurableSet_interior
  refine le_antisymm (measure_mono interior_subset_closure) ?_
  refine (measure_mono (closure_normLeOne_subset K)).trans ?_
  refine le_of_eq_of_le ?_ (measure_mono (subset_interior_normLeOne K))
  rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₁,
    normAtAllPlaces_image_preimage_of_nonneg (fun x a w ↦ nonneg_of_mem_compactSet K a w),
    volume_eq_two_pow_mul_two_pi_pow_mul_integral Set.preimage_image_preimage h₂,
    normAtAllPlaces_image_preimage_expMapBasis, setLIntegral_congr (compactSet_ae K),
    setLIntegral_expMapBasis_image measurableSet_closure (by fun_prop),
    setLIntegral_expMapBasis_image measurableSet_interior (by fun_prop),
    setLIntegral_congr (closure_paramSet_ae_interior K)]

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