lineMap_slope_lineMap_slope_lineMap
theorem lineMap_slope_lineMap_slope_lineMap :
∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
[inst_3 : AddTorsor E PE] (f : k → PE) (a b r : k),
(AffineMap.lineMap (slope f ((AffineMap.lineMap a b) r) b) (slope f a ((AffineMap.lineMap a b) r))) r =
slope f a b
This theorem states that, for a function `f` mapping from a field `k` to a type `PE` with additive torsor structure over an additive commutative group `E`, and given any three elements `a`, `b`, and `r` of the field `k`, the slope of `f` between `a` and `b` can be expressed as a specific affine combination of the slopes of `f` at two other points. More specifically, the value of the slope of `f` from `a` to `b` is equal to the value of the affine map at `r` which is defined by the line map between the slope of `f` at the point `r` on the line map from `a` to `b` to `b`, and the slope of `f` from `a` to the point `r` on the line map from `a` to `b`.
More concisely: Given a function `f` from a field `k` to an additive torsor `PE` over a commutative additive group `E`, and elements `a, b, r` in `k`, the slope of `f` from `a` to `b` is equal to the affine combination of the slopes of `f` at `r` and at `a` along the line from `a` to `b`.
|
sub_div_sub_smul_slope_add_sub_div_sub_smul_slope
theorem sub_div_sub_smul_slope_add_sub_div_sub_smul_slope :
∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
[inst_3 : AddTorsor E PE] (f : k → PE) (a b c : k),
((b - a) / (c - a)) • slope f a b + ((c - b) / (c - a)) • slope f b c = slope f a c
The theorem `sub_div_sub_smul_slope_add_sub_div_sub_smul_slope` states that for any field `k`, additively commutative group `E`, and module `PE`, and for any function `f` mapping from `k` to `PE`, and any three elements `a`, `b`, and `c` in `k`, the slope of the function `f` at the interval `[a, c]` can be expressed as a linear combination of the slope of `f` at intervals `[a, b]` and `[b, c]`. The coefficients of this linear combination are respectively `(b - a) / (c - a)` and `(c - b) / (c - a)`. If `a` and `c` are not equal, then the sum of the coefficients is `1`, meaning this is an affine combination.
More concisely: Given a field `k`, an additively commutative group `E`, an `E`-module `PE`, and a function `f : k -> PE`, the slope of `f` at the interval `[a, c]` in `k` is equal to the linear combination of the slopes of `f` at intervals `[a, b]` and `[b, c]` with coefficients `(b - a) / (c - a)` and `(c - b) / (c - a)`, respectively.
|
lineMap_slope_slope_sub_div_sub
theorem lineMap_slope_slope_sub_div_sub :
∀ {k : Type u_1} {E : Type u_2} {PE : Type u_3} [inst : Field k] [inst_1 : AddCommGroup E] [inst_2 : Module k E]
[inst_3 : AddTorsor E PE] (f : k → PE) (a b c : k),
a ≠ c → (AffineMap.lineMap (slope f a b) (slope f b c)) ((c - b) / (c - a)) = slope f a c
This theorem states that for any field `k`, groups `E` and point `PE` with the field acting on them, and a function `f` mapping from `k` to `PE`, along with three distinct points `a`, `b`, `c` in `k` such that `a` is not equal to `c`, the slope of the function `f` at `a` and `c` can be expressed as an affine combination of the slope of the function `f` at `a` and `b` and the slope of the function `f` at `b` and `c`. This affine combination is computed using the `lineMap` function and the ratio `(c - b) / (c - a)`. In mathematical terms, this is expressing the secant line between `a` and `c` as a weighted average of the secant lines between `a` and `b` and between `b` and `c`, where the weights depend on the distances between the points.
More concisely: For any field `k`, group `E` with field action, point `PE`, and function `f` from `k` to `PE`, the slope of `f` at points `a`, `b`, and `c` in `k` (distinct from each other) satisfies the relation: (slope of `f` from `a` to `c`) = (slope of `f` from `a` to `b`) * (`c - b) / (`c - a`) + (slope of `f` from `b` to `c`) * (`c - a`) / (`b - a`).
|