volume_sum_rpow_lt_one — Mathlib

English

If a continuous map f on R with restriction to Icc(0,1) has translations whose sup-norms form a summable series, then f is integrable over R.

Русский

Если непрерывная карта f на R, ограниченная на Icc(0,1), имеет сумму норм своих сдвигов, то f интегрируема по R.

LaTeX

$$$\text{Summable}\bigl( \|f \circ (\text{addRight } n) \bigr|_{Icc(0,1)} \bigr) \Rightarrow \text{Integrable}(f)$$$$

Lean4

theorem volume_sum_rpow_lt_one {p : ℝ} (hp : 1 ≤ p) :
    volume {x : ι → ℂ | ∑ i, ‖x i‖ ^ p < 1} =
      .ofReal ((π * Real.Gamma (2 / p + 1)) ^ card ι / Real.Gamma (2 * 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 (norm_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₁)] at eq_norm
  have : Fact (1 ≤ ENNReal.ofReal p) := fact_iff.mpr (ENNReal.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] 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 (norm_nonneg _) _)
  · simp_rw [← rpow_mul (h₂ _), div_mul_cancel₀ _ (ne_of_gt h₁), Real.rpow_one, ← Finset.sum_neg_distrib, Real.exp_sum]
    rw [integral_fintype_prod_volume_eq_pow fun x : ℂ => Real.exp (-‖x‖ ^ p), Complex.integral_exp_neg_rpow hp]
  ·
    rw [finrank_pi_fintype, Complex.finrank_real_complex, Finset.sum_const, smul_eq_mul, Nat.cast_mul, Nat.cast_ofNat,
      Fintype.card, mul_comm]

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