English
There exists a tagged prepartition π' such that π'.toPrepartition ≤ π, π' is Henstock and subordinate to r, π'.distortion = π.distortion, and π'.iUnion = π.iUnion.
Русский
Существует тэгированное предразбиение π', такое что π'.toPrepartition ≤ π, π' — Хеншкоптово и подчинено r, distortion совпадает, и iUnion совпадает.
LaTeX
$$$ \\exists \\pi':\\mathrm{TaggedPrepartition}(I),\\ \\pi'.\\mathrm{toPrepartition} \\le \\pi \\wedge \\pi'.\\mathrm{IsHenstock} \\wedge \\pi'.\\mathrm IsSubordinate r \\wedge \\pi'.\\mathrm{distortion} = \\pi.distortion \\wedge \\pi'.\\mathrm iUnion = \\pi.iUnion$$$
Lean4
/-- Given a box `I` in `ℝⁿ`, a function `r : ℝⁿ → (0, ∞)`, and a prepartition `π` of `I`, there
exists a tagged prepartition `π'` of `I` such that
* each box of `π'` is included in some box of `π`;
* `π'` is a Henstock partition;
* `π'` is subordinate to `r`;
* `π'` covers exactly the same part of `I` as `π`;
* the distortion of `π'` is equal to the distortion of `π`.
-/
theorem exists_tagged_le_isHenstock_isSubordinate_iUnion_eq {I : Box ι} (r : (ι → ℝ) → Ioi (0 : ℝ))
(π : Prepartition I) :
∃ π' : TaggedPrepartition I,
π'.toPrepartition ≤ π ∧
π'.IsHenstock ∧ π'.IsSubordinate r ∧ π'.distortion = π.distortion ∧ π'.iUnion = π.iUnion :=
by
have := fun J => Box.exists_taggedPartition_isHenstock_isSubordinate_homothetic J r
choose! πi πip πiH πir _ πid using this
refine
⟨π.biUnionTagged πi, biUnion_le _ _, isHenstock_biUnionTagged.2 fun J _ => πiH J,
isSubordinate_biUnionTagged.2 fun J _ => πir J, ?_, π.iUnion_biUnion_partition fun J _ => πip J⟩
rw [distortion_biUnionTagged]
exact sup_congr rfl fun J _ => πid J
