lp.memℓp_of_tendsto
theorem lp.memℓp_of_tendsto :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_3}
{l : Filter ι} [inst_1 : l.NeBot] [_i : Fact (1 ≤ p)] {F : ι → ↥(lp E p)},
Bornology.IsBounded (Set.range F) →
∀ {f : (a : α) → E a}, Filter.Tendsto (id fun i => ↑(F i)) l (nhds f) → Memℓp f p
The theorem `lp.memℓp_of_tendsto` asserts that, for any nonnegative real number `p` (which may be infinite), a normed add commutative group `E` indexed by `α`, a filter `l` over some type `ι` that is not minimal (not empty or does not contain only the empty set), and a sequence `F` in the `lp` space `E` indexed by `ι`, if `F` is a bounded sequence (i.e., every subset of the codomain of `F` is cobounded) and the limit of `F` exists and equals to a function `f` for the pointwise convergence (i.e., for every neighborhood of `f`, the preimage under `F` of that neighborhood is a neighborhood in the filter `l`), then the function `f` belongs to the `lp` space `E` with exponent `p`. This `lp` space membership means that `f` is finitely supported if `p = 0`, has an upper bound for the norm of its values if `p = ∞`, or the `p`-th power sum of its norms is summable if `0 < p < ∞`.
More concisely: If a bounded sequence in an `lp` space indexed by a non-minimal filter converges pointwise to a function, then the limit is an element of the `lp` space with the same exponent.
|
lp.norm_rpow_eq_tsum
theorem lp.norm_rpow_eq_tsum :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
0 < p.toReal → ∀ (f : ↥(lp E p)), ‖f‖ ^ p.toReal = ∑' (i : α), ‖↑f i‖ ^ p.toReal
The theorem `lp.norm_rpow_eq_tsum` states that for any type `α`, any function `E` from `α` to some type, any extended nonnegative real number `p` with a positive real part, and any normed additive commutative group indexed by `α`, if `f` is an element of the `lp` space for `E` and `p`, then the norm of `f` raised to the power of the real part of `p` is equal to the sum over all `α` of the norm of `f` at `i` raised to the power of the real part of `p`. In mathematical terms, this says ⟦f⟧^p = ∑ᵢ(|f(i)|^p), where ⟦f⟧ is the norm of `f`, |f(i)| is the absolute value of `f` at `i`, and the sum is over all `i` in `α`.
More concisely: For any `α`, `E : α → Type`, extended nonnegative real `p` with positive real part, `lp` space `f` over `(α, E)` for norm and `p`, the norm of `f` raised to the power of the real part of `p` equals the sum over all `i` in `α` of the norm of `f` at `i` raised to the power of the real part of `p`.
|
memℓp_zero_iff
theorem memℓp_zero_iff :
∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
Memℓp f 0 ↔ {i | f i ≠ 0}.Finite
The theorem `memℓp_zero_iff` states that for any type `α`, a function `f` from `α` to a normed addition commutative group `E`, `f` belongs to `ℓp` space with `p = 0` if and only if the set of all `i` in `α` for which `f(i)` is not equal to zero is finite. In other words, a function `f` has the `ℓp` property with `p = 0` exactly when `f` is finitely supported. Here, `ℓp` space is a generalization of sequence spaces including `ℓ∞` (the space of bounded sequences) and `ℓ1` (the space of absolutely convergent series), defined for any real number `p ≥ 0`.
More concisely: A function from a type to a normed additive commutative group belongs to the ℓp space with p = 0 if and only if it has a finite number of non-zero values.
|
lp.norm_apply_le_norm
theorem lp.norm_apply_le_norm :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
p ≠ 0 → ∀ (f : ↥(lp E p)) (i : α), ‖↑f i‖ ≤ ‖f‖
This theorem is stating that for any type `α`, any function `E` from `α` to another type, and any extended nonnegative real number `p` that is not zero, if each `E i` is a normed additive commutative group, then for every function `f` in the LP space and every `i` in `α`, the norm of `f i` is less than or equal to the norm of `f`. In other words, the norm of the value of a function at a point in an LP space is always less than or equal to the norm of the function itself.
More concisely: For any function `f` in an LP space and any type `α` with each `E i` an additive commutative normed group, the norm of `f i` is less than or equal to the norm of `f` for all `i` in `α`.
|
lp.norm_le_of_tendsto
theorem lp.norm_le_of_tendsto :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {ι : Type u_3}
{l : Filter ι} [inst_1 : l.NeBot] [_i : Fact (1 ≤ p)] {C : ℝ} {F : ι → ↥(lp E p)},
(∀ᶠ (k : ι) in l, ‖F k‖ ≤ C) → ∀ {f : ↥(lp E p)}, Filter.Tendsto (id fun i => ↑(F i)) l (nhds ↑f) → ‖f‖ ≤ C
The theorem "lp.norm_le_of_tendsto" is about the semicontinuity of the `lp` norm. It states that for any type `α`, function `E` from `α` to another type, extended nonnegative real number `p`, normed add commutative group `(E i)`, type `ι`, filter `l` on `ι`, a real number `C` and a sequence `F` of elements from `lp E p`: if all sufficiently large elements of the sequence `F` have `lp` norm less than or equal to `C`, and if the pointwise limit `f` of the sequence `F` with respect to the filter `l` exists (i.e., as `i` tends to `l`, `F i` tends to `f`), then the `lp` norm of `f` is also less than or equal to `C`. In mathematical terms, $\|f\|_{p} \leq C$ if $\lim_{i \to l} F(i)$ exists and $\|F(k)\|_{p} \leq C$ for all large enough `k`.
More concisely: Given a type `α`, function `E` from `α` to a normed add commutative group, extended nonnegative real number `p`, filter `l` on `ι`, sequence `F` of elements from `lp E p`, and real number `C`, if all sufficiently large elements of `F` have `lp` norm less than or equal to `C` and `F` converges to a limit `f` with respect to `l`, then `||f||_p ≤ C`.
|
Memℓp.const_smul
theorem Memℓp.const_smul :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {𝕜 : Type u_3}
[inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), BoundedSMul 𝕜 (E i)]
{f : (i : α) → E i}, Memℓp f p → ∀ (c : 𝕜), Memℓp (c • f) p
The theorem `Memℓp.const_smul` states that for any given type `α`, a function `f` from `α` to a type `E` (where `E` is a normed additive commutative group), an extended nonnegative real number `p`, a normed ring `𝕜`, a module structure over `𝕜` and `E`, and a bounded scalar multiplication operation, if `f` has the property `Memℓp` for the value `p`, then for any constant `c` in `𝕜`, the function resulting from scalar multiplication of `f` by `c` also has the property `Memℓp` for the same `p`.
The `Memℓp` property can have three different meanings depending on the value of `p`. If `p` is 0, `Memℓp` means that `f` is finitely supported. If `p` is ∞, `Memℓp` means that the set of the norms of `f` has an upper bound. If `p` is any other number between 0 and ∞, `Memℓp` means that the series formed by raising the norms of `f` to the power `p` is summable.
More concisely: If `f` is a function from type `α` to a normed additive commutative group `E` with the `Memℓp` property for some extended nonnegative real number `p`, then the scalar multiplication of `f` by any constant `c` in the normed ring `𝕜` also possesses the `Memℓp` property for the same `p`.
|
memℓp_zero
theorem memℓp_zero :
∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
{i | f i ≠ 0}.Finite → Memℓp f 0
The theorem `memℓp_zero` states that for any type `α`, any function `f : α → E i` from `α` to `E i` (where `E i` is a normed additive commutative group for each `i : α`), if the set of `i` such that `f i` is non-zero is finite, then `f` belongs to the space `ℓp` for `p = 0`. In mathematical terms, this means that a function is in the sequence space `ℓ^0` if and only if it is finitely supported.
More concisely: A function from a type to a normed additive commutative group belongs to the sequence space ℓ^0 if and only if its support is finite.
|
Memℓp.bddAbove
theorem Memℓp.bddAbove :
∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
Memℓp f ⊤ → BddAbove (Set.range fun i => ‖f i‖)
The theorem `Memℓp.bddAbove` states that for all types `α` and for all types `E` which depend on `α`, given a normed add commutative group structure on `E i` for every `i` in `α`, and a function `f` from `α` to `E i`, if `f` belongs to the space `ℓ∞` (denoted as `Memℓp f ⊤`), then the set formed by the range of the norm of `f`, i.e., the set of all `‖f i‖`, is bounded above. In simpler terms, if a function belongs to the space of bounded sequences, then the norms of its values form a set which has an upper bound.
More concisely: Given a normed add commutative group `E` indexed by a type `α`, and a function `f` from `α` to `E` belonging to `ℓ∞`, the set of norms `{||f i|| | i ∈ α}` is bounded above.
|
Memℓp.add
theorem Memℓp.add :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f g : (i : α) → E i},
Memℓp f p → Memℓp g p → Memℓp (f + g) p
The theorem `Memℓp.add` states that for any types `α` and `E` (where `E` is a function from `α` to some type), a nonnegative extended real number `p`, and any two functions `f` and `g` from `α` to `E`, if both `f` and `g` satisfy the `Memℓp` property with respect to `p`, then their sum `(f + g)` also satisfies the `Memℓp` property with respect to the same `p`. In other words, the `Memℓp` property is preserved under addition. In mathematical terms, this theorem says that if `f` and `g` are in the `ℓp` space (a space of sequences for which the `p`-th power of the absolute values is summable when `p` is between 0 and infinity, is finitely supported when `p = 0`, or admits an upper bound when `p = ∞`), then `f + g` is also in the `ℓp` space.
More concisely: If `f` and `g` are functions from a type `α` to a real or complex vector space, and `f`, `g`, and their sum belong to the `ℓp` space for some nonnegative extended real number `p`, then their sum also belongs to the `ℓp` space.
|
memℓp_infty
theorem memℓp_infty :
∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
BddAbove (Set.range fun i => ‖f i‖) → Memℓp f ⊤
The theorem `memℓp_infty` states that for any type `α` and for any function `f` from `α` to a normed add commutative group `E`, if the set of norms of `f i` for all `i` in `α` (i.e., `Set.range fun i => ‖f i‖`) is bounded above, then `f` belongs to the space `ℓp` for `p = ∞`. In other words, if there exists an upper bound for the norms of all values of `f`, then `f` is said to be in the `ℓ∞` space, which is the space of bounded functions.
More concisely: If the set of norms of a function from a type to a normed add commutative group is bounded, then the function belongs to the space of bounded functions (ℓ∞).
|
Memℓp.summable
theorem Memℓp.summable :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)],
0 < p.toReal → ∀ {f : (i : α) → E i}, Memℓp f p → Summable fun i => ‖f i‖ ^ p.toReal
The theorem `Memℓp.summable` asserts that for any type `α` and a function `E` mapping from `α` to another type, and given a nonnegative extended real number `p` and a set of `NormedAddCommGroup` instances indexed by `α`, if the real part of `p` is greater than zero, then for any function `f` from `α` to `E i` that satisfies the `Memℓp` property for `p`, the series formed by taking the norm of `f i` raised to the power of the real part of `p` for each `i` is summable. In other words, if the function `f` is in ℓp space (where the real part of `p` is greater than zero), then the series of its elements' norms raised to the power of `p` converges to a sum.
More concisely: If `α` is a type, `E` maps `α` to a `NormedAddCommGroup`, `p` is a nonnegative real number with positive real part, and `f : α → E i` satisfies the `Memℓp` property for `p`, then the series ∑ₙ(|f i(n)|ⁱ)⁺ p, where i ranges over `α` and n over ℕ, converges.
|
lp.norm_nonneg'
theorem lp.norm_nonneg' :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E p)),
0 ≤ ‖f‖
This theorem states that for any type `α`, any function `E` from `α` to another type, any extended nonnegative real `p`, and any instance of a normed add commutative group for every `i` in `α`, the norm of a function `f` that belongs to the `lp` space defined with `E` and `p` is always nonnegative. In other words, it asserts that the norm of any function in the `lp` space is always greater than or equal to zero, which is a fundamental property of norms in mathematical analysis.
More concisely: For any type `α`, function `E` from `α` to another type, normed add commutative group instance for each `i` in `α`, and extended nonnegative real `p`, the norm of any function `f` from `α` to the range of `E` belonging to the `lp` space is nonnegative.
|
lp.norm_eq_ciSup
theorem lp.norm_eq_ciSup :
∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E ⊤)),
‖f‖ = ⨆ i, ‖↑f i‖
This theorem, `lp.norm_eq_ciSup`, states that for any type `α`, a type `E` that varies with `α` , and any instance `inst` of the `NormedAddCommGroup` class for `E` such that `f` is an element of the `lp` space (with the supremum norm), the norm of `f` is equal to the supremum of the norms of the elements of `f`. In mathematical terms, this is stating that ‖f‖ = sup_{i} ‖f(i)‖ for f in the L^∞ space (the space of bounded sequences).
More concisely: For any type `α`, any `E` varying with `α` that is an `NormedAddCommGroup` with `lp` space element `f` having finite supremum norm, the norm of `f` equals the supremum of the norms of its elements.
|
Memℓp.neg
theorem Memℓp.neg :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
Memℓp f p → Memℓp (-f) p
The theorem `Memℓp.neg` states that for any type `α`, any function `E : α → Type` that maps `α` to a Normed Additive Commutative Group, any extended nonnegative real number `p`, and any function `f : (i : α) → E i`, if `f` belongs to `ℓp` (denoted as `Memℓp f p`), then the negation of `f` (denoted as `-f`) also belongs to `ℓp`. This means the property defined by `Memℓp` is preserved under negation of the function. This property is important in the context of sequences or series in functional analysis and measure theory, where `ℓp` spaces play a significant role.
More concisely: If `f : α → E α` belongs to the `ℓp` space with respect to aNormed Additive Commutative Group `E : α → Type`, then the negation of `f` also belongs to the `ℓp` space with respect to `E`.
|
lp.uniformContinuous_coe
theorem lp.uniformContinuous_coe :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 ≤ p)],
UniformContinuous Subtype.val
The theorem `lp.uniformContinuous_coe` states that for any type `α`, any function `E` from `α` to some type, and any extended nonnegative real number `p` that's greater than or equal to 1, the coercion from the space of `p`-integrable sequences (`lp E p`) to the function space `∀ i, E i` is uniformly continuous. In more details, if we have a normed additive commutative group structure on each `E i`, then for any pair of sequences in `lp E p` that are close to each other, their corresponding sequences in `∀ i, E i` are also close to each other, regardless of the specific position in the sequence `i`.
More concisely: For any type `α`, function `E` from `α` to some type, and extended nonnegative real number `p` ≥ 1, the coercion from the space of `p`-integrable sequences of `E` to the function space `∀ i, E i` is uniformly continuous, preserving the group structure on each `E i`.
|
Memℓp.finite_dsupport
theorem Memℓp.finite_dsupport :
∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
Memℓp f 0 → {i | f i ≠ 0}.Finite
The theorem `Memℓp.finite_dsupport` states that for any index set `α` and any type family `E` indexed by `α`, given any normed additive commutative group structure on the types `E i`, if a function `f` from index `i` in `α` to `E i` belongs to the set `Memℓp` for `p = 0`, then the set of indices `{i | f i ≠ 0}` where `f` is non-zero is finite. In other words, it means that `f` is finitely supported if it belongs to the `ℓp` space for `p = 0`.
More concisely: For any indexed type family `E` over a set `α` with normed additive commutative group structures, if a function `f` from `α` to `E` belongs to the `ℓp` space with `p = 0`, then the support of `f` is finite.
|
lp.hasSum_single
theorem lp.hasSum_single :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
[inst_1 : DecidableEq α] [inst_2 : Fact (1 ≤ p)],
p ≠ ⊤ → ∀ (f : ↥(lp E p)), HasSum (fun i => lp.single p i (↑f i)) f
The theorem `lp.hasSum_single` states that for any type `α`, function `E` from `α` to a type `u_2`, extended nonnegative real number `p`, normed add commutative group `E i` for each `i` in `α`, decidable equality on `α`, and a fact that `p` is greater than or equal to 1, if `p` is not `∞`, then for every element `f` of the extended nonnegative real number `lp E p`, the sum of `lp.single p i (↑f i)` for all `i` in `α` equals `f`. In other words, it asserts that the canonical finitely-supported approximations to an element `f` of `lp` converge to it in the `lp` topology.
More concisely: For any type `α`, function `E` from `α` to a type `u_2`, extended nonnegative real number `p` (not `∞`), normed add commutative group `E i` for each `i` in `α`, decidable equality on `α`, if `p ≥ 1`, then the sum of `lp.single p i (↑f i)` for all `i` in `α` equals `f` for every `f` in the extended nonnegative real number `lp E p`.
|
lp.memℓp
theorem lp.memℓp :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E p)),
Memℓp (↑f) p
This theorem states that for any type `α`, a function `E` mapping from `α` to another type, a nonnegative real number `p`, and an instance of `NormedAddCommGroup` for each `i` in `α`, if `f` is an element of the `lp` space with respect to `E` and `p`, then `f` satisfies the `Memℓp` property. In more mathematical terms, for `f` belonging to the `lp` space, if `p` equals 0, `f` is finitely supported; if `p` equals infinity, there exists an upper bound for the set of norms of `f`; if `p` is between 0 and infinity, the series of the `p`-th power of the norms of `f` is summable.
More concisely: If `f` is an element of the `lp` space with respect to a function `E` mapping from type `α` to another type, a nonnegative real number `p`, and instances of `NormedAddCommGroup` for each `i` in `α`, then `f` satisfies the `Memℓp` property with respect to `p`, i.e., it is finitely supported for `p` = 0, has an upper bound for the set of norms for `p` = ∞, and its series of `p`-th power norms is summable for 0 < `p` < ∞.
|
lp.isLUB_norm
theorem lp.isLUB_norm :
∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : Nonempty α]
(f : ↥(lp E ⊤)), IsLUB (Set.range fun i => ‖↑f i‖) ‖f‖
The theorem `lp.isLUB_norm` states that for any type `α` and a type `E` which is a function from `α` to a normed additive commutative group, given the condition that `α` is nonempty, for any element `f` of the lp space with `E` and `⊤` (`lp E ⊤`), the least upper bound (supremum) of the set of norms of elements `i` in `f` (`Set.range fun i => ‖↑f i‖`) is the norm of `f` itself (`‖f‖`). In simpler terms, this theorem asserts that the norm of `f` is the supremum of the norms of its elements.
More concisely: The norm of a vector in an lp space with respect to a function mapping elements to a normed additive commutative group is the supremum of the norms of its components.
|
memℓp_gen
theorem memℓp_gen :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
(Summable fun i => ‖f i‖ ^ p.toReal) → Memℓp f p
The theorem `memℓp_gen` states that for any type `α`, any normed group `E` indexed by `α`, any extended nonnegative real number `p`, and any function `f` from `α` to `E`, if the series formed by taking the p-th norm of each output of `f` and summing them is summable, then the function `f` is in the L^p space (denoted as `Memℓp f p`).
In other words, it's saying that if we can sum the p-th power of the norms of a function's values, then that function is said to be "p-integrable" or within the p-th L^p space, a concept used in functional analysis and measure theory.
More concisely: If a function from a type to a normed group has summable series of p-th powers of its values' norms, then the function belongs to the L^p space.
|
memℓp_infty_iff
theorem memℓp_infty_iff :
∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i},
Memℓp f ⊤ ↔ BddAbove (Set.range fun i => ‖f i‖)
The theorem `memℓp_infty_iff` states that for any types `α` and `E` (where `E` is a function from `α`), and for any instance of a normed add commutative group on `E`, and for any function `f` from `α` to `E`, the function `f` belongs to `ℓ^∞` (i.e., `f` is in `Memℓp` for `p = ∞`) if and only if the set of norms of `f` is bounded above (i.e., there exists an upper bound for the set of norms of `f`). In other words, a function `f` is in the space `ℓ^∞` if and only if the magnitudes of its values are bounded from above.
More concisely: A function from a type to a normed add commutative group belongs to the space `ℓ^∞` if and only if its norms are bounded above.
|
lp.tsum_mul_le_mul_norm
theorem lp.tsum_mul_le_mul_norm :
∀ {α : Type u_1} {E : α → Type u_2} [inst : (i : α) → NormedAddCommGroup (E i)] {p q : ENNReal},
p.toReal.IsConjExponent q.toReal →
∀ (f : ↥(lp E p)) (g : ↥(lp E q)),
(Summable fun i => ‖↑f i‖ * ‖↑g i‖) ∧ ∑' (i : α), ‖↑f i‖ * ‖↑g i‖ ≤ ‖f‖ * ‖g‖
The theorem `lp.tsum_mul_le_mul_norm` is a formal statement of the Hölder's inequality in the context of lp spaces. It states that for any types `α` and `E`, where each `E i` is a normed add commutative group, and for any extended nonnegative real numbers `p` and `q` that are conjugate exponents, for any functions `f` and `g` in the lp spaces defined by `E`, `p` and `q` respectively, the infinite sum of the product of the norms of `f i` and `g i` is summable, and the sum is at most the product of the norms of `f` and `g`. This theorem captures a fundamental property of functions in lp spaces, providing a bound on the sum of products of function values in terms of the overall norms of the functions.
More concisely: For any functions $f$ and $g$ in the $L^p$ and $L^q$ spaces, respectively, with conjugate exponents $p, q > 1$, the sum of the pointwise products of their norms satisfies $\left(\sum_{i}|f_i g_i|^p\right)^{\frac{1}{p}} \leq \left(\sum_{i}|f_i|^p\right)^{\frac{1}{p}}\left(\sum_{i}|g_i|^q\right)^{\frac{1}{q}}$.
|
lp.normedAddCommGroup.proof_1
theorem lp.normedAddCommGroup.proof_1 :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [hp : Fact (1 ≤ p)]
(f g : ↥(lp E p)), ‖f + g‖ ≤ ‖f‖ + ‖g‖
This theorem states that for any type `α`, any function `E` from `α` to another type, and any extended nonnegative real number `p`, given an instance of `NormedAddCommGroup` for `E i` for all `i` in `α`, the norm of the zero element in this normed additive commutative group is zero. The norm here could be thought of as the "length" or "size" of the element, and this theorem is asserting the common mathematical principle that the size of the zero element is zero.
More concisely: For any normed additive commutative group `(E : α →* X)` with `α` being any type, the norm of the zero element is zero.
|
lp.ext
theorem lp.ext :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f g : ↥(lp E p)},
↑f = ↑g → f = g
The theorem `lp.ext` states that for any type `α`, any function `E` from `α` to a type, any extended nonnegative real number `p`, any instance of a normed additive commutative group over the range of `E`, and any two elements `f` and `g` of the `lp` space of `E` with respect to `p`, if the underlying elements of `f` and `g` in the pre-Lp space are equal, then `f` and `g` themselves are equal in the `lp` space. In other words, this theorem asserts the extensionality of the `lp` function.
More concisely: If `α` is any type, `E` is any function from `α` to a normed additive commutative group, `p` is any extended nonnegative real number, and `f` and `g` are in the `lp` space of `E` with respect to `p` with equal underlying elements in the pre-`Lp` space, then `f` and `g` are equal in the `lp` space.
|
lp.normedAddCommGroup.proof_2
theorem lp.normedAddCommGroup.proof_2 :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] (f : ↥(lp E p)),
‖f‖ = 0 → f = 0
This theorem states that for any type `α`, a function `E` from `α` to some type, a nonnegative extended real number `p`, and given that each `E i` forms a normed add commutative group, and `p` is greater than or equal to 1, for any two elements `f` and `g` in the lp space defined by `E` and `p`, the norm of the sum of `f` and `g` is less than or equal to the sum of their norms. This property is generally known in mathematics as the triangle inequality in the context of normed spaces.
More concisely: For any normed add commutative group `(α, E)` and `p ≥ 1`, the triangle inequality holds: `‖f + g‖≤‖f‖ + ‖g‖` for all `f, g ∈ α`.
|
lp.tendsto_lp_of_tendsto_pi
theorem lp.tendsto_lp_of_tendsto_pi :
∀ {α : Type u_1} {E : α → Type u_2} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [_i : Fact (1 ≤ p)]
{F : ℕ → ↥(lp E p)},
CauchySeq F →
∀ {f : ↥(lp E p)},
Filter.Tendsto (id fun i => ↑(F i)) Filter.atTop (nhds ↑f) → Filter.Tendsto F Filter.atTop (nhds f)
This theorem states that if a sequence `F` is Cauchy in the `lp E p` topology, where `E` is a function from a type `α` to a type `u_2`, `p` is an extended nonnegative real number, and for each `i` in `α`, `E i` forms a normed additive commutative group, and `p` is greater than or equal to 1 (as ensured by `Fact (1 ≤ p)`). Furthermore, if this sequence pointwise converges to an element `f` of `lp E p` (as expressed by `Filter.Tendsto (id fun i => ↑(F i)) Filter.atTop (nhds ↑f)`), then the theorem asserts that the sequence `F` converges to `f` in the `lp E p` topology (denoted by `Filter.Tendsto F Filter.atTop (nhds f)`). Essentially, the theorem is establishing a connection between pointwise convergence and convergence in the `lp E p` topology for a Cauchy sequence.
More concisely: If a Cauchy sequence of functions from a type to a normed additive commutative group with respect to the `lp E p` topology, where `p` is a real number greater than or equal to 1, pointwise converges to an element in the space, then it converges to that element in the `lp E p` topology.
|