English
For B with integral vertices and suitable subset s, the integral sum with respect to the unit partition equals a divided sum over the index-set s ∩ (n⁻¹) • L.
Русский
Для B с интегральными вершинами и подходящего множества s интегральная сумма по единичному разбиению равна делённой сумме по множеству индексов s ∩ (n⁻¹) • L.
LaTeX
$$$$ \text{integralSum}(\mathbf{1}_s F) = \frac{1}{n^{|ι|}} \sum'_{x \in s \cap (n^{-1}) \cdot L} F(x) $$$$
Lean4
/-- Let `s` be a bounded, measurable set of `ι → ℝ` whose frontier has zero volume and let `F`
be a continuous function. Then the limit as `n → ∞` of `∑ F x / n ^ card ι`, where the sum is
over the points in `s ∩ n⁻¹ • (ι → ℤ)`, tends to the integral of `F` over `s`. -/
theorem _root_.tendsto_tsum_div_pow_atTop_integral (hF : Continuous F) (hs₁ : IsBounded s) (hs₂ : MeasurableSet s)
(hs₃ : volume (frontier s) = 0) :
Tendsto (fun n : ℕ ↦ (∑' x : ↑(s ∩ (n : ℝ)⁻¹ • L), F x) / n ^ card ι) atTop (nhds (∫ x in s, F x)) :=
by
obtain ⟨B, hB, hs₀⟩ := le_hasIntegralVertices_of_isBounded hs₁
refine Metric.tendsto_atTop.mpr fun ε hε ↦ ?_
have h₁ : ∃ C, ∀ x ∈ Box.Icc B, ‖Set.indicator s F x‖ ≤ C :=
by
obtain ⟨C₀, h₀⟩ := (Box.isCompact_Icc B).exists_bound_of_continuousOn hF.continuousOn
refine ⟨max 0 C₀, fun x hx ↦ ?_⟩
rw [Set.indicator]
split_ifs with hs
· exact le_max_of_le_right (h₀ x hx)
· exact norm_zero.trans_le <| le_max_left 0 _
have h₂ : ∀ᵐ x, ContinuousAt (s.indicator F) x := by
filter_upwards [compl_mem_ae_iff.mpr hs₃] with _ h using (hF.continuousOn).continuousAt_indicator h
obtain ⟨r, hr₁, hr₂⟩ :=
(hasIntegral_iff.mp <| AEContinuous.hasBoxIntegral (volume : Measure (ι → ℝ)) h₁ h₂ IntegrationParams.Riemann)
(ε / 2) (half_pos hε)
refine ⟨⌈(r 0 0 : ℝ)⁻¹⌉₊, fun n hn ↦ lt_of_le_of_lt ?_ (half_lt_self_iff.mpr hε)⟩
have : NeZero n := ⟨Nat.ne_zero_iff_zero_lt.mpr <| (Nat.ceil_pos.mpr (inv_pos.mpr (r 0 0).prop)).trans_le hn⟩
rw [← integralSum_eq_tsum_div _ s F hB hs₀, ← Measure.restrict_restrict_of_subset hs₀, ← integral_indicator hs₂]
refine hr₂ 0 _ ⟨?_, fun _ ↦ ?_, fun h ↦ ?_, fun h ↦ ?_⟩ (prepartition_isPartition _ hB)
· rw [show r 0 = fun _ ↦ r 0 0 from funext_iff.mpr (hr₁ 0 rfl)]
apply prepartition_isSubordinate n B
rw [one_div, inv_le_comm₀ (mod_cast (Nat.pos_of_neZero n)) (r 0 0).prop]
exact le_trans (Nat.le_ceil _) (Nat.cast_le.mpr hn)
· exact prepartition_isHenstock n B
· simp only [IntegrationParams.Riemann, Bool.false_eq_true] at h
· simp only [IntegrationParams.Riemann, Bool.false_eq_true] at h
