NormedAddCommGroup (WithLp p α × β)

Stream: mathlib4

[Christopher Hoskin]

Please can someone advise why the following mwe doesn't work:

import Mathlib.Analysis.Normed.Lp.ProdLp
import Mathlib.Analysis.NormedSpace.MStructure

noncomputable section WithL1

open Real Set Filter RCLike Bornology Uniformity Topology NNReal ENNReal

variable (p : ℝ≥0∞) (𝕜 α β : Type*)

variable {p 𝕜 α β}
variable [NormedAddCommGroup α] [NormedAddCommGroup β]

def P1 : AddMonoid.End (WithLp p α × β) := (AddMonoidHom.inl α β).comp (AddMonoidHom.fst α β)

def P2 : AddMonoid.End (WithLp p α × β) := (AddMonoidHom.inr α β).comp (AddMonoidHom.snd α β)

variable (x : WithLp p α × β)

#check P1 x

lemma P1_idempotent : IsIdempotentElem (M := (AddMonoid.End (WithLp p α × β))) P1 := by
  rw [IsIdempotentElem, P1]
  rfl

variable [hp : Fact (1 ≤ p)]

noncomputable instance instProdNormedAddCommGroup :
    NormedAddCommGroup (WithLp p (α × β)) := {
       WithLp.instProdNormedAddCommGroup p α β with
  }

lemma P1_Lprojection :
  IsLprojection (WithLp p α × β) (M := (AddMonoid.End (WithLp p α × β))) P1 := sorry

end WithL1

Lemma P1_Lprojection (which I know is only true with the current def with p=1) produces the error message:

failed to synthesize
  NormedAddCommGroup (WithLp p α × β)

What am missing?

Thanks and Happy New Year!

Christopher

[Edward van de Meent]

i think you're looking for this:

lemma P1_Lprojection :
  IsLprojection (WithLp p (α × β)) (M := (AddMonoid.End (WithLp p (α × β)))) (P1 (p := p)) := sorry

[Christopher Hoskin]

This works as a statement:

lemma P1lproj :
  letI := WithLp.instProdNormedAddCommGroup 1 α β
  @IsLprojection (WithLp 1 α × β) (WithLp.instProdNormedAddCommGroup 1 α β)
    (AddMonoid.End (WithLp 1 α × β)) _ _ P1 := sorry

But then I get the same failed to synthesize NormedAddCommGroup (WithLp p α × β) message when trying to fill in the proof.

[Edward van de Meent]

i'm not sure why you're using WithLp p without the brackets... you do realise that it only does things when the argument is a pi type or product?

[Christopher Hoskin]

Edward van de Meent said:

i think you're looking for this:

lemma P1_Lprojection :
  IsLprojection (WithLp p (α × β)) (M := (AddMonoid.End (WithLp p (α × β)))) (P1 (p := p)) := sorry

Thanks - thought I'd tried that, but obviously not. It looks like it works!

[Edward van de Meent]

i.e. WithLp p α × β(which gets bracketed as (WithLp p α) × β) means "put the Lp norm on α, then use the maximum of the norms on the product", which i'm guessing doesn't respect addition?

[Christopher Hoskin]

Ah, it should be WithLp p (α × β) not WithLp p α × β - that was my typo.

[Christopher Hoskin]

I've drafted a PR #20380 - needs work though. Showing:

‖x.1‖ = ‖(x.1, 0)‖

for (x : WithLp p (α × β)) 0 < p < ∞ seems surprisingly difficult.

[Edward van de Meent]

do you mean ‖(WithLp.equiv p (α × β)).symm (x.1,0)‖, btw?

[Edward van de Meent]

otherwise lean might think you mean the maximum norm of α × β

[Christopher Hoskin]

@Edward van de Meent it's here: https://github.com/leanprover-community/mathlib4/pull/20380/files#diff-cb790f5ea1d9fce79724cd8acc3c53dab6d56b3c3e5f1d3b8844a0f9ad8ec162R356

on the left, @norm α NormedAddCommGroup.toNorm x.1 : ℝ and on the right @norm (WithLp p (α × β)) (WithLp.instProdNorm p α β) (x.1, 0) : ℝ.

[Edward van de Meent]

