English
The integral of -f equals the negative of the integral of f: integral I l (-f) vol = - integral I l f vol.
Русский
Интеграл от −f равен отрицанию интеграла от f: ∫−f = −∫f.
LaTeX
$$$\mathrm{integral}(I,l,-f,vol) = -\mathrm{integral}(I,l,f,vol)$$$
Lean4
/-- In a complete space, a function is integrable if and only if its integral sums form a Cauchy
net. Here we restate this fact in terms of `∀ ε > 0, ∃ r, ...`. -/
theorem integrable_iff_cauchy_basis [CompleteSpace F] :
Integrable I l f vol ↔
∀ ε > (0 : ℝ),
∃ r : ℝ≥0 → ℝⁿ → Ioi (0 : ℝ),
(∀ c, l.RCond (r c)) ∧
∀ c₁ c₂ π₁ π₂,
l.MemBaseSet I c₁ (r c₁) π₁ →
π₁.IsPartition →
l.MemBaseSet I c₂ (r c₂) π₂ →
π₂.IsPartition → dist (integralSum f vol π₁) (integralSum f vol π₂) ≤ ε :=
by
rw [integrable_iff_cauchy, cauchy_map_iff',
(l.hasBasis_toFilteriUnion_top _).prod_self.tendsto_iff uniformity_basis_dist_le]
refine forall₂_congr fun ε _ => exists_congr fun r => ?_
simp only [Prod.forall, exists_imp, prodMk_mem_set_prod_eq, and_imp, mem_setOf_eq]
exact
and_congr Iff.rfl
⟨fun H c₁ c₂ π₁ π₂ h₁ hU₁ h₂ hU₂ => H π₁ π₂ c₁ h₁ hU₁ c₂ h₂ hU₂, fun H π₁ π₂ c₁ h₁ hU₁ c₂ h₂ hU₂ =>
H c₁ c₂ π₁ π₂ h₁ hU₁ h₂ hU₂⟩
