measure_le_eq_lt — Mathlib

English

For a function g with appropriate regularity, the measure of the sublevel set {x: g(x) ≤ r} equals the measure of {x: g(x) < r} for any real r: μ({g ≤ r}) = μ({g < r}).

Русский

Для любой реальной величины r верно равенство мер множеств {g ≤ r} и {g < r}.

LaTeX

$$$\mu\{ x : g(x) \le r \} = \mu\{ x : g(x) < r \}$$$

Lean4

theorem measure_le_eq_lt [Nontrivial E] (r : ℝ) : μ {x : E | g x ≤ r} = μ {x : E | g x < r} := by
  -- We copy `E` to a new type `F` on which we will put the norm defined by `g`

  letI F : Type _ := E
  letI : NormedAddCommGroup F :=
    { norm := g
      dist := fun x y => g (x - y)
      dist_self := by simp only [_root_.sub_self, h1, forall_const]
      dist_comm := fun _ _ => by rw [← h2, neg_sub]
      dist_triangle := fun x y z => by convert h3 (x - y) (y - z) using 1; simp [F]
      edist := fun x y => .ofReal (g (x - y))
      edist_dist := fun _ _ => rfl
      eq_of_dist_eq_zero := by convert fun _ _ h => eq_of_sub_eq_zero (h4 h) }
  letI : NormedSpace ℝ F :=
    { norm_smul_le := fun _ _ ↦ h5 _ _ }
      -- We put the new topology on F

  letI : TopologicalSpace F := UniformSpace.toTopologicalSpace
  letI : MeasurableSpace F := borel F
  have : BorelSpace F :=
    { measurable_eq := rfl }
      -- The map between `E` and `F` as a continuous linear equivalence

  let φ :=
    @LinearEquiv.toContinuousLinearEquiv ℝ _ E _ _ tE _ _ F _ _ _ _ _ _ _ _ _
      (LinearEquiv.refl ℝ E : E ≃ₗ[ℝ] F)
        -- The measure `ν` is the measure on `F` defined by `μ`
          -- Since we have two different topologies, it is necessary to specify the topology of E

  let ν : Measure F := @Measure.map E F mE _ φ μ
  convert addHaar_closedBall_eq_addHaar_ball ν 0 r using 1
  · rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_closedBall]
    · congr!
      simp_rw [Metric.closedBall, dist_zero_right]
      rfl
    · refine @Continuous.measurable E F tE mE _ _ _ _ φ ?_
      exact @ContinuousLinearEquiv.continuous ℝ ℝ _ _ _ _ _ _ E tE _ F _ _ _ _ φ
  · rw [@Measure.map_apply E F mE _ μ φ _ _ measurableSet_ball]
    · congr!
      simp_rw [Metric.ball, dist_zero_right]
      rfl
    · refine @Continuous.measurable E F tE mE _ _ _ _ φ ?_
      exact @ContinuousLinearEquiv.continuous ℝ ℝ _ _ _ _ _ _ E tE _ F _ _ _ _ φ

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