Oriented Henstock integrals on real intervals

HasHenstockIntervalIntegral f a b y is the existing Henstock box integral on the one-dimensional interval box, with the sign reversed when b < a and value zero when the endpoints coincide. No new choice of integral values is introduced. Restriction and subdivision use Mathlib's subbox theorem and box additivity, and apply to conditionally integrable functions.

def TauCeti.BoxIntegral.HasHenstockIntervalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ) (y : E) : Prop

The actual Henstock box integral with the orientation of a raw real parameter interval.

Equations

• One or more equations did not get rendered due to their size.

def TauCeti.BoxIntegral.HenstockIntervalIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ) : Prop

Genuine existence of an oriented Henstock interval integral.

Equations

• TauCeti.BoxIntegral.HenstockIntervalIntegrable f a b = ∃ (y : E), TauCeti.BoxIntegral.HasHenstockIntervalIntegral f a b y

theorem TauCeti.BoxIntegral.henstockIntervalIntegrable_iff {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} : HenstockIntervalIntegrable f a b ↔ ∃ (y : E), HasHenstockIntervalIntegral f a b y

Oriented gauge integrability is existence of an actual integral value.

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_iff_of_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {y : E} (hab : a < b) : HasHenstockIntervalIntegral f a b y ↔ BoxIntegral.HasIntegral (intervalBox a b hab) BoxIntegral.IntegrationParams.Henstock (fun (x : Fin 1 → ℝ) => f (x 0)) BoxIntegral.BoxAdditiveMap.volume y

On a positively oriented interval the predicate is exactly the existing box predicate.

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_iff_of_gt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {y : E} (hba : b < a) : HasHenstockIntervalIntegral f a b y ↔ BoxIntegral.HasIntegral (intervalBox b a hba) BoxIntegral.IntegrationParams.Henstock (fun (x : Fin 1 → ℝ) => f (x 0)) BoxIntegral.BoxAdditiveMap.volume (-y)

On a negatively oriented interval the existing box value has the opposite sign.

theorem TauCeti.BoxIntegral.henstockIntervalIntegrable_iff_of_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hab : a < b) : HenstockIntervalIntegrable f a b ↔ BoxIntegral.Integrable (intervalBox a b hab) BoxIntegral.IntegrationParams.Henstock (fun (x : Fin 1 → ℝ) => f (x 0)) BoxIntegral.BoxAdditiveMap.volume

On positive intervals, oriented gauge integrability is existing box integrability.

theorem TauCeti.BoxIntegral.henstockIntervalIntegrable_iff_of_gt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hba : b < a) : HenstockIntervalIntegrable f a b ↔ BoxIntegral.Integrable (intervalBox b a hba) BoxIntegral.IntegrationParams.Henstock (fun (x : Fin 1 → ℝ) => f (x 0)) BoxIntegral.BoxAdditiveMap.volume

On negative intervals, oriented gauge integrability is existing box integrability.

@[simp]

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_same {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a : ℝ} {y : E} : HasHenstockIntervalIntegral f a a y ↔ y = 0

@[simp]

theorem TauCeti.BoxIntegral.henstockIntervalIntegrable_refl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a : ℝ) : HenstockIntervalIntegrable f a a

