English
If l ≤ Henstock and B, g satisfy a bounding property, then HasIntegral I l f vol (g I).
Русский
Если l ≤ Хеншток и B, g удовлетворяют ограничивающему свойству, то функция f имеет интеграл HasIntegral на I, равный g I.
LaTeX
$$$$\\text{HasIntegral } I l f vol (g I).$$$$
Lean4
/-- A function `f` has Henstock (or `⊥`) integral over `I` is equal to the value of a box-additive
function `g` on `I` provided that `vol J (f x)` is sufficiently close to `g J` for sufficiently
small boxes `J ∋ x`. This lemma is useful to prove, e.g., to prove the Divergence theorem for
integral along `⊥`.
Let `l` be either `BoxIntegral.IntegrationParams.Henstock` or `⊥`. Let `g` a box-additive function
on subboxes of `I`. Suppose that there exists a nonnegative box-additive function `B` and a
countable set `s` 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
- `x ∈ 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 `ε` if `x ∈ s` and is less than or equal to `ε * B J` otherwise.
Then `f` is integrable on `I` along `l` with integral `g I`. -/
theorem of_le_Henstock_of_forall_isLittleO (hl : l ≤ Henstock) (B : ι →ᵇᵃ[I] ℝ) (hB0 : ∀ J, 0 ≤ B J) (g : ι →ᵇᵃ[I] F)
(s : Set ℝⁿ) (hs : s.Countable)
(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 δ →
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) :=
have A : l.bHenstock := Bool.eq_true_of_true_le hl.2.1
HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (Bool.eq_false_of_le_false hl.1) B hB0 _ s hs (fun _ => A) H₁ <|
by simpa only [A, true_imp_iff] using H₂
