Supremum norm of continuous functions over compact sets

Stream: new members

[Giulio Caflisch]

I can work around it but it annoyes me that I cannot find a theorem in mathlib that says that for continuous functions over a compact space, like the one in the example below, the supremum norm is actually attained at some value of the function.

theorem my_problem (f : C(ℤ_[p], ℚ_[p])) : ∃ y : ℚ_[p], ‖y‖ = ‖f‖ := by

or equivalently

theorem my_problem' (f : C(ℤ_[p], ℚ_[p])) : ∃ x : ℤ_[p], ‖f x‖ = ‖f‖ := by

If you know how to do this it would shorten a proof of mine by a lot.
Thanks in advance for your help!

[Vincent Beffara]

You can probably use docs#IsCompact.exists_isMaxOn with s = univ or docs#isCompact_range

[Giulio Caflisch]

Ok thanks, I have something like already

obtain ⟨x, -, hx⟩ := (PadicInt.compactSpace p).isCompact_univ.exists_isMaxOn Set.univ_nonempty (map_continuous f).norm.continuousOn

But I don't know hot to tell Lean that ‖f x‖ = ‖f‖. Any hint?

[Vincent Beffara]

import Mathlib

variable [Fact (Nat.Prime p)]

theorem my_problem' (f : C(ℤ_[p], ℚ_[p])) : ∃ x : ℤ_[p], ‖f x‖ = ‖f‖ := by
  rw [ContinuousMap.norm_eq_iSup_norm]
  obtain ⟨x₀, hx₀⟩ := @IsCompact.exists_sSup_image_eq ℝ ℤ_[p] _ _ _ _ Set.univ ?_ ?_ (‖f ·‖) (by fun_prop)
  use x₀
  rw [← hx₀.2]
  sorry

[Vincent Beffara]

Fails because I didn't fill in the assumptions in line 2 but it reaches a state that should be provable.

[Vincent Beffara]

Namely:

import Mathlib

variable [Fact (Nat.Prime p)]

theorem my_problem' (f : C(ℤ_[p], ℚ_[p])) : ∃ x : ℤ_[p], ‖f x‖ = ‖f‖ := by
  rw [ContinuousMap.norm_eq_iSup_norm]
  obtain ⟨x₀, hx₀⟩ := @IsCompact.exists_sSup_image_eq ℝ ℤ_[p] _ _ _ _ Set.univ ?_ ?_ (‖f ·‖) (by fun_prop)
  use x₀
  rw [← hx₀.2]
  simp [sSup_range]

[Giulio Caflisch]

Thanks a lot. I really think the general case should be inserted in mathlib since it seems like it might be common to use

[Giulio Caflisch]

I rewrote it this way

theorem Padic.attained_sup_norm (f : C(ℤ_[p], ℚ_[p])) : ∃ x : ℤ_[p], ‖f x‖ = ‖f‖ := by
  rw [ContinuousMap.norm_eq_iSup_norm]
  obtain ⟨x, hx⟩ := (PadicInt.compactSpace p).isCompact_univ.exists_sSup_image_eq Set.univ_nonempty (map_continuous f).norm.continuousOn
  use x
  rw [← hx.2]
  simp [sSup_range]

and now it works completely. Again thanks for your time!

[Yoh Tanimoto]

it is not exactly what you write but you can use exist_norm_eq.

[Jireh Loreaux]

I think we want / need a version which yields an docs#IsGreatest to be most user-friendly.

[Vincent Beffara]

This version is nicer indeed:

import Mathlib

variable [Fact (Nat.Prime p)]

theorem my_problem' (f : C(ℤ_[p], ℚ_[p])) : ∃ x : ℤ_[p], ‖f x‖ = ‖f‖ :=
  exist_norm_eq (f := .mkOfCompact f) (by simp [compactlySupported_eq_top])