Can't prove convergence of PiLp

Stream: mathlib4

[fra guu]

instance instNorm : Norm (PiLp p β) where
  norm f :=
    if p = 0 then {i | ‖f i‖ ≠ 0}.toFinite.toFinset.card
    else if p = ∞ then ⨆ i, ‖f i‖ else (∑ i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal)

I want to prove that (∑ i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal) = ⨆ i, ‖f i‖ when p = ∞.

From the theorem below we know that p.toReal = 0 when p = ∞.

When f = 0 and $0^0$ = 1, we get (∑ i, 1) ^ (1 / 0). Then we get (∑ i, 1) ^ 0 because of div_zero.

At last we get 1. However, ⨆ i, ‖f i‖ equals 0 when f = 0. So it seems to be impossible to prove the equality when f = 0.

So I stopped at this simple case and don't know if it's possible to prove.

theorem toReal_eq_zero_iff (x : ℝ≥0∞) : x.toReal = 0 ↔ x = 0 ∨ x = ∞

theorem div_zero (a : G₀) : a / 0 = 0

[Eric Wieser]

Can you be a little clearer about what your question is? You included three code blocks above, but I can work out if you're asking about them.

[Eric Wieser]

If your question is really:

example (h : p = ∞) : (∑ i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal) = ⨆ i, ‖f i‖ := sorry

then I'm afraid you're out of luck because as you remark this is false

[Eric Wieser]

Maybe what you intended to show is the behavior taking the limit over p?

[Eric Wieser]

Which I guess amounts to showing that Continuous fun p => ‖(WithLp.equiv p _).symm f‖

[fra guu]

Eric Wieser said:

If your question is really:

example (h : p = ∞) : (∑ i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal) = ⨆ i, ‖f i‖ := sorry

then I'm afraid you're out of luck because as you remark this is false

Yes，this is exactly what I want.

I have defined LpNorm and want to prove its convergence and continuity on $[1, \infty)$ as below.

Maybe it's proper to use tendsto rather than = to describe the convergence.

In lpnorm_continuous_p , I tried to apply? and find ContinuousOn.if may be useful, but the first subgoal it generates is exactly the = version of lpnorm_tendsto_maxnorm after some steps, which seems to be impossbile.

Maybe I should prove that lpnorm tendsto to maxnorm when p tendsto infinity rather than prove the equality when p = ∞. However, I don't know how to build the connection between the two cases, are they defined to be equal?

As for the continuity, is it possible to prove only if p ≠ ∞?

import Mathlib.Analysis.SpecialFunctions.Pow.Real

noncomputable section

open scoped ENNReal

variable {m n 𝕂 : Type*}
variable [RCLike 𝕂] [Fintype m] [Fintype n]

def LpNorm (p : ℝ≥0∞) (M : Matrix m n 𝕂) : ℝ :=
  if p = ∞ then ⨆ i, ⨆ j, ‖M i j‖
  else (∑ i, ∑ j, ‖M i j‖ ^ p.toReal) ^ (1 / p.toReal)

variable (p : ℝ≥0∞)

theorem lpnorm_tendsto_maxnorm [Fact (1 ≤ p)] (h : p = ∞) (M : Matrix m n 𝕂) :
    (∑ i, ∑ j, ‖M i j‖ ^ p.toReal) ^ (1 / p.toReal) =  ⨆ i, ⨆ j, ‖M i j‖ := sorry

theorem lpnorm_continuous_p (A : Matrix m n 𝕂) :
    ContinuousOn ((LpNorm (m := m) (n := n) (𝕂 := 𝕂) (M := A))) {p | 1 ≤ p} := by
  refine ContinuousOn.if ?hp ?hf ?hg
  · simp only [Set.setOf_eq_eq_singleton, Set.mem_inter_iff, Set.mem_setOf_eq, and_imp]
    intro p pge1 pinf
    simp only [frontier, closure_singleton, interior_singleton, Set.diff_empty,
      Set.mem_singleton_iff] at pinf
    sorry
  · sorry
  · sorry

end