Lean4
@[simp]
theorem idealOfSet_ofIdeal_eq_closure (I : Ideal C(X, 𝕜)) : idealOfSet 𝕜 (setOfIdeal I) = I.closure := by
/- Since `idealOfSet 𝕜 (setOfIdeal I)` is closed and contains `I`, it contains `I.closure`.
For the reverse inclusion, given `f ∈ idealOfSet 𝕜 (setOfIdeal I)` and `(ε : ℝ≥0) > 0` it
suffices to show that `f` is within `ε` of `I`. -/
refine
le_antisymm ?_
((idealOfSet_closed 𝕜 <| setOfIdeal I).closure_subset_iff.mpr fun f hf x hx => notMem_setOfIdeal.mp hx hf)
refine (fun f hf => Metric.mem_closure_iff.mpr fun ε hε => ?_)
lift ε to ℝ≥0 using hε.lt.le
replace hε := show (0 : ℝ≥0) < ε from hε
simp_rw [dist_nndist]
norm_cast
-- Let `t := {x : X | ε / 2 ≤ ‖f x‖₊}}` which is closed and disjoint from `set_of_ideal I`.
set t := {x : X | ε / 2 ≤ ‖f x‖₊}
have ht : IsClosed t := isClosed_le continuous_const (map_continuous f).nnnorm
have htI : Disjoint t (setOfIdeal I)ᶜ :=
by
refine Set.subset_compl_iff_disjoint_left.mp fun x hx => ?_
simpa only [t, Set.mem_setOf, Set.mem_compl_iff, not_le] using
(nnnorm_eq_zero.mpr (mem_idealOfSet.mp hf hx)).trans_lt
(half_pos hε)
/- It suffices to produce `g : C(X, ℝ≥0)` which takes values in `[0,1]` and is constantly `1` on
`t` such that when composed with the natural embedding of `ℝ≥0` into `𝕜` lies in the ideal `I`.
Indeed, then `‖f - f * ↑g‖ ≤ ‖f * (1 - ↑g)‖ ≤ ⨆ ‖f * (1 - ↑g) x‖`. When `x ∉ t`, `‖f x‖ < ε / 2`
and `‖(1 - ↑g) x‖ ≤ 1`, and when `x ∈ t`, `(1 - ↑g) x = 0`, and clearly `f * ↑g ∈ I`. -/
suffices ∃ g : C(X, ℝ≥0), (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g ∈ I ∧ (∀ x, g x ≤ 1) ∧ t.EqOn g 1
by
obtain ⟨g, hgI, hg, hgt⟩ := this
refine ⟨f * (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g, I.mul_mem_left f hgI, ?_⟩
rw [nndist_eq_nnnorm]
refine (nnnorm_lt_iff _ hε).2 fun x => ?_
simp only [coe_sub, coe_mul, Pi.sub_apply, Pi.mul_apply]
by_cases hx : x ∈ t
·
simpa only [hgt hx, comp_apply, Pi.one_apply, ContinuousMap.coe_coe, algebraMapCLM_apply, map_one, mul_one,
sub_self, nnnorm_zero] using hε
· refine lt_of_le_of_lt ?_ (half_lt_self hε)
have :=
calc
‖((1 - (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x : 𝕜)‖₊ = ‖1 - algebraMap ℝ≥0 𝕜 (g x)‖₊ := by
simp only [coe_sub, coe_one, coe_comp, ContinuousMap.coe_coe, Pi.sub_apply, Pi.one_apply,
Function.comp_apply, algebraMapCLM_apply]
_ = ‖algebraMap ℝ≥0 𝕜 (1 - g x)‖₊ := by
simp only [Algebra.algebraMap_eq_smul_one, NNReal.smul_def, NNReal.coe_sub (hg x), NNReal.coe_one, sub_smul,
one_smul]
_ ≤ 1 := (nnnorm_algebraMap_nnreal 𝕜 (1 - g x)).trans_le tsub_le_self
calc
‖f x - f x * (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g x‖₊ =
‖f x * (1 - (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ :=
by simp only [mul_sub, coe_sub, coe_one, Pi.sub_apply, Pi.one_apply, mul_one]
_ ≤ ε / 2 * ‖(1 - (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) x‖₊ :=
((nnnorm_mul_le _ _).trans (mul_le_mul_right' (not_le.mp <| show ¬ε / 2 ≤ ‖f x‖₊ from hx).le _))
_ ≤ ε / 2 := by
simpa only [mul_one] using
mul_le_mul_left' this
_
/- There is some `g' : C(X, ℝ≥0)` which is strictly positive on `t` such that the composition
`↑g` with the natural embedding of `ℝ≥0` into `𝕜` lies in `I`. This follows from compactness of
`t` and that we can do it in any neighborhood of a point `x ∈ t`. Indeed, since `x ∈ t`, then
`fₓ x ≠ 0` for some `fₓ ∈ I` and so `fun y ↦ ‖(star fₓ * fₓ) y‖₊` is strictly positive in a
neighborhood of `y`. Moreover, `(‖(star fₓ * fₓ) y‖₊ : 𝕜) = (star fₓ * fₓ) y`, so composition of
this map with the natural embedding is just `star fₓ * fₓ ∈ I`. -/
have : ∃ g' : C(X, ℝ≥0), (algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g' ∈ I ∧ ∀ x ∈ t, 0 < g' x :=
by
refine ht.isCompact.induction_on ?_ ?_ ?_ ?_
· refine ⟨0, ?_, fun x hx => False.elim hx⟩
convert I.zero_mem
ext
simp only [comp_apply, zero_apply, ContinuousMap.coe_coe, map_zero]
· rintro s₁ s₂ hs ⟨g, hI, hgt⟩; exact ⟨g, hI, fun x hx => hgt x (hs hx)⟩
· rintro s₁ s₂ ⟨g₁, hI₁, hgt₁⟩ ⟨g₂, hI₂, hgt₂⟩
refine ⟨g₁ + g₂, ?_, fun x hx => ?_⟩
· convert I.add_mem hI₁ hI₂
ext y
simp only [coe_add, Pi.add_apply, map_add, coe_comp, Function.comp_apply, ContinuousMap.coe_coe]
· rcases hx with (hx | hx)
· simpa only [zero_add] using add_lt_add_of_lt_of_le (hgt₁ x hx) zero_le'
· simpa only [zero_add] using add_lt_add_of_le_of_lt zero_le' (hgt₂ x hx)
· intro x hx
replace hx := htI.subset_compl_right hx
rw [compl_compl, mem_setOfIdeal] at hx
obtain ⟨g, hI, hgx⟩ := hx
have := (map_continuous g).continuousAt.eventually_ne hgx
refine
⟨{y : X | g y ≠ 0} ∩ t, mem_nhdsWithin_iff_exists_mem_nhds_inter.mpr ⟨_, this, Set.Subset.rfl⟩,
⟨⟨fun x => ‖g x‖₊ ^ 2, (map_continuous g).nnnorm.pow 2⟩, ?_, fun x hx => pow_pos (norm_pos_iff.mpr hx.1) 2⟩⟩
convert I.mul_mem_left (star g) hI
ext
simp only [comp_apply, ContinuousMap.coe_coe, coe_mk, algebraMapCLM_apply, map_pow, mul_apply, star_apply,
star_def]
simp only [RCLike.conj_mul]
rfl
/- Get the function `g'` which is guaranteed to exist above. By the extreme value theorem and
compactness of `t`, there is some `0 < c` such that `c ≤ g' x` for all `x ∈ t`. Then by
`exists_mul_le_one_eqOn_ge` there is some `g` for which `g * g'` is the desired function. -/
obtain ⟨g', hI', hgt'⟩ := this
obtain ⟨c, hc, hgc'⟩ : ∃ c > 0, ∀ y : X, y ∈ t → c ≤ g' y :=
t.eq_empty_or_nonempty.elim (fun ht' => ⟨1, zero_lt_one, fun y hy => False.elim (by rwa [ht'] at hy)⟩) fun ht' =>
let ⟨x, hx, hx'⟩ := ht.isCompact.exists_isMinOn ht' (map_continuous g').continuousOn
⟨g' x, hgt' x hx, hx'⟩
obtain ⟨g, hg, hgc⟩ := exists_mul_le_one_eqOn_ge g' hc
refine ⟨g * g', ?_, hg, hgc.mono hgc'⟩
convert I.mul_mem_left ((algebraMapCLM ℝ≥0 𝕜 : C(ℝ≥0, 𝕜)).comp g) hI'
ext
simp only [algebraMapCLM_coe, comp_apply, mul_apply, ContinuousMap.coe_coe, map_mul]
