Documentation

TauCeti.Analysis.BoxIntegral.IntervalIntegral

One-dimensional box integrals and interval integrals #

TauCeti.BoxIntegral.intervalBox realizes a nondegenerate real interval as a box on Fin 1. For a Bochner integrable function, the box integral agrees with its interval integral for any non-Riemann integration parameters, in particular Henstock–Kurzweil parameters.

source
def TauCeti.BoxIntegral.intervalBox (a b : ℝ) (hab : a < b) :
BoxIntegral.Box (Fin 1)

The one-dimensional box corresponding to the half-open interval (a, b].

Equations
Instances For
    source
    @[simp]
    theorem TauCeti.BoxIntegral.intervalBox_lower (a b : ℝ) (hab : a < b) (i : Fin 1) :
    (intervalBox a b hab).lower i = a
    source
    @[simp]
    theorem TauCeti.BoxIntegral.intervalBox_upper (a b : ℝ) (hab : a < b) (i : Fin 1) :
    (intervalBox a b hab).upper i = b
    source
    @[simp]
    theorem TauCeti.BoxIntegral.mem_intervalBox {a b : ℝ} {hab : a < b} {x : Fin 1 → ℝ} :
    x ∈ intervalBox a b hab ↔ x 0 ∈ Set.Ioc a b
    source
    @[simp]
    theorem TauCeti.BoxIntegral.mem_Icc_intervalBox {a b : ℝ} {hab : a < b} {x : Fin 1 → ℝ} :
    x ∈ BoxIntegral.Box.Icc (intervalBox a b hab) ↔ x 0 ∈ Set.Icc a b
    source
    theorem TauCeti.BoxIntegral.coe_intervalBox (a b : ℝ) (hab : a < b) :
    ↑(intervalBox a b hab) = ⇑(MeasurableEquiv.piUnique fun (x : Fin 1) => ℝ) ⁻¹' Set.Ioc a b

    Evaluation at the sole coordinate identifies the interval box with a real interval.

    source
    theorem TauCeti.BoxIntegral.ae_eq_intervalBox {E : Type u_1} {a b : ℝ} (hab : a < b) {f g : ℝ → E} (h : f =ᵐ[MeasureTheory.volume.restrict (Set.Ioc a b)] g) :
    (fun (x : Fin 1 → ℝ) => f (x 0)) =ᵐ[MeasureTheory.volume.restrict ↑(intervalBox a b hab)] fun (x : Fin 1 → ℝ) => g (x 0)

    Almost-everywhere equality on a real interval pulls back to its one-dimensional box.

    source
    @[simp]
    theorem TauCeti.BoxIntegral.intervalBox_le_intervalBox_iff {a b c d : ℝ} (hab : a < b) (hcd : c < d) :
    intervalBox c d hcd ≤ intervalBox a b hab ↔ a ≤ c ∧ d ≤ b

    Interval-box inclusion is exactly the pair of endpoint inequalities.

    source
    theorem TauCeti.BoxIntegral.splitLower_intervalBox {a c b : ℝ} (hac : a < c) (hcb : c < b) :
    (intervalBox a b ⋯).splitLower 0 c = ↑(intervalBox a c hac)

    Splitting at an interior point gives the lower interval box.

    source
    theorem TauCeti.BoxIntegral.splitUpper_intervalBox {a c b : ℝ} (hac : a < c) (hcb : c < b) :
    (intervalBox a b ⋯).splitUpper 0 c = ↑(intervalBox c b hcb)

    Splitting at an interior point gives the upper interval box.

    source
    theorem TauCeti.BoxIntegral.integrableOn_intervalBox_iff {E : Type u_1} [TopologicalSpace E] [ENormedAddMonoid E] {a b : ℝ} (hab : a < b) {f : ℝ → E} :
    MeasureTheory.IntegrableOn (fun (x : Fin 1 → ℝ) => f (x 0)) (↑(intervalBox a b hab)) MeasureTheory.volume ↔ IntervalIntegrable f MeasureTheory.volume a b

    Integrability on an interval is equivalent to integrability on its interval box.

    source
    theorem TauCeti.BoxIntegral.setIntegral_intervalBox {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] {a b : ℝ} (hab : a < b) (f : ℝ → E) :
    ∫ (x : Fin 1 → ℝ) in ↑(intervalBox a b hab), f (x 0) = ∫ (x : ℝ) in a..b, f x

    The Bochner integral on an interval box is the usual oriented interval integral.

    source
    theorem IntervalIntegrable.hasBoxIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {a b : ℝ} (hf : IntervalIntegrable f MeasureTheory.volume a b) (hab : a < b) (l : BoxIntegral.IntegrationParams) (hl : l.bRiemann = false) :
    BoxIntegral.HasIntegral (TauCeti.BoxIntegral.intervalBox a b hab) l (fun (x : Fin 1 → ℝ) => f (x 0)) BoxIntegral.BoxAdditiveMap.volume (∫ (x : ℝ) in a..b, f x)

    Every Bochner integrable function has the same non-Riemann box integral on Fin 1.