Theorems · Theorem · real analysis

BoxIntegral.Integrable.dist_integralSum_le_of_memBaseSet

∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤}
  {c₁ c₂ : NNReal} {ε₁ ε₂ : ℝ} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} (h : BoxIntegral.Integrable I l f vol),
  0 < ε₁ →
    0 < ε₂ →
      l.MemBaseSet I c₁ (h.convergenceR ε₁ c₁) π₁ →
        l.MemBaseSet I c₂ (h.convergenceR ε₂ c₂) π₂ →
          π₁.iUnion = π₂.iUnion → dist (BoxIntegral.integralSum f vol π₁) (BoxIntegral.integralSum f vol π₂) ≤ ε₁ + ε₂

Henstock-Sacks inequality. Let r₁ r₂ : ℝⁿ → (0, ∞) be a function such that for any tagged partition of I subordinate to rₖ, k=1,2, the integral sum of f over this partition differs from the integral of f by at most εₖ. Then for any two tagged prepartition π₁ π₂ subordinate to r₁ and r₂ respectively and covering the same part of I, the integral sums of f over these prepartitions differ from each other by at most ε₁ + ε₂. The actual statement - uses BoxIntegral.Integrable.convergenceR instead of a predicate assumption on r; - uses BoxIntegral.IntegrationParams.MemBaseSet instead of “subordinate to r” to account for additional requirements like being a Henstock partition or having a bounded distortion. See also BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet_of_iUnion_eq and BoxIntegral.Integrable.dist_integralSum_sum_integral_le_of_memBaseSet.

Defined in

Mathlib.Analysis.BoxIntegral.Basic

Cited by

2 results in Mathlib

Foundations

Depth 174 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceNormedAddCommGroupNormedSpaceFintype