right.... my main concern here is that(from the snippets you send) you are abusing the fact that WithLp p is the identity. this is bad from a lemma application pov

[Edward van de Meent]

i think this file might benefit from the following:

protected def fst : α := (WithLp.equiv p (α × β) x).fst
protected def snd : β := (WithLp.equiv p (α × β) x).snd

@[simp]
theorem prod_fst {α β : Type*} (x : WithLp p (α × β)) : Prod.fst x = x.fst := rfl

@[simp]
theorem prod_snd {α β : Type*} (x : WithLp p (α × β)) : Prod.snd x = x.snd := rfl

with this, the simp normal form at least is immediately type correct.

[Christopher Hoskin]

@Edward van de Meent isn't that essentially what WithLp.equiv_fst and WithLp.equiv_snd do?

Did you mean for this to be added to Analysis/Normed/Lp/ProdLp?

[Edward van de Meent]

no. currently, the normal form uses Prod.fst and Prod.snd, which forces defeq abuse

[Edward van de Meent]

making WithLp.fst and -snd available in the file makes it automagically use this version tho, so the fix is very light

[Edward van de Meent]

aamof, the change really only needs 3 lines of code on all of mathlib, imma PR this in a minute

[Eric Wieser]

I'm not sure this is actually a good idea

[Edward van de Meent]

how so? this removes defeq abuse?

[Eric Wieser]

Certainly I don't like the strategy of having simp lemmas that use defeq abuse to try and avoid later defeq abuse

[Edward van de Meent]

those simp lemmas i posted actually aren't necessary, i think...

[Edward van de Meent]

i compiled mathlib without them

[Christopher Hoskin]

From my perspective, the main difficulty I was having was showing that:

a^ (p.toReal) ^ (1 / p.toReal) = a

This is almost NNReal.rpow_inv_rpow_self but not quite.

[Eric Wieser]

As for x.1 vs (WithLp.equiv p (α × β) x).fst when x : WithLp p (α × β), I think the latter is indeed the more principled, but in practice I think it just creates boilerplate. We already have something similar with x : WithLp p (α →β)and x i, and seem to largely get away with it

[Eric Wieser]

Christopher Hoskin said:

This is almost NNReal.rpow_inv_rpow_self but not quite.

It would certainly help if we were consistent in choosing between x ^ (1 / p) and x ^ (p⁻¹). My preference would be for the latter...

[Edward van de Meent]

Eric Wieser said:

but in practice I think it just creates boilerplate

from my local build run, it looks like the boilerplate already exists, but just using the wrong function :upside_down:

[Edward van de Meent]

no added simp lemmas needed, sheer existance of these functions seems to make all defeq abuse fly away

[Eric Wieser]

A little more precisely, I think the issue with #20380 is not defeq abuse of fst and snd, but defeq abuse of Prod.mk

[Edward van de Meent]

all that aside, i am of the opinion that WithLp.equiv is the wrong way around (or should come in the opposite flavour too)

[Eric Wieser]

Regarding the original topic, does docs#WihLp.norm_equiv_symm_fst make the proof any easier?

[Edward van de Meent]

#20385

[Eric Wieser]

Indeed,

lemma prod_norm_eq_add_P1 [Fact (1 ≤ p)] (hp : 0 < p.toReal) (x : WithLp p (α × β)) :
    ‖x‖ = (‖P1 x‖ ^ p.toReal + ‖(1 - P1) x‖ ^ p.toReal) ^ (1 / p.toReal) := by
  rw [WithLp.prod_norm_eq_add hp]
  rw [← WithLp.norm_equiv_symm_fst p α β x.1, ← WithLp.norm_equiv_symm_snd p α β x.2, P1_compl]
  rfl

works

[Eric Wieser]

Generally much of the LP library unecessarily assumes [Fact (1 ≤ p)] when it doesn't need it; I tried to fix this last year in #20389 (which I just promoted from a branch to a draft PR)

[Christopher Hoskin]

@Edward van de Meent @Eric Wieser thanks very much for your help. I've updated #20380 to use WithLp.norm_equiv_symm_fst and WithLp.norm_equiv_symm_snd with [Fact (1 ≤ p)] for now.