English
If B has integral vertices, then the prepartition n B is a partition of B and its integral structure aligns with the box-additive framework.
Русский
Если у B есть интегральные вершины, то предразбиение n B образует разбиение B и интегральная структура согласуется с рамкой BoxAdditive.
LaTeX
$$$$ (\mathrm{prepartition}(n,B)).\mathrm{IsPartition} \land \text{(compatibility with box-additive structure)} $$$$
Lean4
theorem integralSum_eq_tsum_div {B : Box ι} (hB : hasIntegralVertices B) (hs₀ : s ≤ B) :
integralSum (Set.indicator s F) (BoxAdditiveMap.toSMul (Measure.toBoxAdditive volume)) (prepartition n B) =
(∑' x : ↑(s ∩ (n : ℝ)⁻¹ • L), F x) / n ^ card ι :=
by
classical
unfold integralSum
have : Fintype ↑(s ∩ (n : ℝ)⁻¹ • L) := by
apply Set.Finite.fintype
rw [← coe_pointwise_smul, ZSpan.smul _ (inv_ne_zero (NeZero.ne _))]
exact ZSpan.setFinite_inter _ (B.isBounded.subset hs₀)
rw [tsum_fintype, Finset.sum_set_coe, Finset.sum_div, eq_comm]
simp_rw [Set.indicator_apply, apply_ite, BoxAdditiveMap.toSMul_apply, Measure.toBoxAdditive_apply, smul_eq_mul,
mul_zero, Finset.sum_ite, Finset.sum_const_zero, add_zero]
refine
Finset.sum_bij (fun x _ ↦ box n (index n x)) (fun _ hx ↦ Finset.mem_filter.mpr ?_) (fun _ hx _ hy h ↦ ?_)
(fun I hI ↦ ?_) (fun _ hx ↦ ?_)
· rw [Set.mem_toFinset] at hx
refine ⟨mem_prepartition_boxes_iff.mpr ⟨index n _, mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1), rfl⟩, ?_⟩
simp_rw [prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
tag_index_eq_self_of_mem_smul_span n hx.2, hx.1]
· rw [Set.mem_toFinset] at hx hy
exact eq_of_mem_smul_span_of_index_eq_index n hx.2 hy.2 (box_injective n h)
· rw [Finset.mem_filter] at hI
refine ⟨(prepartition n B).tag I, Set.mem_toFinset.mpr ⟨hI.2, ?_⟩, box_index_tag_eq_self n hI.1⟩
rw [← box_index_tag_eq_self n hI.1, prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hI.2))]
exact tag_mem_smul_span _ _
· rw [Set.mem_toFinset] at hx
rw [measureReal_def, volume_box, prepartition_tag n (mem_admissibleIndex_of_mem_box n hB (hs₀ hx.1)),
tag_index_eq_self_of_mem_smul_span n hx.2, ENNReal.toReal_div, ENNReal.toReal_one, ENNReal.toReal_pow,
ENNReal.toReal_natCast, mul_comm_div, one_mul]
