volume_sum_rpow_lt_one — Mathlib

English

If s has density one at x with respect to closed balls, then for every measurable t with μ t ≠ 0, the intersection s ∩ ({x} + r t) is nonempty for all sufficiently small positive r.

Русский

Если s имеет плотность единицу в x относительно замкнутых шаров, то при любом измеримом t с μ t ≠ 0 пересечение s ∩ ({x} + r t) непусто для достаточно малых положительных r.

LaTeX

$$$\forall^\infty r \to 0^+,\ (s \cap (\{x\} + r\, t)).\text{Nonempty}$$$

Lean4

theorem volume_sum_rpow_lt_one (hp : 1 ≤ p) :
    volume {x : ι → ℝ | ∑ i, |x i| ^ p < 1} = .ofReal ((2 * Gamma (1 / p + 1)) ^ card ι / Gamma (card ι / p + 1)) :=
  by
  have h₁ : 0 < p := by linarith
  have h₂ : ∀ x : ι → ℝ, 0 ≤ ∑ i, |x i| ^ p :=
    by
    refine fun _ => Finset.sum_nonneg' ?_
    exact fun i =>
      (fun _ => rpow_nonneg (abs_nonneg _) _)
        _
          -- We collect facts about `Lp` norms that will be used in `measure_lt_one_eq_integral_div_gamma`

  have eq_norm := fun x : ι → ℝ =>
    (PiLp.norm_eq_sum (p := .ofReal p) (f := x) ((toReal_ofReal (le_of_lt h₁)).symm ▸ h₁))
  simp_rw [toReal_ofReal (le_of_lt h₁), Real.norm_eq_abs] at eq_norm
  have : Fact (1 ≤ ENNReal.ofReal p) := fact_iff.mpr (ofReal_one ▸ (ofReal_le_ofReal hp))
  have nm_zero := norm_zero (E := PiLp (.ofReal p) (fun _ : ι => ℝ))
  have eq_zero := fun x : ι → ℝ => norm_eq_zero (E := PiLp (.ofReal p) (fun _ : ι => ℝ)) (a := x)
  have nm_neg := fun x : ι → ℝ => norm_neg (E := PiLp (.ofReal p) (fun _ : ι => ℝ)) x
  have nm_add := fun x y : ι → ℝ => norm_add_le (E := PiLp (.ofReal p) (fun _ : ι => ℝ)) x y
  simp_rw [eq_norm] at eq_zero nm_zero nm_neg nm_add
  have nm_smul := fun (r : ℝ) (x : ι → ℝ) => norm_smul_le (β := PiLp (.ofReal p) (fun _ : ι => ℝ)) r x
  simp_rw [eq_norm, norm_eq_abs] at nm_smul
  convert
    (measure_lt_one_eq_integral_div_gamma (volume : Measure (ι → ℝ)) (g := fun x => (∑ i, |x i| ^ p) ^ (1 / p)) nm_zero
      nm_neg nm_add (eq_zero _).mp (fun r x => nm_smul r x) (by linarith : 0 < p)) using
    4
  · rw [rpow_lt_one_iff' _ (one_div_pos.mpr h₁)]
    exact Finset.sum_nonneg' (fun _ => rpow_nonneg (abs_nonneg _) _)
  · simp_rw [← rpow_mul (h₂ _), div_mul_cancel₀ _ (ne_of_gt h₁), Real.rpow_one, ← Finset.sum_neg_distrib, exp_sum]
    rw [integral_fintype_prod_volume_eq_pow fun x : ℝ => exp (-|x| ^ p), integral_comp_abs (f := fun x => exp (-x ^ p)),
      integral_exp_neg_rpow h₁]
  · rw [finrank_fintype_fun_eq_card]

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