English
On a finite product space, the product of integrable functions is integrable.
Русский
На конечном произведении пространство, произведение интегрируемых функций интегрируемо.
LaTeX
$$$\\text{fin_nat_prod}$: if each f_i is integrable on μ_i, then ∏ f_i is integrable on π μ$$
Lean4
/-- If a continuous function `c` realizes its maximum at a unique point `x₀` in a compact set `s`,
then the sequence of functions `(c x) ^ n / ∫ (c x) ^ n` is a sequence of peak functions
concentrating around `x₀`. Therefore, `∫ (c x) ^ n * g / ∫ (c x) ^ n` converges to `g x₀` if `g` is
integrable on `s` and continuous at `x₀`.
Version assuming that `μ` gives positive mass to all open sets.
For a less precise but more usable version, see
`tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn`.
-/
theorem tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_integrableOn [MetrizableSpace α]
[IsLocallyFiniteMeasure μ] [IsOpenPosMeasure μ] (hs : IsCompact s) {c : α → ℝ} (hc : ContinuousOn c s)
(h'c : ∀ y ∈ s, y ≠ x₀ → c y < c x₀) (hnc : ∀ x ∈ s, 0 ≤ c x) (hnc₀ : 0 < c x₀) (h₀ : x₀ ∈ closure (interior s))
(hmg : IntegrableOn g s μ) (hcg : ContinuousWithinAt g s x₀) :
Tendsto (fun n : ℕ => (∫ x in s, c x ^ n ∂μ)⁻¹ • ∫ x in s, c x ^ n • g x ∂μ) atTop (𝓝 (g x₀)) :=
by
have : x₀ ∈ s := by rw [← hs.isClosed.closure_eq]; exact closure_mono interior_subset h₀
apply
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_measure_nhdsWithin_pos hs _ hc h'c hnc hnc₀ this hmg
hcg
intro u u_open x₀_u
calc
0 < μ (u ∩ interior s) := (u_open.inter isOpen_interior).measure_pos μ (_root_.mem_closure_iff.1 h₀ u u_open x₀_u)
_ ≤ μ (u ∩ s) := by gcongr; apply interior_subset
