measure_lt_one_eq_integral_div_gamma

English

Let g be a density-like function on E with symmetry and regularity properties. Then the measure of the sublevel set {x : g(x) < 1} equals a gamma-normalized integral: μ({g < 1}) = ∫ e^{-g^p} / Γ(… ).

Русский

Пусть g — функция плотности на E с симметрией и регулярностью. Тогда мера подмножества {x: g(x) < 1} равна гамма-нормализованному интегралу.

LaTeX

$$$\\mu\\{ x : g(x) < 1\\} = \\mathrm{OfReal}\\left( \\frac{ \\int_E e^{-(g(x))^p} d\\mu(x) }{ \\Gamma( \\dim(E)/p + 1 ) } \\right)$$$

Lean4

theorem measure_lt_one_eq_integral_div_gamma {p : ℝ} (hp : 0 < p) :
    μ {x : E | g x < 1} = .ofReal ((∫ (x : E), Real.exp (-(g x) ^ p) ∂μ) / Real.Gamma (finrank ℝ E / p + 1)) := 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 (measure_unitBall_eq_integral_div_gamma ν hp) using 1
  · 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 _ _ _ _ φ
  · -- The map between `E` and `F` as a measurable equivalence

    let ψ :=
      @Homeomorph.toMeasurableEquiv E F tE mE _ _ _ _
        (@ContinuousLinearEquiv.toHomeomorph ℝ ℝ _ _ _ _ _ _ E tE _ F _ _ _ _ φ)
          -- The map `ψ` is measure preserving by construction

    have : @MeasurePreserving E F mE _ ψ μ ν :=
      @Measurable.measurePreserving E F mE _ ψ (@MeasurableEquiv.measurable E F mE _ ψ) _
    rw [← this.integral_comp']
    rfl

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