English
If there exists B such that for all x, ε, there exists δ giving a bound on vol J (f x) − g J ≤ ε B J, then HasIntegral I McShane f vol (g I).
Русский
Если существует B, такая что для любых x и ε найдётся δ, дающее предел по vol J (f x) − g J ≤ ε B J, то f интегрируема по McShane на I с интегралом g I.
LaTeX
$$$$\\text{HasIntegral } I \\text{ McShane } f vol (g I).$$$$
Lean4
/-- Suppose that there exists a nonnegative box-additive function `B` with the following property.
For every `c : ℝ≥0`, a point `x ∈ I.Icc`, and a positive `ε` there exists `δ > 0` such that for any
box `J ≤ I` such that
- `J.Icc ⊆ Metric.closedBall x δ`;
- if `l.bDistortion` (i.e., `l = ⊥`), then the distortion of `J` is less than or equal to `c`,
the distance between the term `vol J (f x)` of an integral sum corresponding to `J` and `g J` is
less than or equal to `ε * B J`.
Then `f` is McShane integrable on `I` with integral `g I`. -/
theorem mcShane_of_forall_isLittleO (B : ι →ᵇᵃ[I] ℝ) (hB0 : ∀ J, 0 ≤ B J) (g : ι →ᵇᵃ[I] F)
(H :
∀ (_ : ℝ≥0),
∀ x ∈ Box.Icc I,
∀ ε > (0 : ℝ), ∃ δ > 0, ∀ J ≤ I, Box.Icc J ⊆ Metric.closedBall x δ → dist (vol J (f x)) (g J) ≤ ε * B J) :
HasIntegral I McShane f vol (g I) :=
(HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (l := McShane) rfl B hB0 g ∅ countable_empty
(fun ⟨_x, hx⟩ => hx.elim) fun _ _ hx => hx.2.elim) <|
by simpa only [McShane, Bool.coe_sort_false, false_imp_iff, true_imp_iff, diff_empty] using H
