Function.Periodic.intervalIntegral_add_eq_of_pos
theorem Function.Periodic.intervalIntegral_add_eq_of_pos :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {T : ℝ},
Function.Periodic f T → 0 < T → ∀ (t s : ℝ), ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
This theorem states that if a function `f` from the reals to a normed additively commutative group `E` is periodic with a positive period `T`, then the integral of `f` over any interval of length `T` is the same, regardless of where that interval starts. More formally, for any real numbers `t` and `s`, the integral of `f` from `t` to `t + T` is equal to the integral of `f` from `s` to `s + T`.
More concisely: If `f` is a real-valued periodic function with period `T`, then for all real numbers `t` and `s`, the integral of `f` from `t` to `t + T` equals the integral of `f` from `s` to `s + T`.
|
AddCircle.measurePreserving_mk
theorem AddCircle.measurePreserving_mk :
∀ (T : ℝ) [hT : Fact (0 < T)] (t : ℝ),
MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.volume.restrict (Set.Ioc t (t + T)))
MeasureTheory.volume
This theorem states that the canonical map from the real numbers `ℝ` to the additive circle, which is the quotient of `ℝ` by the subgroup `ℤ ∙ T`, preserves the measure. This is considered in relation to the standard measure, defined to be the Haar measure of total mass `T` on the additive circle. The measure on `ℝ` is the restriction of the Lebesgue measure to the interval `(t, t + T]`. In other words, for all real numbers `T` greater than 0 and `t`, the map `QuotientAddGroup.mk` is measure-preserving under the given conditions.
More concisely: The map from the real numbers to the additive circle quotient, induced by `QuotientAddGroup.mk`, preserves the restriction of Lebesgue measure to intervals of length `T` when considered as the Haar measure on the additive circle.
|
AddCircle.measurable_mk'
theorem AddCircle.measurable_mk' : ∀ {a : ℝ}, Measurable QuotientAddGroup.mk
The theorem `AddCircle.measurable_mk'` states that for all real numbers `a`, the function `QuotientAddGroup.mk` is measurable. In mathematical terms, the canonical map from an additive group `α` to the quotient `α ⧸ s` respects the property of measurability. That means, for any subset of the quotient space that is measurable, the preimage of this set under the canonical map is also measurable in the original additive group.
More concisely: The canonical map from an additive group to its quotient by a subgroup preserves measurability of subsets.
|
AddCircle.measure_univ
theorem AddCircle.measure_univ : ∀ (T : ℝ) [hT : Fact (0 < T)], ↑↑MeasureTheory.volume Set.univ = ENNReal.ofReal T := by
sorry
This theorem, `AddCircle.measure_univ`, states that for any real number `T` for which there is a fact proving that it's positive (`0 < T`), the measure of the universal set, which includes all elements of a certain type, is equal to the nonnegative extended real number representation of `T`. In other words, when measuring the size of the universal set under the `MeasureTheory.volume`, it will always be equivalent to `T` if `T` is nonnegative, or to `0` if `T` is negative.
More concisely: For any positive real number `T`, the measure of the universal set under `MeasureTheory.volume` is equal to the nonnegative extended real number `T`.
|
Function.Periodic.intervalIntegral_add_eq_add
theorem Function.Periodic.intervalIntegral_add_eq_add :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {T : ℝ},
Function.Periodic f T →
∀ (t s : ℝ),
(∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.volume t₁ t₂) →
∫ (x : ℝ) in t..s + T, f x = (∫ (x : ℝ) in t..s, f x) + ∫ (x : ℝ) in t..t + T, f x
This theorem states that if we have a function `f` that is periodic with period `T` and integrable over an interval, then the integral of `f` over the interval `[t, s + T]` is equal to the sum of the integrals of `f` over the intervals `[t, s]` and `[t, t + T]`. In essence, this theorem relates the integral of a periodic function over a shifted interval to the integrals over the original and shifted periods.
More concisely: If a periodic function `f` with period `T` is integrable over an interval, then the integral of `f` over `[t, s + T]` equals the sum of the integrals of `f` over `[t, s]` and `[s, s + T]`.
|
UnitAddCircle.measurePreserving_mk
theorem UnitAddCircle.measurePreserving_mk :
∀ (t : ℝ),
MeasureTheory.MeasurePreserving QuotientAddGroup.mk (MeasureTheory.volume.restrict (Set.Ioc t (t + 1)))
MeasureTheory.volume
This theorem states that the canonical mapping from the real numbers (ℝ) to the quotient group of real numbers modulo integers (ℝ/ℤ), often referred to as the "unit additive circle", preserves measure. More specifically, it says that when considering the standard measure on the additive circle (defined to be the Haar measure of total mass 1) and the restriction of Lebesgue measure on ℝ to an interval (t, t + 1], the map preserves this measure for all real numbers t. This essentially means that the "size" or "volume" of a set does not change when transferred from ℝ to ℝ/ℤ via this map.
More concisely: The canonical mapping from the real numbers to the additive circle preserves the restriction of Lebesgue measure to intervals, i.e., the measure of a set on the real numbers equals the measure of its image under this mapping on the additive circle.
|
Function.Periodic.sInf_add_zsmul_le_integral_of_pos
theorem Function.Periodic.sInf_add_zsmul_le_integral_of_pos :
∀ {T : ℝ} {g : ℝ → ℝ},
Function.Periodic g T →
(∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) →
0 < T →
∀ (t : ℝ),
sInf ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Set.Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x ≤
∫ (x : ℝ) in 0 ..t, g x
The theorem `Function.Periodic.sInf_add_zsmul_le_integral_of_pos` states that given a real valued function `g` that is periodic with a positive period `T`, for any real number `t`, the function mapping `t` to the integral of `g` from `0` to `t` has a lower bound. This lower bound is given by the function `t ↦ X + ⌊t/T⌋ • Y`, where `X` and `Y` are constants. Here, `X` is the greatest lower bound of the set of all integrals of `g` over the interval from `0` to `T`, and `Y` is the integral of `g` over the same interval. The theorem requires that `g` is 'interval integrable', meaning that it can be integrated over any interval between any pair of real numbers.
More concisely: Given a real-valued, periodic function `g` with period `T` and integrable over any interval, the function mapping `t` to the integral of `g` from `0` to `t` has a lower bound `X + ⌊t/T⌋ • Y`, where `X` is the integral of `g` over `[0, T]` and `Y` is a constant.
|
Function.Periodic.integral_le_sSup_add_zsmul_of_pos
theorem Function.Periodic.integral_le_sSup_add_zsmul_of_pos :
∀ {T : ℝ} {g : ℝ → ℝ},
Function.Periodic g T →
(∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) →
0 < T →
∀ (t : ℝ),
∫ (x : ℝ) in 0 ..t, g x ≤
sSup ((fun t => ∫ (x : ℝ) in 0 ..t, g x) '' Set.Icc 0 T) + ⌊t / T⌋ • ∫ (x : ℝ) in 0 ..T, g x
This theorem states that if a function `g : ℝ → ℝ` is periodic with a positive period `T`, then for any real number `t`, the integral of `g` from `0` to `t` is bounded above. Specifically, the integral is less than or equal to `X + ⌊t/T⌋ * Y`, where `X` is the supremum of the set of integrals of `g` from `0` to `t` over the interval from `0` to `T`, and `Y` is the integral of `g` from `0` to `T`. This upper bound holds regardless of the specific value of `t`. The theorem also requires that `g` is interval integrable for any two real numbers `t₁` and `t₂`.
More concisely: If a real-valued function `g` is periodic with positive period `T` and is integrable over any interval of length `T`, then for any real number `t`, the integral of `g` from `0` to `t` is bounded above by the supremum of integrals of `g` over intervals of length `T` plus `⌊t/T⌋` times the integral of `g` over one period.
|
AddCircle.intervalIntegral_preimage
theorem AddCircle.intervalIntegral_preimage :
∀ (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (t : ℝ)
(f : AddCircle T → E), ∫ (a : ℝ) in t..t + T, f ↑a = ∫ (b : AddCircle T), f b
The theorem `AddCircle.intervalIntegral_preimage` states that for any real number T greater than 0, and any function f from the additive circle of T to a normed additive commutative group with a normed real number space, the integral of f over an interval (t, t + T] in real numbers is equal to the integral of f over the AddCircle T. Here, the 'additive circle' of T is a quotient of the real numbers by the integer multiples of T. Essentially, this theorem is about equating the integral of a function over a segment of real numbers and its respective projection on the additive circle.
More concisely: For any real number T > 0 and any function f from the additive circle of T to a normed additive commutative group with a real normed space, the integral of f over (t, t + T] equals the integral of its restriction to the additive circle of T.
|
UnitAddCircle.lintegral_preimage
theorem UnitAddCircle.lintegral_preimage :
∀ (t : ℝ) (f : UnitAddCircle → ENNReal), ∫⁻ (a : ℝ) in Set.Ioc t (t + 1), f ↑a = ∫⁻ (b : UnitAddCircle), f b := by
sorry
This theorem states that for any real number `t` and any function `f` from the unit circle in the additive group of real numbers modulo integers (`UnitAddCircle`) to the extended nonnegative real numbers (`ENNReal`), the integral of `f` over the interval `(t, t + 1]` in the real numbers, when `f` is lifted to the real numbers, is equal to the integral of `f` over the entire `UnitAddCircle`. In other words, given a function defined on the unit circle in the additive group of real numbers modulo integers, the integral of this function over a one-unit length interval in the real numbers is the same as the integral of the function over the whole circle when the function is appropriately lifted from the circle to the real numbers.
More concisely: For any real-valued function `f` on the unit circle in the additive group of real numbers modulo integers, the integral of `f` over one unit length in the real numbers equals the integral of the lifted function over the entire unit circle.
|
AddCircle.lintegral_preimage
theorem AddCircle.lintegral_preimage :
∀ (T : ℝ) [hT : Fact (0 < T)] (t : ℝ) (f : AddCircle T → ENNReal),
∫⁻ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫⁻ (b : AddCircle T), f b
The theorem `AddCircle.lintegral_preimage` states that: for any positive real number `T`, and any real number `t`, the lower integral (denoted by `∫⁻`) of a function `f` over the additive circle `AddCircle T` (which is a quotient set representing the real line modulo `T`), is identical to the lower integral over the interval `(t, t + T]` in the real numbers of the lift of `f` to the real numbers. In other words, integrating `f` over a single period `(t, t + T]` in the real numbers gives the same result as integrating `f` over the whole additive circle. This theorem essentially establishes the invariance of the lower integral under changes in the domain from an interval in the real line to the additive circle.
More concisely: The lower integral of a function over an additive circle is equal to the lower integral over the corresponding interval in the real numbers for any positive real period.
|
UnitAddCircle.intervalIntegral_preimage
theorem UnitAddCircle.intervalIntegral_preimage :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (t : ℝ) (f : UnitAddCircle → E),
∫ (a : ℝ) in t..t + 1, f ↑a = ∫ (b : UnitAddCircle), f b
The theorem `UnitAddCircle.intervalIntegral_preimage` states that for any real number `t` and any function `f` from the unit additive circle (which is a set of real numbers modulo 1) to a normed vector space `E` over the reals, the integral of `f` over the interval `(t, t + 1]` in the real numbers, where `f` is lifted to the reals, is equal to the integral of `f` over the entire unit additive circle. This is true for almost-everywhere strongly measurable functions `f`.
More concisely: For almost-everywhere strongly measurable functions `f` from the unit additive circle to a normed vector space over the reals, the integral of `f` over an interval `(t, t+1]` equals the integral of `f` over the entire unit additive circle.
|
Function.Periodic.tendsto_atTop_intervalIntegral_of_pos
theorem Function.Periodic.tendsto_atTop_intervalIntegral_of_pos :
∀ {T : ℝ} {g : ℝ → ℝ},
Function.Periodic g T →
(∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) →
0 < ∫ (x : ℝ) in 0 ..T, g x →
0 < T → Filter.Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) Filter.atTop Filter.atTop
This theorem states that if a real-valued function `g` is periodic with a positive period `T`, and the integral of `g` over the interval `0` to `T` is positive, then the function that maps a real number `t` to the integral of `g` from `0` to `t` tends to positive infinity as `t` itself tends to positive infinity. It also requires that `g` is interval integrable for any interval `[t1, t2]` with respect to the Lebesgue measure.
More concisely: If `g` is a real-valued, periodic function with positive period `T` that is interval integrable over any `[t1, t2]` and has a positive integral over `[0, T]`, then the function that maps `t` to the integral of `g` from `0` to `t` approaches positive infinity as `t` approaches positive infinity.
|
UnitAddCircle.integral_preimage
theorem UnitAddCircle.integral_preimage :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (t : ℝ) (f : UnitAddCircle → E),
∫ (a : ℝ) in Set.Ioc t (t + 1), f ↑a = ∫ (b : UnitAddCircle), f b
This theorem asserts that for any real number `t` and any function `f` mapping from the unit addition circle to a normed space over the real numbers, the integral of the function over the unit addition circle is equal to the integral over the interval (t, t + 1) in the real numbers of the lifted function. Here, lifting refers to the process of taking a function defined on the unit addition circle and extending it to a function defined on the real numbers. The unit addition circle is defined as the real numbers modulo 1, which essentially "wraps" the real line around the unit circle. The interval (t, t + 1) is a subset of the real numbers that includes all numbers strictly greater than `t` and less than or equal to `t + 1`.
More concisely: For any real number `t` and continuous function `f` from the unit circle to a normed space, the integral of `f` over the unit circle is equal to the integral of the lifted function `f` over the real interval (t, t+1).
|
AddCircle.integral_preimage
theorem AddCircle.integral_preimage :
∀ (T : ℝ) [hT : Fact (0 < T)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (t : ℝ)
(f : AddCircle T → E), ∫ (a : ℝ) in Set.Ioc t (t + T), f ↑a = ∫ (b : AddCircle T), f b
This theorem, named as `AddCircle.integral_preimage`, states that for any positive real number `T`, and for any `t` in real numbers, if we have a function `f` from the additive circle of `T` to a normed additive commutative group `E` over real numbers, then the integral of `f` over the interval `(t, t + T]` is equivalent to the integral of `f` over the entire additive circle of `T`. Here, the additive circle of `T` is essentially the real numbers modulo the integer multiples of `T`, and the interval `(t, t + T]` is a left-open right-closed interval in real numbers. This theorem links the concept of integration over an "additive circle" (or a circle in the additive group of real numbers) to the more familiar concept of integration over a real interval.
More concisely: For any positive real number `T`, any `t` in real numbers, and any integrable function `f` from the additive circle of `T` to a normed additive commutative group over real numbers, the integral of `f` over the interval `(t, t + T]` is equal to the integral of `f` over the entire additive circle of `T`.
|
Function.Periodic.intervalIntegral_add_eq
theorem Function.Periodic.intervalIntegral_add_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {T : ℝ},
Function.Periodic f T → ∀ (t s : ℝ), ∫ (x : ℝ) in t..t + T, f x = ∫ (x : ℝ) in s..s + T, f x
The theorem `Function.Periodic.intervalIntegral_add_eq` states that if a function `f` is periodic with a period `T`, then the integral of `f` over the interval `[t, t + T]` is independent of the choice of `t`. In other words, for any real numbers `t` and `s`, the integral of `f` from `t` to `t + T` is equal to the integral of `f` from `s` to `s + T`. This means that the area under the curve of `f` in one period is the same no matter where the period starts.
More concisely: Given a real-valued function `f` that is periodic with period `T`, the integral of `f` over the interval `[t, t + T]` is equal to the integral of `f` over the interval `[s, s + T]` for any real numbers `s` and `t`.
|
Function.Periodic.intervalIntegral_add_zsmul_eq
theorem Function.Periodic.intervalIntegral_add_zsmul_eq :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {T : ℝ},
Function.Periodic f T →
∀ (n : ℤ) (t : ℝ),
(∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.volume t₁ t₂) →
∫ (x : ℝ) in t..t + n • T, f x = n • ∫ (x : ℝ) in t..t + T, f x
The theorem states that if `f` is an integrable periodic function with period `T`, then the integral of `f` over the interval `[t, t + nT]` is `n` times the integral of `f` over the interval `[t, t + T]`, for any integer `n` and any real number `t`. Here, `n • T` and `n • ∫ (x : ℝ) in t..t + T, f x` represent the scalar multiplication of the integer `n` with the real number `T` and the integral of `f` over `[t, t + T]`, respectively. The scalar multiplication `n • T` extends the interval `[t, t + T]` `n` times. The condition `∀ (t₁ t₂ : ℝ), IntervalIntegrable f MeasureTheory.volume t₁ t₂` ensures that `f` is interval integrable with respect to the Lebesgue measure on any real interval `[t₁, t₂]`.
More concisely: If `f` is a periodic integrable function with period `T`, then the integral of `f` over any interval of length `nT` starting at `t` is `n` times the integral of `f` over one period `[t, t + T]`.
|
Function.Periodic.tendsto_atTop_intervalIntegral_of_pos'
theorem Function.Periodic.tendsto_atTop_intervalIntegral_of_pos' :
∀ {T : ℝ} {g : ℝ → ℝ},
Function.Periodic g T →
(∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) →
(∀ (x : ℝ), 0 < g x) → 0 < T → Filter.Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) Filter.atTop Filter.atTop
This theorem states that if a function `g : ℝ → ℝ` is periodic with a positive period `T > 0` and all values of the function are positive (`∀ x, 0 < g x`), then the function that maps a real number `t` to the integral of `g` from `0` to `t` tends to infinity as `t` tends to infinity. This is denoted as `t ↦ ∫ x in 0..t, g x` tending to `∞` as `t` tends to `∞`. The theorem also assumes that `g` is interval integrable with respect to the Lebesgue measure on any interval `[t₁, t₂]`.
More concisely: If `g : ℝ → ℝ` is a positive, periodic function with period `T > 0` that is integrable on any interval, then the integral of `g` from `0` to `t` tends to infinity as `t` tends to infinity.
|
Function.Periodic.tendsto_atBot_intervalIntegral_of_pos'
theorem Function.Periodic.tendsto_atBot_intervalIntegral_of_pos' :
∀ {T : ℝ} {g : ℝ → ℝ},
Function.Periodic g T →
(∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) →
(∀ (x : ℝ), 0 < g x) → 0 < T → Filter.Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) Filter.atBot Filter.atBot
The theorem `Function.Periodic.tendsto_atBot_intervalIntegral_of_pos'` states that if `g` is a function from real numbers to real numbers that is periodic with a positive period `T`, is interval integrable with respect to Lebesgue measure for any two real numbers, and for all `x`, `g(x)` is positive, then the function that maps `t` to the integral of `g` from `0` to `t` tends to negative infinity as `t` tends to negative infinity. In other words, the integral of a positive, periodic function over the interval from `0` to `t` decreases without bound as `t` decreases.
More concisely: Given a positive, periodic real-valued function `g` with period `T`, if `g` is integrable for all intervals `[0, t]` and `g(x) > 0` for all `x`, then the integral `∫[0,t] g(s) ds` tends to negative infinity as `t` tends to negative infinity.
|
Function.Periodic.tendsto_atBot_intervalIntegral_of_pos
theorem Function.Periodic.tendsto_atBot_intervalIntegral_of_pos :
∀ {T : ℝ} {g : ℝ → ℝ},
Function.Periodic g T →
(∀ (t₁ t₂ : ℝ), IntervalIntegrable g MeasureTheory.volume t₁ t₂) →
0 < ∫ (x : ℝ) in 0 ..T, g x →
0 < T → Filter.Tendsto (fun t => ∫ (x : ℝ) in 0 ..t, g x) Filter.atBot Filter.atBot
The theorem states that if a real-valued function `g` is periodic with a positive period `T` and the integral of `g` from 0 to `T` is positive, then the function `t ↦ ∫ x in 0..t, g x` (representing the integral of `g` from 0 to `t`) tends to negative infinity as `t` tends to negative infinity. In other words, as we move `t` further into the negative numbers, the accumulated area under the curve of `g` from 0 to `t` keeps decreasing without bound. This holds for all `t₁` and `t₂` such that `g` is interval integrable over the interval from `t₁` to `t₂` with respect to the Lebesgue measure.
More concisely: If a real-valued, periodic function `g` with positive period `T` and integrable over any interval with positive integral from 0 to `T` decreases without bound as `t` approaches negative infinity when integrating `g` over the interval [0, `t`].
|