map_lt_lineMap_iff_slope_lt_slope
theorem map_lt_lineMap_iff_slope_lt_slope :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
a < b →
0 < r →
r < 1 →
(f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔
slope f a ((AffineMap.lineMap a b) r) < slope f ((AffineMap.lineMap a b) r) b)
This theorem states that for a given function `f` mapping a linear ordered field `k` to an ordered additively commutative group `E`, and parameters `a`, `b`, and `r` in `k` such that `a < b`, `0 < r`, and `r < 1`, the point `(c, f c)`, where `c` is defined as `lineMap a b r`, is strictly below the line segment from `(a, f a)` to `(b, f b)` if and only if the slope of the function `f` at the interval from `a` to `c` is less than the slope of `f` at the interval from `c` to `b`. Here, the slope of the function `f` on an interval `[u, v]` is defined as `(v - u)⁻¹ • (f v -ᵥ f u)` and `lineMap a b r` is the affine map from `k` to `P1` sending `0` to `p₀` and `1` to `p₁`.
More concisely: Given a function `f` mapping a linear ordered field to an additively commutative group, and parameters `a < b`, `0 < r < 1` in the field, the point `(c, f c)` is strictly below the line segment from `(a, f a)` to `(b, f b)` if and only if the slope of `f` on the interval from `a` to `c` is less than the slope of `f` on the interval from `c` to `b`.
|
lineMap_le_map_iff_slope_le_slope_left
theorem lineMap_le_map_iff_slope_le_slope_left :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
0 < r * (b - a) →
((AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔
slope f a b ≤ slope f a ((AffineMap.lineMap a b) r))
The theorem `lineMap_le_map_iff_slope_le_slope_left` states that for a given linear ordered field `k`, ordered add commutative group `E`, a module structure of `E` over `k` and an ordered scalar multiplication of `k` over `E`, if we have a function `f` from `k` to `E`, and three elements `a`, `b`, and `r` of `k` such that `0 < r * (b - a)`, then the point `(c, f c)` (where `c = lineMap a b r`) lies on or above the line segment joining `(a, f a)` and `(b, f b)` if and only if the slope of the function `f` on the interval `[a, b]` is less than or equal to the slope of the function `f` on the interval `[a, c]`. Here, the slope of the function `f` on an interval `[x, y]` is defined as `(y - x)⁻¹ • (f y -ᵥ f x)`, and the term `lineMap p q x` refers to a specific point on the line between `p` and `q` determined by `x`.
More concisely: For a linear ordered field `k`, an ordered add commutative group `E` with a module and scalar multiplication over `k`, and a function `f` from `k` to `E`, if `0 < r * (b - a)` and `(c, f c)` is the point on the line between `(a, f a)` and `(b, f b)` determined by `c = lineMap a b r`, then `f` has slope less than or equal to `(b - a)⁻¹ • (f b - f a)` on the interval `[a, b]` if and only if `(c, f c)` lies on or above the line segment joining `(a, f a)` and `(b, f b)`.
|
map_lt_lineMap_iff_slope_lt_slope_right
theorem map_lt_lineMap_iff_slope_lt_slope_right :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
0 < (1 - r) * (b - a) →
(f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔
slope f a b < slope f ((AffineMap.lineMap a b) r) b)
The theorem `map_lt_lineMap_iff_slope_lt_slope_right` states that for a given linear ordered field `k`, an ordered additive commutative group `E`, a module `k` over `E`, and an ordered scalar multiplication of `k` over `E`, along with a function `f : k -> E` and three elements `a`, `b`, `r` of `k` such that `0 < (1 - r) * (b - a)`, the y-value `f(c)` of a point `(c, f(c))` is strictly less than the y-value on the line segment between `(a, f(a))` and `(b, f(b))` at `c` if and only if the slope of the function `f` between `a` and `b` is less than the slope of the function `f` between point `c` and `b`. Here `c` is a point on the line segment between `a` and `b` defined by `c = lineMap a b r`, and `c` is strictly less than `b`.
More concisely: Given a linear ordered field `k`, an ordered additive commutative group `E`, a module `k` over `E`, an ordered scalar multiplication of `k` over `E`, a function `f : k -> E`, and elements `a, b, r, c (c < b) in k` with `0 < (1 - r) * (b - a)`, the point `(c, f(c))` lies below the line segment between `(a, f(a))` and `(b, f(b))` if and only if the slope of `f` between `a` and `b` is less than the slope of `f` from `a` to `c`.
|
map_le_lineMap_iff_slope_le_slope
theorem map_le_lineMap_iff_slope_le_slope :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
a < b →
0 < r →
r < 1 →
(f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔
slope f a ((AffineMap.lineMap a b) r) ≤ slope f ((AffineMap.lineMap a b) r) b)
The theorem `map_le_lineMap_iff_slope_le_slope` states that for a given linear ordered field `k`, an ordered additive commutative group `E`, a module `E` over `k`, an ordered scalar multiplication of `k` and `E`, and a function `f` from `k` to `E`, let's consider `a` and `b` in `k` such that `a < b`, and a real number `r` between 0 and 1. If `c` is the point on the line between `a` and `b` corresponding to `r` (i.e., `c = lineMap a b r`), then the point `(c, f(c))` is non-strictly below the line segment joining the points `(a, f(a))` and `(b, f(b))` if and only if the slope of the function `f` on the interval `[a, c]` is less than or equal to the slope of `f` on the interval `[c, b]`. This essentially states that if `(c, f(c))` is below or on the line segment, then the function `f` is not increasing faster on `[c, b]` than it is on `[a, c]`.
More concisely: Given a linear ordered field `k`, an ordered additive commutative group `E`, a module `E` over `k`, an ordered scalar multiplication of `k` and `E`, a function `f` from `k` to `E`, and `a`, `b` in `k` with `a < b` and `r` a real number between 0 and 1, the point `(c, f(c))` is below the line segment joining `(a, f(a))` and `(b, f(b))` if and only if the slope of `f` on the interval `[a, c]` is less than or equal to the slope of `f` on the interval `[c, b]`.
|
lineMap_lt_map_iff_slope_lt_slope_left
theorem lineMap_lt_map_iff_slope_lt_slope_left :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
0 < r * (b - a) →
((AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔
slope f a b < slope f a ((AffineMap.lineMap a b) r))
This theorem states that for a given linear-ordered field `k`, an ordered additive commutative group `E`, and `f` as a function from `k` to `E`, if `c` equals `lineMap a b r` with `a` less than `c`, then the point `(c, f c)` is strictly above the line segment from `(a, f a)` to `(b, f b)` if and only if the slope of `f` on the interval `[a, b]` is less than the slope of `f` on the interval `[a, c]`. Here, `0 < r * (b - a)` guarantees that `r` is in `(0,1)` when `a < b`, meaning `c = lineMap a b r` is strictly between `a` and `b`. In geometric terms, it means the curve represented by `f` is strictly above the straight line segment from `(a, f a)` to `(b, f b)` at the point `c` if and only if the slope of the curve at `c` is greater than the slope of the line segment.
More concisely: For a given linear-ordered field `k`, an ordered additive commutative group `E`, and function `f` from `k` to `E`, the point `(c, f c)` lies strictly above the line segment from `(a, f a)` to `(b, f b)` if and only if the slope of `f` on the interval `[a, b]` is less than the slope of `f` on the interval `[a, c]`.
|
lineMap_lt_map_iff_slope_lt_slope
theorem lineMap_lt_map_iff_slope_lt_slope :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
a < b →
0 < r →
r < 1 →
((AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔
slope f ((AffineMap.lineMap a b) r) b < slope f a ((AffineMap.lineMap a b) r))
This theorem states that for any linear ordered field `k`, an ordered additive commutative group `E`, a module `E` over `k`, a function `f` from `k` to `E`, and three elements `a`, `b`, and `r` of `k` such that `a < b` and `0 < r < 1`, the point `(c, f(c))` is strictly above the line segment between `(a, f(a))` and `(b, f(b))` (where `c` is the image of `r` under the affine map from `a` to `b`) if and only if the slope of `f` at `c` to `b` is less than the slope of `f` at `a` to `c`. Here, the slope of the function `f` on the interval `[a, b]` is defined as `(f(b) - f(a)) / (b - a)`, and the affine map from `k` to `E` sends `0` to `f(a)` and `1` to `f(b)`.
More concisely: For any linear ordered field `k`, an ordered additive commutative group `E`, a module `E` over `k`, a function `f` from `k` to `E`, and elements `a < b` and `0 < r < 1` in `k`, the point `(f(c), f(c))` is strictly above the line segment between `(f(a), f(a))` and `(f(b), f(b))` if and only if the slope of `f` on the interval `[a, b]` is less than the slope of `f` from `a` to `c`, where `c = a + r(b - a)`.
|
map_le_lineMap_iff_slope_le_slope_left
theorem map_le_lineMap_iff_slope_le_slope_left :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
0 < r * (b - a) →
(f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔
slope f a ((AffineMap.lineMap a b) r) ≤ slope f a b)
The theorem `map_le_lineMap_iff_slope_le_slope_left` states that for a given linear ordered field `k`, an ordered add commutative group `E` which is a module over `k`, a function `f` from `k` to `E`, and elements `a`, `b`, and `r` in `k` such that `0 < r * (b - a)`, the function value at `c` (where `c` is the affine map from `a` to `b` with ratio `r`), `f(c)`, is less than or equal to the affine map from `f(a)` to `f(b)` with ratio `r` if and only if the slope of the function `f` at `a` and `c` is less than or equal to the slope of the function `f` at `a` and `b`. In other words, the point `(c, f(c))` lies on or below the line segment connecting `(a, f(a))` and `(b, f(b))` if and only if the rate of change of the function `f` from `a` to `c` is less than or equal to the rate of change from `a` to `b`.
More concisely: Given a linear ordered field `k`, an add commutative group `E` that is a `k`-module, a function `f` from `k` to `E`, and `a`, `b`, and `r` in `k` with `0 < r * (b - a)`, the point `(c, f(c))` lies on or below the line connecting `(a, f(a))` and `(b, f(b))` if and only if the slope of `f` at `a` and `c` is less than or equal to the slope of `f` at `a` and `b`.
|
map_le_lineMap_iff_slope_le_slope_right
theorem map_le_lineMap_iff_slope_le_slope_right :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
0 < (1 - r) * (b - a) →
(f ((AffineMap.lineMap a b) r) ≤ (AffineMap.lineMap (f a) (f b)) r ↔
slope f a b ≤ slope f ((AffineMap.lineMap a b) r) b)
The theorem states that for a given function `f` mapping from a type `k` to a type `E`, and given points `a`, `b`, and `r` of type `k` such that `c = lineMap a b r` and `c < b`, the point `(c, f c)` is non-strictly below the line segment joining `(a, f a)` and `(b, f b)` if and only if the slope of the function `f` on the interval `[a, b]` is less than or equal to the slope of the function `f` on the interval `[c, b]`. Here `lineMap` is an affine map from `k` to `P1` sending `0` to `p₀` and `1` to `p₁`, and `slope` is defined as `(b - a)⁻¹ • (f b -ᵥ f a)`. The condition `0 < (1 - r) * (b - a)` ensures that `b` is strictly greater than `c`.
More concisely: For a function `f` from type `k` to a vector space `E`, points `a`, `b` of type `k`, and `r` satisfying `0 < (1 - r) * (b - a)`, the point `(c, f c)` lies strictly below the line segment joining `(a, f a)` and `(b, f b)` if and only if the slope of `f` on `[a, b]` is less than or equal to that on `[c, b]`, where `c = lineMap a b r` and `lineMap` is the affine map from `k` to `P1`.
|
map_lt_lineMap_iff_slope_lt_slope_left
theorem map_lt_lineMap_iff_slope_lt_slope_left :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
0 < r * (b - a) →
(f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔
slope f a ((AffineMap.lineMap a b) r) < slope f a b)
The theorem `map_lt_lineMap_iff_slope_lt_slope_left` states that for any linear ordered field `k`, ordered additive commutative group `E`, `k`-module `E`, `k`-scalable ordered multiplicative `E`, a function `f` from `k` to `E`, and `a`, `b`, `r` in `k` such that `0 < r * (b - a)`, point `c` is determined on the line segment from `a` to `b` by `c = lineMap a b r` and `a < c`. Then, the point `(c, f(c))` lies strictly below the line segment joining `(a, f(a))` and `(b, f(b))` if and only if the slope of `f` on the interval `[a, c]` is less than the slope of `f` on the interval `[a, b]`. Here, the slope of `f` on an interval `[x, y]` is defined as `(y - x)⁻¹ • (f y -ᵥ f x)`.
More concisely: For a linear ordered field `k`, an ordered additive commutative group `E`, `k`-module and `k`-scalable ordered multiplicative `E`, function `f` from `k` to `E`, and `a`, `b`, `r` in `k` with `0 < r * (b - a)`, the point `(c, f(c))` lies strictly below the line passing through `(a, f(a))` and `(b, f(b))` if and only if the slope of `f` on the interval `[a, c]` is less than the slope of `f` on the interval `[a, b]`.
|
lineMap_le_map_iff_slope_le_slope
theorem lineMap_le_map_iff_slope_le_slope :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
a < b →
0 < r →
r < 1 →
((AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔
slope f ((AffineMap.lineMap a b) r) b ≤ slope f a ((AffineMap.lineMap a b) r))
The theorem `lineMap_le_map_iff_slope_le_slope` states that for all types `k` and `E`, where `k` is a linear-ordered field and `E` is a ordered add commutative group and also a module over `k`, for any function `f` mapping from `k` to `E` and for any values `a`, `b`, and `r` of type `k` such that `a < b`, `0 < r`, and `r < 1`, the point `(c, f c)` (where `c` is the affine map from `k` to `P1` sending `0` to `a` and `1` to `b` evaluated at `r`) is non-strictly above the line segment between `(a, f a)` and `(b, f b)` if and only if the slope of `f` on the interval `[c, b]` is less than or equal to the slope of `f` on the interval `[a, c]`. Here, the slope of a function `f` on the interval `[a, b]` is defined as `(b - a)⁻¹ • (f b -ᵥ f a)`.
More concisely: Given a function `f` from a linear-ordered field `k` to an ordered add commutative group and module `E`, and values `a`, `b` in `k` with `a < b`, `0 < r < 1`, the point `(c, f c)` lies below the line through `(a, f a)` and `(b, f b)` if and only if the slope of `f` on the interval `[a, b]` is less than or equal to the slope of `f` on the interval `[c, b]`, where `c` is the affine map sending `0` to `a` and `1` to `b` evaluated at `r`.
|
lineMap_le_map_iff_slope_le_slope_right
theorem lineMap_le_map_iff_slope_le_slope_right :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
0 < (1 - r) * (b - a) →
((AffineMap.lineMap (f a) (f b)) r ≤ f ((AffineMap.lineMap a b) r) ↔
slope f ((AffineMap.lineMap a b) r) b ≤ slope f a b)
This theorem says that for a given function `f` mapping from a type `k` to a type `E`, and given three points `a`, `b`, and `r` in `k` with certain conditions (`b` > `a`, `r` is a scalar on the line segment from `a` to `b`), the point `(c, f(c))` lies on or above the line segment joining `(a, f(a))` and `(b, f(b))` if and only if the slope of the function `f` at `c` towards `b` is less than or equal to the slope of `f` from `a` to `b`. Here, `c` is the image under `lineMap a b` of `r`, and 'slope' is defined as `slope f a b = (b - a)⁻¹ • (f b -ᵥ f a)`.
More concisely: Given a function `f` from type `k` to a type `E`, points `a`, `b` in `k` with `b > a`, and scalar `r`, the point `(c, f(c))` lies on or above the line segment joining `(a, f(a))` and `(b, f(b))` if and only if the slope of `f` from `c` to `b` is less than or equal to the slope of `f` from `a` to `b`, where `c` is the image under `lineMap a b` of `r`.
|
lineMap_lt_map_iff_slope_lt_slope_right
theorem lineMap_lt_map_iff_slope_lt_slope_right :
∀ {k : Type u_1} {E : Type u_2} [inst : LinearOrderedField k] [inst_1 : OrderedAddCommGroup E] [inst_2 : Module k E]
[inst_3 : OrderedSMul k E] {f : k → E} {a b r : k},
0 < (1 - r) * (b - a) →
((AffineMap.lineMap (f a) (f b)) r < f ((AffineMap.lineMap a b) r) ↔
slope f ((AffineMap.lineMap a b) r) b < slope f a b)
The theorem `lineMap_lt_map_iff_slope_lt_slope_right` states that for a given function `f` mapping from a linearly ordered field `k` to an ordered additive commutative group `E`, and given points `a`, `b`, and `r` on `k`, where `c = lineMap a b r` is a point on the line between `a` and `b` and `c < b`. It then asserts that the point `(c, f c)` is strictly above the line segment joining `(a, f a)` and `(b, f b)` if and only if the slope of the function `f` between `c` and `b` is less than the slope of the function `f` between `a` and `b`. This is subject to the condition that `0 < (1 - r) * (b - a)`. The slopes are calculated as `(b - a)⁻¹ • (f b -ᵥ f a)`, where `-ᵥ` denotes the difference in the `E` space.
More concisely: For a function `f` mapping from a linearly ordered field to an ordered additive commutative group, and given points `a`, `b`, and `r` such that `0 < (1 - r) * (b - a)`, the point `(c, f c)` is strictly above the line segment joining `(a, f a)` and `(b, f b)` if and only if the slope of `f` between `c` and `b` is less than the slope of `f` between `a` and `b`.
|