English
A function continuousOn a box is box-integrable with respect to any locally finite measure.
Русский
Функция непрерывна на коробке, значит по любой локально конечной мере она box-интегрируема.
LaTeX
$$$$\\text{Integrable on } I \\; l \\; f \\; μ.$$$$
Lean4
/-- This is an auxiliary lemma used to prove two statements at once. Use one of the next two
lemmas instead. -/
theorem of_bRiemann_eq_false_of_forall_isLittleO (hl : l.bRiemann = false) (B : ι →ᵇᵃ[I] ℝ) (hB0 : ∀ J, 0 ≤ B J)
(g : ι →ᵇᵃ[I] F) (s : Set ℝⁿ) (hs : s.Countable) (hlH : s.Nonempty → l.bHenstock = true)
(H₁ :
∀ (c : ℝ≥0),
∀ x ∈ Box.Icc I ∩ s,
∀ ε > (0 : ℝ),
∃ δ > 0,
∀ J ≤ I,
Box.Icc J ⊆ Metric.closedBall x δ →
x ∈ Box.Icc J → (l.bDistortion → J.distortion ≤ c) → dist (vol J (f x)) (g J) ≤ ε)
(H₂ :
∀ (c : ℝ≥0),
∀ x ∈ Box.Icc I \ s,
∀ ε > (0 : ℝ),
∃ δ > 0,
∀ J ≤ I,
Box.Icc J ⊆ Metric.closedBall x δ →
(l.bHenstock → x ∈ Box.Icc J) →
(l.bDistortion → J.distortion ≤ c) → dist (vol J (f x)) (g J) ≤ ε * B J) :
HasIntegral I l f vol (g I) := by
/- We choose `r x` differently for `x ∈ s` and `x ∉ s`.
For `x ∈ s`, we choose `εs` such that `∑' x : s, εs x < ε / 2 / 2 ^ #ι`, then choose `r x` so
that `dist (vol J (f x)) (g J) ≤ εs x` for `J` in the `r x`-neighborhood of `x`. This guarantees
that the sum of these distances over boxes `J` such that `π.tag J ∈ s` is less than `ε / 2`. We
need an additional multiplier `2 ^ #ι` because different boxes can have the same tag.
For `x ∉ s`, we choose `r x` so that `dist (vol (J (f x))) (g J) ≤ (ε / 2 / B I) * B J` for a
box `J` in the `δ`-neighborhood of `x`. -/
refine ((l.hasBasis_toFilteriUnion_top _).tendsto_iff Metric.nhds_basis_closedBall).2 ?_
intro ε ε0
simp only [← exists_prop, gt_iff_lt, Subtype.exists'] at H₁ H₂
choose! δ₁ Hδ₁ using H₁
choose! δ₂ Hδ₂ using H₂
have ε0' := half_pos ε0; have H0 : 0 < (2 : ℝ) ^ Fintype.card ι := pow_pos zero_lt_two _
rcases hs.exists_pos_forall_sum_le (div_pos ε0' H0) with ⟨εs, hεs0, hεs⟩
simp only [le_div_iff₀' H0, mul_sum] at hεs
rcases exists_pos_mul_lt ε0' (B I) with ⟨ε', ε'0, hεI⟩
classical
set δ : ℝ≥0 → ℝⁿ → Ioi (0 : ℝ) := fun c x => if x ∈ s then δ₁ c x (εs x) else (δ₂ c) x ε'
refine ⟨δ, fun c => l.rCond_of_bRiemann_eq_false hl, ?_⟩
simp only [mem_setOf_eq]
rintro π
⟨c, hπδ, hπp⟩
-- Now we split the sum into two parts based on whether `π.tag J` belongs to `s` or not.
rw [← g.sum_partition_boxes le_rfl hπp, Metric.mem_closedBall, integralSum, ←
sum_filter_add_sum_filter_not π.boxes fun J => π.tag J ∈ s, ←
sum_filter_add_sum_filter_not π.boxes fun J => π.tag J ∈ s, ← add_halves ε]
refine dist_add_add_le_of_le ?_ ?_
· rcases s.eq_empty_or_nonempty with (rfl | hsne);
·
simp [ε0'.le]
/- For the boxes such that `π.tag J ∈ s`, we use the fact that at most `2 ^ #ι` boxes have the
same tag. -/
specialize hlH hsne
have : ∀ J ∈ {J ∈ π.boxes | π.tag J ∈ s}, dist (vol J (f <| π.tag J)) (g J) ≤ εs (π.tag J) := fun J hJ ↦
by
rw [Finset.mem_filter] at hJ; obtain ⟨hJ, hJs⟩ := hJ
refine
Hδ₁ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ (hεs0 _) _ (π.le_of_mem' _ hJ) ?_ (hπδ.2 hlH J hJ) fun hD =>
(Finset.le_sup hJ).trans (hπδ.3 hD)
convert hπδ.1 J hJ using 3; exact (if_pos hJs).symm
refine (dist_sum_sum_le_of_le _ this).trans ?_
rw [sum_comp]
refine (sum_le_sum ?_).trans (hεs _ ?_)
· rintro b -
rw [← Nat.cast_two, ← Nat.cast_pow, ← nsmul_eq_mul]
refine nsmul_le_nsmul_left (hεs0 _).le ?_
refine (Finset.card_le_card ?_).trans ((hπδ.isHenstock hlH).card_filter_tag_eq_le b)
exact filter_subset_filter _ (filter_subset _ _)
· rw [Finset.coe_image, Set.image_subset_iff]
exact fun J hJ =>
(Finset.mem_filter.1 hJ).2
/- Now we deal with boxes such that `π.tag J ∉ s`.
In this case the estimate is straightforward. -/
calc
dist (∑ J ∈ π.boxes with tag π J ∉ s, vol J (f (tag π J))) (∑ J ∈ π.boxes with tag π J ∉ s, g J) ≤
∑ J ∈ π.boxes with tag π J ∉ s, ε' * B J :=
dist_sum_sum_le_of_le _ fun J hJ ↦ by
rw [Finset.mem_filter] at hJ; obtain ⟨hJ, hJs⟩ := hJ
refine
Hδ₂ c _ ⟨π.tag_mem_Icc _, hJs⟩ _ ε'0 _ (π.le_of_mem' _ hJ) ?_ (fun hH => hπδ.2 hH J hJ) fun hD =>
(Finset.le_sup hJ).trans (hπδ.3 hD)
convert hπδ.1 J hJ using 3; exact (if_neg hJs).symm
_ ≤ ∑ J ∈ π.boxes, ε' * B J := by
gcongr
· exact fun _ _ _ ↦ mul_nonneg ε'0.le (hB0 _)
· apply filter_subset
_ = B I * ε' := by rw [← mul_sum, B.sum_partition_boxes le_rfl hπp, mul_comm]
_ ≤ ε / 2 := hεI.le