Every raw function is gauge integrable on a zero-length interval.

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_refl {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (f : ℝ → E) (a : ℝ) : HasHenstockIntervalIntegral f a a 0

Every raw function has integral zero over a zero-length parameter interval.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {y : E} (h : HasHenstockIntervalIntegral f a b y) : HasHenstockIntervalIntegral f b a (-y)

Reversing the parameter interval negates its actual gauge integral.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.unique {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {y z : E} (h : HasHenstockIntervalIntegral f a b y) (h' : HasHenstockIntervalIntegral f a b z) : y = z

Gauge interval integral values are unique, for either orientation.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.henstockIntervalIntegrable {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {y : E} (h : HasHenstockIntervalIntegral f a b y) : HenstockIntervalIntegrable f a b

Existence of a gauge interval value supplies genuine integrability.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.congr {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {a b : ℝ} {y : E} (h : HasHenstockIntervalIntegral f a b y) (hfg : Set.EqOn f g (Set.uIcc a b)) : HasHenstockIntervalIntegral g a b y

Changing a raw integrand outside the unoriented interval changes no Henstock value.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.congr_ae {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {a b : ℝ} {y : E} (h : HasHenstockIntervalIntegral f a b y) (hfg : f =ᵐ[MeasureTheory.volume.restrict (Set.uIoc a b)] g) : HasHenstockIntervalIntegral g a b y

Almost-everywhere equal integrands have the same oriented Henstock value.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {a b : ℝ} {y z : E} (hf : HasHenstockIntervalIntegral f a b y) (hg : HasHenstockIntervalIntegral g a b z) : HasHenstockIntervalIntegral (fun (t : ℝ) => f t + g t) a b (y + z)

Addition is valid without absolute or Bochner integrability.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {y : E} (hf : HasHenstockIntervalIntegral f a b y) (r : ℝ) : HasHenstockIntervalIntegral (fun (t : ℝ) => r • f t) a b (r • y)

Scalar multiplication of an oriented gauge integral.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {y : E} (hf : HasHenstockIntervalIntegral f a b y) : HasHenstockIntervalIntegral (fun (t : ℝ) => -f t) a b (-y)

Negation of an oriented gauge integrand.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {a b : ℝ} {y z : E} (hf : HasHenstockIntervalIntegral f a b y) (hg : HasHenstockIntervalIntegral g a b z) : HasHenstockIntervalIntegral (fun (t : ℝ) => f t - g t) a b (y - z)

Subtraction of oriented gauge integrals.

theorem TauCeti.BoxIntegral.HenstockIntervalIntegrable.symm {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (h : HenstockIntervalIntegrable f a b) : HenstockIntervalIntegrable f b a

Reversing endpoints preserves existence of an oriented gauge integral.

theorem TauCeti.BoxIntegral.HenstockIntervalIntegrable.add {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {a b : ℝ} (hf : HenstockIntervalIntegrable f a b) (hg : HenstockIntervalIntegrable g a b) : HenstockIntervalIntegrable (fun (t : ℝ) => f t + g t) a b

Addition preserves existence of oriented gauge integrals.

theorem TauCeti.BoxIntegral.HenstockIntervalIntegrable.smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hf : HenstockIntervalIntegrable f a b) (r : ℝ) : HenstockIntervalIntegrable (fun (t : ℝ) => r • f t) a b

Scalar multiplication preserves existence of an oriented gauge integral.

theorem TauCeti.BoxIntegral.HenstockIntervalIntegrable.neg {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} (hf : HenstockIntervalIntegrable f a b) : HenstockIntervalIntegrable (fun (t : ℝ) => -f t) a b

Negation preserves existence of an oriented Henstock integral.

theorem TauCeti.BoxIntegral.HenstockIntervalIntegrable.sub {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f g : ℝ → E} {a b : ℝ} (hf : HenstockIntervalIntegrable f a b) (hg : HenstockIntervalIntegrable g a b) : HenstockIntervalIntegrable (fun (t : ℝ) => f t - g t) a b

Subtraction preserves existence of oriented Henstock integrals.

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_const {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (v : E) (a b : ℝ) : HasHenstockIntervalIntegral (fun (x : ℝ) => v) a b ((b - a) • v)

A constant has oriented Henstock integral (b - a) • v for every pair of endpoints, without any completeness assumption on its values.

@[simp]

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_zero {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (a b : ℝ) : HasHenstockIntervalIntegral 0 a b 0

The zero function has oriented Henstock integral zero for every pair of endpoints.

theorem IntervalIntegrable.hasHenstockIntervalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} [CompleteSpace E] (hf : IntervalIntegrable f MeasureTheory.volume a b) : TauCeti.BoxIntegral.HasHenstockIntervalIntegral f a b (∫ (t : ℝ) in a..b, f t)

Bochner integrability supplies the genuine oriented Henstock value, including zero and reversed intervals.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.eq_intervalIntegral {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {y : E} [CompleteSpace E] (h : HasHenstockIntervalIntegral f a b y) (hf : IntervalIntegrable f MeasureTheory.volume a b) : y = ∫ (t : ℝ) in a..b, f t

Under genuine Bochner integrability, the oriented gauge value agrees with intervalIntegral.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.henstockIntervalIntegrable_of_subset {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b c d : ℝ} {y : E} [CompleteSpace E] (h : HasHenstockIntervalIntegral f a b y) (hcd : Set.uIcc c d ⊆ Set.uIcc a b) : HenstockIntervalIntegrable f c d

Genuine conditional Henstock integrability restricts to any oriented subinterval.

theorem TauCeti.BoxIntegral.HenstockIntervalIntegrable.mono_set {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b c d : ℝ} [CompleteSpace E] (h : HenstockIntervalIntegrable f a b) (hcd : Set.uIcc c d ⊆ Set.uIcc a b) : HenstockIntervalIntegrable f c d

Integrability, without a named value, also restricts to every oriented subinterval.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.split_of_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b c : ℝ} {y : E} [CompleteSpace E] (h : HasHenstockIntervalIntegral f a b y) (hac : a ≤ c) (hcb : c ≤ b) : ∃ (y₁ : E) (y₂ : E), HasHenstockIntervalIntegral f a c y₁ ∧ HasHenstockIntervalIntegral f c b y₂ ∧ y₁ + y₂ = y

Splitting a gauge-integrable positively oriented interval gives actual integrals on both pieces whose values add to the original value, without a Bochner-integrability assumption.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.split {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b c : ℝ} {y : E} [CompleteSpace E] (h : HasHenstockIntervalIntegral f a b y) (hc : c ∈ Set.uIcc a b) : ∃ (y₁ : E) (y₂ : E), HasHenstockIntervalIntegral f a c y₁ ∧ HasHenstockIntervalIntegral f c b y₂ ∧ y₁ + y₂ = y

Splitting at any point of the unoriented interval preserves the original orientation. The two actual gauge values add to the value of the whole interval.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b c : ℝ} {y z : E} [CompleteSpace E] (h₁ : HasHenstockIntervalIntegral f a c y) (h₂ : HasHenstockIntervalIntegral f c b z) : HasHenstockIntervalIntegral f a b (y + z)

Local conditional Henstock integrals glue across any intermediate parameter, including backtracking beyond either endpoint. No integrability on the whole interval is assumed.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.split_fin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {y : E} [CompleteSpace E] {N : ℕ} {s : Fin (N + 1) → ℝ} (h : HasHenstockIntervalIntegral f (s 0) (s (Fin.last N)) y) (hs : ∀ (i : Fin (N + 1)), s i ∈ Set.uIcc (s 0) (s (Fin.last N))) : ∃ (v : Fin N → E), (∀ (i : Fin N), HasHenstockIntervalIntegral f (s i.castSucc) (s i.succ) (v i)) ∧ ∑ i : Fin N, v i = y

Any finite subdivision whose nodes lie in the endpoint interval admits actual gauge values on its pieces whose sum is the value on the whole interval. Nodes may repeat and backtrack.

theorem TauCeti.BoxIntegral.HenstockIntervalIntegrable.trans {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b c : ℝ} [CompleteSpace E] (h₁ : HenstockIntervalIntegrable f a c) (h₂ : HenstockIntervalIntegrable f c b) : HenstockIntervalIntegrable f a b

Gauge integrability on adjacent parameter intervals glues, including backtracking.

theorem TauCeti.BoxIntegral.HasHenstockIntervalIntegral.add_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} {a b c : ℝ} {y : E} [CompleteSpace E] (h : HasHenstockIntervalIntegral f a b y) {y₁ y₂ : E} (h₁ : HasHenstockIntervalIntegral f a c y₁) (h₂ : HasHenstockIntervalIntegral f c b y₂) : y₁ + y₂ = y

The oriented additivity identity holds at any intermediate parameter, including backtracking.

theorem TauCeti.BoxIntegral.hasHenstockIntervalIntegral_of_subdivision {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {f : ℝ → E} [CompleteSpace E] {N : ℕ} {s : Fin (N + 1) → ℝ} {v : Fin N → E} (hv : ∀ (i : Fin N), HasHenstockIntervalIntegral f (s i.castSucc) (s i.succ) (v i)) : HasHenstockIntervalIntegral f (s 0) (s (Fin.last N)) (∑ i : Fin N, v i)

Conditional Henstock integrals on a finite sequence of parameter intervals glue to the sum of their values. The nodes may repeat, reverse direction, and leave the endpoint interval.