How do I use the default norm for EuclideanSpace?

Stream: new members

[Yongxi Lin (Aaron)]

I proved that the inclusion from ℤᵈ to ℝᵈ maps the filter of cofinite sets to the filter of cocompact sets and here is my code:

import Mathlib.Analysis.InnerProductSpace.PiL2
import Mathlib.Data.Real.StarOrdered

open Set
variable {d : Type*} [Fintype d]

lemma IntLattice.tendsto_coe_cofinite :
    Filter.Tendsto (fun n : d → ℤ => fun i => (n i : ℝ))
    Filter.cofinite (Filter.cocompact (EuclideanSpace ℝ d)) := by
  apply tendsto_cofinite_cocompact_iff.mpr ?_
  intro K hK
  obtain ⟨M, hM⟩ : ∃ M > 0, ∀ x ∈ K, @Norm.norm (EuclideanSpace ℝ d)
    SeminormedAddCommGroup.toSeminormedAddGroup.toNorm x ≤ M :=
    hK.isBounded.exists_pos_norm_le (E := EuclideanSpace ℝ d)
  have h_bound : ∀ n : d → ℤ, (fun i => (n i : ℝ)) ∈ K → ∀ i, |(n i : ℝ)| ≤ M := by
    intro n hn i
    simp [EuclideanSpace.norm_eq] at hM
    exact le_trans (Real.abs_le_sqrt (Finset.single_le_sum (fun a _ => sq_nonneg (n a : ℝ))
      (Finset.mem_univ i))) (hM.2 _ hn)
  have h_finite_components : ∀ i : d, Set.Finite {n : ℤ | |(n : ℝ)| ≤ M} := by
    refine fun i => Set.Finite.subset (Set.finite_Icc (-⌈M⌉) ⌈M⌉) ?_
    exact fun n hn => ⟨neg_le_of_abs_le <| by exact_mod_cast hn.out.trans <| Int.le_ceil _,
      le_of_abs_le <| by exact_mod_cast hn.out.trans <| Int.le_ceil _⟩
  exact Finite.subset (Finite.pi fun i => h_finite_components i) fun n hn => by aesop

One thing that I am very upset with my code is that I can't use the shortened notation ‖x‖ directly in the following lines:

  obtain ⟨M, hM⟩ : ∃ M > 0, ∀ x ∈ K, @Norm.norm (EuclideanSpace ℝ d)
    SeminormedAddCommGroup.toSeminormedAddGroup.toNorm x ≤ M :=
    hK.isBounded.exists_pos_norm_le (E := EuclideanSpace ℝ d)

The reason is that even though hK has type @IsCompact (d → ℝ) (PiLp.topologicalSpace 2 fun x ↦ ℝ) K, isBounded.exists_pos_norm_le still use E : d → ℝ instead of E : EuclideanSpace ℝ d so that ‖x‖ is interpreted as the supremum norm (Pi.normedRing) instead of the $l^2$ norm (and the latter is what I want).

I guess my question is: are there anyways that can make Lean automatically understand that I want the $l^2$ norm here so that I can use the notation ‖x‖?

[Etienne Marion]

That's because the function you are looking at does not take values in EuclideanSpace ℝ d but in d → ℝ. Your code is relying on defeq abuse between these two types. What you should do is use toLp 2 to transfer from d → ℝ to EuclideanSpace ℝ d.

import Mathlib

open Set WithLp

variable {d : Type*} [Fintype d]

lemma IntLattice.tendsto_coe_cofinite :
    Filter.Tendsto (fun n : d → ℤ => toLp 2 fun i => (n i : ℝ))
    Filter.cofinite (Filter.cocompact (EuclideanSpace ℝ d)) := by
  apply tendsto_cofinite_cocompact_iff.mpr ?_
  intro K hK
  obtain ⟨M, hM⟩ : ∃ M > 0, ∀ x ∈ K, ‖x‖ ≤ M :=
    hK.isBounded.exists_pos_norm_le
  have h_bound : ∀ n : d → ℤ, (toLp 2 fun i => (n i : ℝ)) ∈ K → ∀ i, |(n i : ℝ)| ≤ M := by
    intro n hn i
    simp [EuclideanSpace.norm_eq] at hM
    exact le_trans (Real.abs_le_sqrt (Finset.single_le_sum (fun a _ => sq_nonneg (n a : ℝ))
      (Finset.mem_univ i))) (hM.2 _ hn)
  have h_finite_components : ∀ i : d, Set.Finite {n : ℤ | |(n : ℝ)| ≤ M} := by
    refine fun i => Set.Finite.subset (Set.finite_Icc (-⌈M⌉) ⌈M⌉) ?_
    exact fun n hn => ⟨neg_le_of_abs_le <| by exact_mod_cast hn.out.trans <| Int.le_ceil _,
      le_of_abs_le <| by exact_mod_cast hn.out.trans <| Int.le_ceil _⟩
  exact Finite.subset (Finite.pi fun i => h_finite_components i) fun n hn => by aesop

Once the refactor in #27270 lands this defeq abuse won't be possible anymore.

[Yongxi Lin (Aaron)]

I see. Right now we haveEuclideanSpace ℝ d = WithLp 2 (d → ℝ) = d → ℝ.

[Yongxi Lin (Aaron)]

Thanks for your answer! @Etienne Marion

[Etienne Marion]

No problem. The thing is WithLp 2 (d → ℝ) and d → ℝ are equal as types but are not equipped with the same norm structure.