Lean4
/-- Induction step in M. Riesz extension theorem. Given a convex cone `s` in a vector space `E`,
a partially defined linear map `f : f.domain → ℝ`, assume that `f` is nonnegative on `f.domain ∩ p`
and `p + s = E`. If `f` is not defined on the whole `E`, then we can extend it to a larger
submodule without breaking the non-negativity condition. -/
theorem step (nonneg : ∀ x : f.domain, (x : E) ∈ s → 0 ≤ f x) (dense : ∀ y, ∃ x : f.domain, (x : E) + y ∈ s)
(hdom : f.domain ≠ ⊤) : ∃ g, f < g ∧ ∀ x : g.domain, (x : E) ∈ s → 0 ≤ g x :=
by
obtain ⟨y, -, hy⟩ : ∃ y ∈ ⊤, y ∉ f.domain := SetLike.exists_of_lt (lt_top_iff_ne_top.2 hdom)
obtain ⟨c, le_c, c_le⟩ :
∃ c, (∀ x : f.domain, -(x : E) - y ∈ s → f x ≤ c) ∧ ∀ x : f.domain, (x : E) + y ∈ s → c ≤ f x :=
by
set Sp := f '' {x : f.domain | (x : E) + y ∈ s}
set Sn := f '' {x : f.domain | -(x : E) - y ∈ s}
suffices (upperBounds Sn ∩ lowerBounds Sp).Nonempty by
simpa only [Sp, Sn, Set.Nonempty, upperBounds, lowerBounds, forall_mem_image] using this
refine exists_between_of_forall_le (Nonempty.image f ?_) (Nonempty.image f (dense y)) ?_
· rcases dense (-y) with ⟨x, hx⟩
rw [← neg_neg x, NegMemClass.coe_neg, ← sub_eq_add_neg] at hx
exact ⟨_, hx⟩
rintro a ⟨xn, hxn, rfl⟩ b ⟨xp, hxp, rfl⟩
have := s.add_mem hxp hxn
rw [add_assoc, add_sub_cancel, ← sub_eq_add_neg, ← AddSubgroupClass.coe_sub] at this
replace := nonneg _ this
rwa [f.map_sub, sub_nonneg] at this
refine ⟨f.supSpanSingleton y (-c) hy, ?_, ?_⟩
· refine lt_iff_le_not_ge.2 ⟨f.left_le_sup _ _, fun H => ?_⟩
replace H := LinearPMap.domain_mono.monotone H
rw [LinearPMap.domain_supSpanSingleton, sup_le_iff, span_le, singleton_subset_iff] at H
exact hy H.2
· rintro ⟨z, hz⟩ hzs
rcases mem_sup.1 hz with ⟨x, hx, y', hy', rfl⟩
rcases mem_span_singleton.1 hy' with ⟨r, rfl⟩
simp only at hzs
rw [LinearPMap.supSpanSingleton_apply_mk _ _ _ _ _ hx, smul_neg, ← sub_eq_add_neg, sub_nonneg]
rcases lt_trichotomy r 0 with (hr | hr | hr)
· have : -(r⁻¹ • x) - y ∈ s := by
rwa [← s.smul_mem_iff (neg_pos.2 hr), smul_sub, smul_neg, neg_smul, neg_neg, smul_smul, mul_inv_cancel₀ hr.ne,
one_smul, sub_eq_add_neg, neg_smul, neg_neg]
replace := le_c (r⁻¹ • ⟨x, hx⟩) this
rwa [← mul_le_mul_iff_right₀ (neg_pos.2 hr), neg_mul, neg_mul, neg_le_neg_iff, f.map_smul, smul_eq_mul, ←
mul_assoc, mul_inv_cancel₀ hr.ne, one_mul] at this
· subst r
simp only [zero_smul, add_zero] at hzs ⊢
apply nonneg
exact hzs
· have : r⁻¹ • x + y ∈ s := by rwa [← s.smul_mem_iff hr, smul_add, smul_smul, mul_inv_cancel₀ hr.ne', one_smul]
replace := c_le (r⁻¹ • ⟨x, hx⟩) this
rwa [← mul_le_mul_iff_right₀ hr, f.map_smul, smul_eq_mul, ← mul_assoc, mul_inv_cancel₀ hr.ne', one_mul] at this
