Convex Analysis (Rockafellar, 1970) -- Chapter 05 -- Section 24 -- Part 10
section Chap05section Section24open scoped ConvexAnalysisattribute [local instance] Classical.propDecidable
Helper for Theorem 5.24.4: once the scalar interval-integral primitive is genuinely
constructed, it should first produce a normalized closed proper convex function whose scalar
derivative band contains φ.
lemma helperForTheorem_5_24_4_intervalIntegralPrimitive_closed_normalized_scalarBand
(φ : ℝ → EReal) (a : ℝ) (hmono : Monotone φ)
(ha_finite : φ a ≠ (⊤ : EReal) ∧ φ a ≠ (⊥ : EReal)) :
let f : (Fin 1 → ℝ) → EReal := oneDimensionalIntervalIntegralPrimitive φ a
ClosedConvexFunction f ∧
f (scalarPoint a) = 0 ∧
(∀ x : ℝ, leftDerivativeExtension f x ≤ φ x ∧ φ x ≤ rightDerivativeExtension f x) := by
let f : (Fin 1 → ℝ) → EReal := oneDimensionalIntervalIntegralPrimitive φ a
have hconv : ConvexFunction f := by
simpa [f] using
helperForTheorem_5_24_4_intervalIntegralPrimitive_convex φ a hmono ha_finite
have hproper : ProperConvexFunctionOn (Set.univ : Set (Fin 1 → ℝ)) f :=
helperForTheorem_5_24_4_intervalIntegralPrimitive_proper_of_convex φ a hconv
have hBandReduction :
(∀ x ∈ scalarEffectiveDomain f,
leftDerivativeExtension f x ≤ φ x ∧ φ x ≤ rightDerivativeExtension f x) →
∀ x : ℝ, leftDerivativeExtension f x ≤ φ x ∧ φ x ≤ rightDerivativeExtension f x := by
simpa [f] using helperForTheorem_5_24_4_scalarBand_of_domain_band φ a hmono ha_finite
have hBandOnDom :
∀ x ∈ scalarEffectiveDomain f,
leftDerivativeExtension f x ≤ φ x ∧ φ x ≤ rightDerivativeExtension f x := by
intro x hxDom
simpa [f] using
helperForTheorem_5_24_4_scalarBand_on_scalarEffectiveDomain φ a x hmono ha_finite hxDom
have hBand :
∀ x : ℝ, leftDerivativeExtension f x ≤ φ x ∧ φ x ≤ rightDerivativeExtension f x :=
hBandReduction hBandOnDom
have hAtBase : f (scalarPoint a) = 0 := by
simpa [f] using helperForTheorem_5_24_4_primitive_at_scalarBasePoint φ a
refine ⟨?_, hAtBase, hBand⟩
have hScalarLsc : LowerSemicontinuous (oneDimensionalIntervalIntegralPrimitiveValue φ a) := by
intro x
by_cases hxDom : x ∈ scalarEffectiveDomain f
· simpa [f] using
helperForTheorem_5_24_4_primitiveValue_lowerSemicontinuousAt_of_mem_scalarEffectiveDomain
φ a x hmono ha_finite hxDom
· rcases
helperForTheorem_5_24_4_off_scalarEffectiveDomain_is_exterior
φ a x hmono ha_finite hxDom with
hxRight | hxLeft
· simpa [f] using
helperForTheorem_5_24_4_primitiveValue_lowerSemicontinuousAt_of_rightOfScalarEffectiveDomain
φ a x hmono ha_finite hxRight
· simpa [f] using
helperForTheorem_5_24_4_primitiveValue_lowerSemicontinuousAt_of_leftOfScalarEffectiveDomain
φ a x hmono ha_finite hxLeft
have hLsc : LowerSemicontinuous f := by
simpa [f, oneDimensionalIntervalIntegralPrimitive] using
(hScalarLsc.comp (continuous_apply 0))
exact (properConvexFunction_closed_iff_lowerSemicontinuous hproper).2 hLsc-- Route correction: to formalize the textbook linear example in a stable way, we first record
-- the quarter-turn counterexample as reusable helpers.
Helper for Remark 5.24.5: the quarter-turn on R^2 used for the linear counterexample.
def helperForRemark_5_24_5_quarterTurn : (Fin 2 → ℝ) → (Fin 2 → ℝ) :=
fun x => ![-x 1, x 0]Helper for Remark 5.24.5: the singleton-valued mapping generated by the quarter-turn.
def helperForRemark_5_24_5_quarterTurnMapping : (Fin 2 → ℝ) → Set (Fin 2 → ℝ) :=
fun x => {helperForRemark_5_24_5_quarterTurn x}Helper for Remark 5.24.5: the planar quarter-turn is additive. This records the linear structure behind the textbook counterexample.
lemma helperForRemark_5_24_5_quarterTurn_add
(x y : Fin 2 → ℝ) :
helperForRemark_5_24_5_quarterTurn (x + y) =
helperForRemark_5_24_5_quarterTurn x + helperForRemark_5_24_5_quarterTurn y := by
-- Expanding both coordinates shows that the quarter-turn distributes over vector addition.
ext i
fin_cases i
· simp [helperForRemark_5_24_5_quarterTurn]
ring
· simp [helperForRemark_5_24_5_quarterTurn]Helper for Remark 5.24.5: the planar quarter-turn commutes with scalar multiplication.
lemma helperForRemark_5_24_5_quarterTurn_smul
(c : ℝ) (x : Fin 2 → ℝ) :
helperForRemark_5_24_5_quarterTurn (c • x) =
c • helperForRemark_5_24_5_quarterTurn x := by
-- Coordinatewise expansion reduces the claim to elementary real algebra.
ext i
fin_cases i
· simp [helperForRemark_5_24_5_quarterTurn, smul_eq_mul]
· simp [helperForRemark_5_24_5_quarterTurn, smul_eq_mul]
Helper for Remark 5.24.5: the quarter-turn packaged as a linear map on R^2.
def helperForRemark_5_24_5_quarterTurnLinearMap : (Fin 2 → ℝ) →ₗ[ℝ] (Fin 2 → ℝ) :=
{ toFun := helperForRemark_5_24_5_quarterTurn
map_add' := helperForRemark_5_24_5_quarterTurn_add
map_smul' := helperForRemark_5_24_5_quarterTurn_smul }Helper for Remark 5.24.5: the quarter-turn is skew with respect to the Euclidean dot product, so every vector is orthogonal to its image.
lemma helperForRemark_5_24_5_dotProduct_self_quarterTurn
(x : Fin 2 → ℝ) :
dotProduct x (helperForRemark_5_24_5_quarterTurn x) = 0 := by
-- Expanding the two coordinates leaves the alternating bilinear form `-x0*x1 + x1*x0`.
simp [helperForRemark_5_24_5_quarterTurn, dotProduct]
ringHelper for Remark 5.24.5: the singleton-valued quarter-turn mapping is monotone, because the dot product of any increment with its rotated increment vanishes.
lemma helperForRemark_5_24_5_quarterTurnMapping_monotone :
IsMonotoneMultivaluedMapping helperForRemark_5_24_5_quarterTurnMapping := by
intro x0 x1 x0Star x1Star hx0Star hx1Star
have hx0StarEq : x0Star = helperForRemark_5_24_5_quarterTurn x0 := by
-- Singleton fibers identify the chosen graph point with the quarter-turn image.
simpa [helperForRemark_5_24_5_quarterTurnMapping] using hx0Star
have hx1StarEq : x1Star = helperForRemark_5_24_5_quarterTurn x1 := by
-- The second graph point is identified in the same way.
simpa [helperForRemark_5_24_5_quarterTurnMapping] using hx1Star
have hdiff :
x1Star - x0Star = helperForRemark_5_24_5_quarterTurn (x1 - x0) := by
-- Coordinatewise subtraction commutes with the linear quarter-turn.
ext i
fin_cases i
· simp [helperForRemark_5_24_5_quarterTurn, hx0StarEq, hx1StarEq]
ring
· simp [helperForRemark_5_24_5_quarterTurn, hx0StarEq, hx1StarEq]
rw [hdiff]
-- The monotonicity form is exactly the self-pairing from the previous orthogonality lemma.
have hzero :
dotProduct (x1 - x0) (helperForRemark_5_24_5_quarterTurn (x1 - x0)) = 0 :=
helperForRemark_5_24_5_dotProduct_self_quarterTurn (x1 - x0)
linarith
Helper for Remark 5.24.5: the quarter-turn mapping fails cyclic monotonicity on the triangle
with vertices (1,0), (0,1), and (0,0).
lemma helperForRemark_5_24_5_quarterTurnMapping_not_cyclicallyMonotone :
¬ IsCyclicallyMonotone helperForRemark_5_24_5_quarterTurnMapping := by
intro hcyclic
let x : Fin 3 → Fin 2 → ℝ := ![![1, 0], ![0, 1], 0]
let xStar : Fin 3 → Fin 2 → ℝ := fun i => helperForRemark_5_24_5_quarterTurn (x i)
have hmem :
∀ i : Fin 3, xStar i ∈ helperForRemark_5_24_5_quarterTurnMapping (x i) := by
intro i
-- Each chosen covector is exactly the value prescribed by the singleton fiber.
simp [xStar, helperForRemark_5_24_5_quarterTurnMapping]
have hineq := hcyclic 2 x xStar hmem
have hineq' : (1 : ℝ) ≤ 0 := by
-- On this explicit 3-cycle, the cyclic sum evaluates to `1`, contradicting nonpositivity.
simpa [Fin.sum_univ_three, x, xStar, helperForRemark_5_24_5_quarterTurn,
helperForRemark_5_24_5_quarterTurnMapping, cyclicSuccessor, dotProduct] using hineq
linarithHelper for Remark 5.24.5: dimension two already supplies a monotone mapping that is not cyclically monotone, namely the singleton-valued quarter-turn.
lemma helperForRemark_5_24_5_exists_monotone_not_cyclicallyMonotone_in_dimension_two :
∃ ρ : (Fin 2 → ℝ) → Set (Fin 2 → ℝ),
IsMonotoneMultivaluedMapping ρ ∧ ¬ IsCyclicallyMonotone ρ := by
-- Package the explicit quarter-turn construction as the witness promised by the remark.
refine ⟨helperForRemark_5_24_5_quarterTurnMapping, ?_, ?_⟩
· exact helperForRemark_5_24_5_quarterTurnMapping_monotone
· exact helperForRemark_5_24_5_quarterTurnMapping_not_cyclicallyMonotone-- Route correction: we next extend the quarter-turn witness to every ambient space `R^(2+m)` so
-- the final remark can be discharged uniformly for all `n > 1`.
Helper for Remark 5.24.5: project a vector in R^(2+m) onto its first two coordinates.
def helperForRemark_5_24_5_frontCoordinates (m : ℕ) :
(Fin (2 + m) → ℝ) → (Fin 2 → ℝ) :=
fun x i => x (Fin.castAdd m i)
Helper for Remark 5.24.5: embed a vector in R^2 into R^(2+m) by zero-extension.
def helperForRemark_5_24_5_extendByZero (m : ℕ) :
(Fin 2 → ℝ) → (Fin (2 + m) → ℝ) :=
fun x => Fin.append x 0Helper for Remark 5.24.5: projecting after zero-extension recovers the original planar vector.
lemma helperForRemark_5_24_5_frontCoordinates_extendByZero
(m : ℕ) (x : Fin 2 → ℝ) :
helperForRemark_5_24_5_frontCoordinates m
(helperForRemark_5_24_5_extendByZero m x) = x := by
-- The first two coordinates of the appended vector are exactly the original entries.
ext i
simp [helperForRemark_5_24_5_frontCoordinates, helperForRemark_5_24_5_extendByZero]Helper for Remark 5.24.5: zero-extension commutes with subtraction.
lemma helperForRemark_5_24_5_extendByZero_sub
(m : ℕ) (x y : Fin 2 → ℝ) :
helperForRemark_5_24_5_extendByZero m (x - y) =
helperForRemark_5_24_5_extendByZero m x - helperForRemark_5_24_5_extendByZero m y := by
-- Check the first two coordinates directly; the appended tail is identically zero.
ext i
refine Fin.addCases ?_ ?_ i
· intro j
simp [helperForRemark_5_24_5_extendByZero]
· intro j
simp [helperForRemark_5_24_5_extendByZero]Helper for Remark 5.24.5: zero-extension preserves the Euclidean dot product.
lemma helperForRemark_5_24_5_dotProduct_extendByZero
(m : ℕ) (u v : Fin 2 → ℝ) :
dotProduct (helperForRemark_5_24_5_extendByZero m u)
(helperForRemark_5_24_5_extendByZero m v) =
dotProduct u v := by
-- Split the ambient sum into its planar part and the zero tail.
rw [dotProduct, Fin.sum_univ_add]
simp [helperForRemark_5_24_5_extendByZero, dotProduct]Helper for Remark 5.24.5: rotate the first two coordinates and kill the remaining ones.
def helperForRemark_5_24_5_stabilizedQuarterTurn (m : ℕ) :
(Fin (2 + m) → ℝ) → (Fin (2 + m) → ℝ) :=
fun x =>
helperForRemark_5_24_5_extendByZero m
(helperForRemark_5_24_5_quarterTurn
(helperForRemark_5_24_5_frontCoordinates m x))
Helper for Remark 5.24.5: the singleton-valued mapping generated by the stabilized
quarter-turn on R^(2+m).
def helperForRemark_5_24_5_stabilizedQuarterTurnMapping (m : ℕ) :
(Fin (2 + m) → ℝ) → Set (Fin (2 + m) → ℝ) :=
fun x => {helperForRemark_5_24_5_stabilizedQuarterTurn m x}Helper for Remark 5.24.5: the stabilized quarter-turn agrees with zero-extension of the planar quarter-turn on vectors supported in the first two coordinates.
lemma helperForRemark_5_24_5_stabilizedQuarterTurn_extendByZero
(m : ℕ) (x : Fin 2 → ℝ) :
helperForRemark_5_24_5_stabilizedQuarterTurn m
(helperForRemark_5_24_5_extendByZero m x) =
helperForRemark_5_24_5_extendByZero m
(helperForRemark_5_24_5_quarterTurn x) := by
-- The front projection removes the zero tail, so only the original planar vector remains.
rw [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_frontCoordinates_extendByZero]Helper for Remark 5.24.5: the stabilized quarter-turn remains additive with respect to subtraction.
lemma helperForRemark_5_24_5_stabilizedQuarterTurn_sub
(m : ℕ) (x y : Fin (2 + m) → ℝ) :
helperForRemark_5_24_5_stabilizedQuarterTurn m (x - y) =
helperForRemark_5_24_5_stabilizedQuarterTurn m x -
helperForRemark_5_24_5_stabilizedQuarterTurn m y := by
-- Split coordinates into the first two and the zero tail, then compute coordinatewise.
ext i
refine Fin.addCases ?_ ?_ i
· intro j
fin_cases j
· simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero, helperForRemark_5_24_5_frontCoordinates,
helperForRemark_5_24_5_quarterTurn]
ring
· simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero, helperForRemark_5_24_5_frontCoordinates,
helperForRemark_5_24_5_quarterTurn]
· intro j
simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero]Helper for Remark 5.24.5: the stabilized quarter-turn is additive in every ambient dimension.
lemma helperForRemark_5_24_5_stabilizedQuarterTurn_add
(m : ℕ) (x y : Fin (2 + m) → ℝ) :
helperForRemark_5_24_5_stabilizedQuarterTurn m (x + y) =
helperForRemark_5_24_5_stabilizedQuarterTurn m x +
helperForRemark_5_24_5_stabilizedQuarterTurn m y := by
-- The first two coordinates behave like the planar quarter-turn, and the tail stays zero.
ext i
refine Fin.addCases ?_ ?_ i
· intro j
fin_cases j
· simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero, helperForRemark_5_24_5_frontCoordinates,
helperForRemark_5_24_5_quarterTurn]
ring
· simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero, helperForRemark_5_24_5_frontCoordinates,
helperForRemark_5_24_5_quarterTurn]
· intro j
simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero]Helper for Remark 5.24.5: the stabilized quarter-turn commutes with scalar multiplication.
lemma helperForRemark_5_24_5_stabilizedQuarterTurn_smul
(m : ℕ) (c : ℝ) (x : Fin (2 + m) → ℝ) :
helperForRemark_5_24_5_stabilizedQuarterTurn m (c • x) =
c • helperForRemark_5_24_5_stabilizedQuarterTurn m x := by
-- Again only the planar block is active; the appended coordinates remain zero.
ext i
refine Fin.addCases ?_ ?_ i
· intro j
fin_cases j
· simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero, helperForRemark_5_24_5_frontCoordinates,
helperForRemark_5_24_5_quarterTurn, smul_eq_mul]
· simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero, helperForRemark_5_24_5_frontCoordinates,
helperForRemark_5_24_5_quarterTurn, smul_eq_mul]
· intro j
simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero, smul_eq_mul]
Helper for Remark 5.24.5: the stabilized quarter-turn packaged as a linear map on R^(2+m).
def helperForRemark_5_24_5_stabilizedQuarterTurnLinearMap (m : ℕ) :
(Fin (2 + m) → ℝ) →ₗ[ℝ] (Fin (2 + m) → ℝ) :=
{ toFun := helperForRemark_5_24_5_stabilizedQuarterTurn m
map_add' := helperForRemark_5_24_5_stabilizedQuarterTurn_add m
map_smul' := helperForRemark_5_24_5_stabilizedQuarterTurn_smul m }
Helper for Remark 5.24.5: every vector is orthogonal to its stabilized quarter-turn image in
R^(2+m).
lemma helperForRemark_5_24_5_dotProduct_self_stabilizedQuarterTurn
(m : ℕ) (x : Fin (2 + m) → ℝ) :
dotProduct x (helperForRemark_5_24_5_stabilizedQuarterTurn m x) = 0 := by
-- Decompose the ambient dot product into the first two coordinates and the vanishing tail.
rw [dotProduct, Fin.sum_univ_add]
have hfront :
(∑ i : Fin 2,
x (Fin.castAdd m i) *
helperForRemark_5_24_5_stabilizedQuarterTurn m x (Fin.castAdd m i)) =
dotProduct (helperForRemark_5_24_5_frontCoordinates m x)
(helperForRemark_5_24_5_quarterTurn
(helperForRemark_5_24_5_frontCoordinates m x)) := by
-- On the planar block this is exactly the original quarter-turn pairing.
simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero, helperForRemark_5_24_5_frontCoordinates, dotProduct]
have htail :
(∑ i : Fin m,
x (Fin.natAdd 2 i) *
helperForRemark_5_24_5_stabilizedQuarterTurn m x (Fin.natAdd 2 i)) = 0 := by
-- All tail coordinates of the stabilized quarter-turn vanish by construction.
simp [helperForRemark_5_24_5_stabilizedQuarterTurn,
helperForRemark_5_24_5_extendByZero]
rw [hfront, htail, add_zero]
exact
helperForRemark_5_24_5_dotProduct_self_quarterTurn
(helperForRemark_5_24_5_frontCoordinates m x)
Helper for Remark 5.24.5: the stabilized singleton-valued quarter-turn remains monotone in
every dimension 2 + m.
lemma helperForRemark_5_24_5_stabilizedQuarterTurnMapping_monotone
(m : ℕ) :
IsMonotoneMultivaluedMapping (helperForRemark_5_24_5_stabilizedQuarterTurnMapping m) := by
intro x0 x1 x0Star x1Star hx0Star hx1Star
have hx0StarEq : x0Star = helperForRemark_5_24_5_stabilizedQuarterTurn m x0 := by
-- Singleton fibers identify the first graph point with the stabilized rotation.
simpa [helperForRemark_5_24_5_stabilizedQuarterTurnMapping] using hx0Star
have hx1StarEq : x1Star = helperForRemark_5_24_5_stabilizedQuarterTurn m x1 := by
-- The second graph point is identified in the same way.
simpa [helperForRemark_5_24_5_stabilizedQuarterTurnMapping] using hx1Star
have hdiff :
x1Star - x0Star =
helperForRemark_5_24_5_stabilizedQuarterTurn m (x1 - x0) := by
-- The stabilized quarter-turn is linear on the active coordinates and zero on the tail.
rw [hx0StarEq, hx1StarEq, helperForRemark_5_24_5_stabilizedQuarterTurn_sub]
rw [hdiff]
-- Monotonicity again reduces to orthogonality of an increment with its rotated image.
have hzero :
dotProduct (x1 - x0)
(helperForRemark_5_24_5_stabilizedQuarterTurn m (x1 - x0)) = 0 :=
helperForRemark_5_24_5_dotProduct_self_stabilizedQuarterTurn m (x1 - x0)
linarith
Helper for Remark 5.24.5: if the stabilized quarter-turn were cyclically monotone in
R^(2+m), then its restriction to the first two coordinates would make the planar quarter-turn
cyclically monotone as well.
lemma helperForRemark_5_24_5_quarterTurnMapping_cyclicallyMonotone_of_stabilized
(m : ℕ)
(hcyclic :
IsCyclicallyMonotone (helperForRemark_5_24_5_stabilizedQuarterTurnMapping m)) :
IsCyclicallyMonotone helperForRemark_5_24_5_quarterTurnMapping := by
intro k x xStar hmem
let X : Fin (k + 1) → Fin (2 + m) → ℝ :=
fun i => helperForRemark_5_24_5_extendByZero m (x i)
let XStar : Fin (k + 1) → Fin (2 + m) → ℝ :=
fun i => helperForRemark_5_24_5_extendByZero m (xStar i)
have hmem' :
∀ i : Fin (k + 1),
XStar i ∈ helperForRemark_5_24_5_stabilizedQuarterTurnMapping m (X i) := by
intro i
have hxStarEq : xStar i = helperForRemark_5_24_5_quarterTurn (x i) := by
-- Planar singleton fibers identify the chosen graph point with the quarter-turn value.
simpa [helperForRemark_5_24_5_quarterTurnMapping] using hmem i
-- After zero-extension, the stabilized graph relation matches the planar one exactly.
simp [X, XStar, hxStarEq, helperForRemark_5_24_5_stabilizedQuarterTurnMapping,
helperForRemark_5_24_5_stabilizedQuarterTurn_extendByZero]
have hineq := hcyclic k X XStar hmem'
-- The cyclic inequality for zero-extended data is identical to the planar cyclic inequality.
simpa [X, XStar, helperForRemark_5_24_5_extendByZero_sub,
helperForRemark_5_24_5_dotProduct_extendByZero] using hineq
Helper for Remark 5.24.5: the stabilized quarter-turn still fails cyclic monotonicity in every
dimension 2 + m.
lemma helperForRemark_5_24_5_stabilizedQuarterTurnMapping_not_cyclicallyMonotone
(m : ℕ) :
¬ IsCyclicallyMonotone (helperForRemark_5_24_5_stabilizedQuarterTurnMapping m) := by
intro hcyclic
-- Otherwise the planar quarter-turn would inherit cyclic monotonicity by restriction.
exact
helperForRemark_5_24_5_quarterTurnMapping_not_cyclicallyMonotone
(helperForRemark_5_24_5_quarterTurnMapping_cyclicallyMonotone_of_stabilized m hcyclic)
Helper for Remark 5.24.5: every dimension 2 + m already contains a monotone mapping that is
not cyclically monotone.
lemma helperForRemark_5_24_5_exists_monotone_not_cyclicallyMonotone_in_dimension_two_add
(m : ℕ) :
∃ ρ : (Fin (2 + m) → ℝ) → Set (Fin (2 + m) → ℝ),
IsMonotoneMultivaluedMapping ρ ∧ ¬ IsCyclicallyMonotone ρ := by
-- Package the stabilized quarter-turn as the witness in the higher-dimensional ambient space.
refine ⟨helperForRemark_5_24_5_stabilizedQuarterTurnMapping m, ?_, ?_⟩
· exact helperForRemark_5_24_5_stabilizedQuarterTurnMapping_monotone m
· exact helperForRemark_5_24_5_stabilizedQuarterTurnMapping_not_cyclicallyMonotone m
Helper for Remark 5.24.5: any natural number strictly larger than one can be reindexed as
2 + m. This isolates the arithmetic step needed to match the textbook statement n > 1 with the
explicit higher-dimensional construction above.
lemma helperForRemark_5_24_5_eq_two_add_of_one_lt
{n : ℕ} (hn : 1 < n) :
∃ m : ℕ, n = 2 + m := by
-- Peeling off two successors from `n` reduces the dimension claim to a pure arithmetic identity.
refine ⟨n - 2, ?_⟩
omega
Helper for Remark 5.24.5: once a dimension has been identified with 2 + m, the stabilized
quarter-turn witness transfers verbatim to that ambient space.
lemma helperForRemark_5_24_5_exists_monotone_not_cyclicallyMonotone_of_eq_two_add
{n m : ℕ} (hdim : n = 2 + m) :
∃ ρ : (Fin n → ℝ) → Set (Fin n → ℝ),
IsMonotoneMultivaluedMapping ρ ∧ ¬ IsCyclicallyMonotone ρ := by
-- After rewriting the dimension, the previously packaged `2 + m` counterexample applies unchanged.
subst hdim
exact helperForRemark_5_24_5_exists_monotone_not_cyclicallyMonotone_in_dimension_two_add m
Helper for Remark 5.24.5: once n = 2 + m, the counterexample can be chosen to come from the
explicit linear stabilized quarter-turn itself, viewed as a singleton-valued mapping.
lemma helperForRemark_5_24_5_exists_linearMapCounterexample_of_eq_two_add
{n m : ℕ} (hdim : n = 2 + m) :
∃ T : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ),
IsMonotoneMultivaluedMapping (fun x => ({T x} : Set (Fin n → ℝ))) ∧
¬ IsCyclicallyMonotone (fun x => ({T x} : Set (Fin n → ℝ))) := by
-- After rewriting the dimension, the stabilized quarter-turn itself is already a linear-map
-- witness for the singleton-valued counterexample.
subst hdim
refine ⟨helperForRemark_5_24_5_stabilizedQuarterTurnLinearMap m, ?_, ?_⟩
· -- Coercing the linear map to a function recovers the singleton-valued mapping proved monotone
-- above.
simpa [helperForRemark_5_24_5_stabilizedQuarterTurnMapping] using
helperForRemark_5_24_5_stabilizedQuarterTurnMapping_monotone m
· -- The same identified singleton-valued mapping still fails cyclic monotonicity.
simpa [helperForRemark_5_24_5_stabilizedQuarterTurnMapping] using
helperForRemark_5_24_5_stabilizedQuarterTurnMapping_not_cyclicallyMonotone m
Helper for Remark 5.24.5: once n = 2 + m, the counterexample can be chosen to come from the
explicit linear stabilized quarter-turn itself, viewed as a singleton-valued mapping.
lemma helperForRemark_5_24_5_exists_linearCounterexample_of_eq_two_add
{n m : ℕ} (hdim : n = 2 + m) :
∃ T : (Fin n → ℝ) → (Fin n → ℝ),
IsMonotoneMultivaluedMapping (fun x => ({T x} : Set (Fin n → ℝ))) ∧
¬ IsCyclicallyMonotone (fun x => ({T x} : Set (Fin n → ℝ))) := by
-- First produce the stronger linear-map witness, then forget the bundled linear structure.
rcases helperForRemark_5_24_5_exists_linearMapCounterexample_of_eq_two_add hdim with
⟨T, hmono, hnotCyclic⟩
exact ⟨T, hmono, hnotCyclic⟩
Helper for Remark 5.24.5: from the hypothesis 1 < n, one can choose both the decomposition
n = 2 + m and the corresponding stabilized quarter-turn counterexample in dimension n.
lemma helperForRemark_5_24_5_counterexample_data_of_one_lt
{n : ℕ} (hn : 1 < n) :
∃ m : ℕ, ∃ _ : n = 2 + m,
∃ ρ : (Fin n → ℝ) → Set (Fin n → ℝ),
IsMonotoneMultivaluedMapping ρ ∧ ¬ IsCyclicallyMonotone ρ := by
-- First reindex the dimension as `2 + m`, then transport the packaged witness along that identity.
rcases helperForRemark_5_24_5_eq_two_add_of_one_lt hn with ⟨m, hdim⟩
refine ⟨m, hdim, ?_⟩
exact helperForRemark_5_24_5_exists_monotone_not_cyclicallyMonotone_of_eq_two_add hdim
Helper for Remark 5.24.5: when n > 1, the counterexample can be packaged simultaneously as a
multivalued mapping and as the singleton graph of a linear map. This is the exact bridge between
the bare existential statement of the remark and its explicit linear example.
lemma helperForRemark_5_24_5_exists_singletonLinearMapCounterexample_of_one_lt
{n : ℕ} (hn : 1 < n) :
∃ (ρ : (Fin n → ℝ) → Set (Fin n → ℝ)) (T : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ)),
ρ = (fun x => ({T x} : Set (Fin n → ℝ))) ∧
IsMonotoneMultivaluedMapping ρ ∧ ¬ IsCyclicallyMonotone ρ := by
-- Reindex the dimension as `2 + m`, then choose the stabilized quarter-turn linear witness in
-- that ambient space.
rcases helperForRemark_5_24_5_eq_two_add_of_one_lt hn with ⟨m, hdim⟩
rcases helperForRemark_5_24_5_exists_linearMapCounterexample_of_eq_two_add hdim with
⟨T, hmono, hnotCyclic⟩
-- Taking the singleton graph of the chosen linear map produces the required multivalued mapping.
refine ⟨(fun x => ({T x} : Set (Fin n → ℝ))), T, rfl, hmono, hnotCyclic⟩
Helper for Remark 5.24.5: the hypothesis n > 1 already yields the final existential
counterexample promised by the remark, after forgetting the auxiliary decomposition n = 2 + m.
lemma helperForRemark_5_24_5_exists_monotone_not_cyclicallyMonotone_of_one_lt
{n : ℕ} (hn : 1 < n) :
∃ ρ : (Fin n → ℝ) → Set (Fin n → ℝ),
IsMonotoneMultivaluedMapping ρ ∧ ¬ IsCyclicallyMonotone ρ := by
-- Forget the linear realization and retain only the multivalued mapping promised by the remark.
rcases helperForRemark_5_24_5_exists_singletonLinearMapCounterexample_of_one_lt hn with
⟨ρ, _T, _hρ, hmono, hnotCyclic⟩
exact ⟨ρ, hmono, hnotCyclic⟩
Helper for Remark 5.24.5: the hypothesis n > 1 allows the counterexample to be chosen as a
linear map whose singleton graph is monotone but not cyclically monotone.
lemma helperForRemark_5_24_5_exists_linearMapCounterexample_of_one_lt
{n : ℕ} (hn : 1 < n) :
∃ T : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ),
IsMonotoneMultivaluedMapping (fun x => ({T x} : Set (Fin n → ℝ))) ∧
¬ IsCyclicallyMonotone (fun x => ({T x} : Set (Fin n → ℝ))) := by
-- The bridge helper already packages the same counterexample together with the required
-- singleton-graph identification.
rcases helperForRemark_5_24_5_exists_singletonLinearMapCounterexample_of_one_lt hn with
⟨ρ, T, hρ, hmono, hnotCyclic⟩
refine ⟨T, ?_, ?_⟩
· -- Rewriting the identified mapping recovers the singleton graph of `T`.
simpa [hρ] using hmono
· -- The non-cyclic-monotonicity statement transports across the same identification.
simpa [hρ] using hnotCyclic
Helper for Remark 5.24.5: the linear counterexample can be chosen so that every vector is
orthogonal to its image. This makes the quarter-turn nature of the textbook example explicit in
every dimension n > 1.
lemma helperForRemark_5_24_5_exists_orthogonalLinearMapCounterexample_of_one_lt
{n : ℕ} (hn : 1 < n) :
∃ T : (Fin n → ℝ) →ₗ[ℝ] (Fin n → ℝ),
(∀ x, dotProduct x (T x) = 0) ∧
IsMonotoneMultivaluedMapping (fun x => ({T x} : Set (Fin n → ℝ))) ∧
¬ IsCyclicallyMonotone (fun x => ({T x} : Set (Fin n → ℝ))) := by
-- Reindex the ambient space as `R^(2+m)` so the stabilized quarter-turn can be used directly.
rcases helperForRemark_5_24_5_eq_two_add_of_one_lt hn with ⟨m, rfl⟩
refine ⟨helperForRemark_5_24_5_stabilizedQuarterTurnLinearMap m, ?_, ?_, ?_⟩
· -- The stabilized quarter-turn is skew, so every vector is orthogonal to its image.
intro x
exact helperForRemark_5_24_5_dotProduct_self_stabilizedQuarterTurn m x
· -- Its singleton graph is monotone by the previously established multivalued-mapping argument.
simpa [helperForRemark_5_24_5_stabilizedQuarterTurnMapping] using
helperForRemark_5_24_5_stabilizedQuarterTurnMapping_monotone m
· -- The same witness still violates cyclic monotonicity in the larger space.
simpa [helperForRemark_5_24_5_stabilizedQuarterTurnMapping] using
helperForRemark_5_24_5_stabilizedQuarterTurnMapping_not_cyclicallyMonotone m
Helper for Remark 5.24.5: the hypothesis n > 1 allows the counterexample to be chosen as a
linear map whose singleton graph is monotone but not cyclically monotone.
lemma helperForRemark_5_24_5_exists_linearCounterexample_of_one_lt
{n : ℕ} (hn : 1 < n) :
∃ T : (Fin n → ℝ) → (Fin n → ℝ),
IsMonotoneMultivaluedMapping (fun x => ({T x} : Set (Fin n → ℝ))) ∧
¬ IsCyclicallyMonotone (fun x => ({T x} : Set (Fin n → ℝ))) := by
-- Use the stronger bundled linear-map witness and then forget only the extra structure.
rcases helperForRemark_5_24_5_exists_linearMapCounterexample_of_one_lt hn with
⟨T, hmono, hnotCyclic⟩
exact ⟨T, hmono, hnotCyclic⟩
Remark 5.24.5: When n > 1, there exist monotone mappings that are not cyclically monotone.
A linear example illustrates the distinction.
theorem exists_monotone_not_cyclicallyMonotone_of_one_lt
{n : ℕ} (hn : 1 < n) :
∃ ρ : (Fin n → ℝ) → Set (Fin n → ℝ),
IsMonotoneMultivaluedMapping ρ ∧ ¬ IsCyclicallyMonotone ρ := by
-- The stabilized quarter-turn singleton graph is exactly the linear counterexample promised by
-- the remark, so the previously packaged existential helper closes the statement immediately.
exact helperForRemark_5_24_5_exists_monotone_not_cyclicallyMonotone_of_one_lt hnend Section24end Chap05