Why does definition of lp use a Pi-type?

Stream: new members

[Adomas Baliuka]

The definition of Memℓp here uses a dependent Pi-type:

variable {α : Type*} {E : α → Type*} {p q : ℝ≥0∞} [∀ i, NormedAddCommGroup (E i)]
def Memℓp (f : ∀ i, E i) (p : ℝ≥0∞) : Prop := ...

Why is a Pi-type used here?

I think an (f : ∀ i, E i) is a function that maps an i : α to an f i : E i, i.e., the output type may depend on the input value. On the other hand, [∀ i, NormedAddCommGroup (E i)] means that for a fixed i, we may add values (a b : E i). However, we cannot (for different (i j : α)) add values a : E i and (b : E j), can we? So how would one compute the lp-norm of a function where the output type actually depends on the input? Is such a thing used anywhere in Mathlib?

I tried to make an example where this Pi-type is used but it seems very convoluted and probably completely wrong

import Mathlib
abbrev myα := Fin 2

abbrev myE (a : myα) := if a = 0 then  ℝ else ℂ

instance fin2Topologicalsp (i : myα) : TopologicalSpace (myE i) where
  IsOpen _ := True
  isOpen_univ := by simp
  isOpen_inter := by simp
  isOpen_sUnion := by simp

def myE.zero : ((i : myα) → myE i) := by
  intro m
  simp [myE]
  by_cases m=0
  · simp [*]
    exact 0
  · simp [*]
    exact 0

def myE.add : ((i : myα) → myE i) → ((i : myα) → myE i) → (i : myα) → myE i := by
  intro m1 m2 i
  simp [myE]
  by_cases h : i=0
  · simp [*]
    let m1r : ℝ := m1 0
    let m2r : ℝ := m2 0
    exact m1r + m2r
  · simp [*]
    let m1r : ℂ := m1 1
    let m2r : ℂ := m2 1
    exact m1r + m2r

instance addCommm : AddCommMonoid ((i : myα) → myE i) where
  zero := myE.zero
  add := myE.add
  zero_add := by
    intro a
    sorry  -- I was not able to prove this
  add_zero := sorry
  add_comm := sorry
  nsmul := sorry
  nsmul_zero := by intros; sorry
  nsmul_succ := by intros; sorry
  add_assoc := by sorry


-- def mySummable (f : (i : myα) → myE i ) :=
--   @Summable (∀ (i : myα), myE i) myα (by infer_instance) fun (i : myα) ↦ f i
``

[Kevin Buzzard]

Why is a Pi-type used here?

I think an (f : ∀ i, E i) is a function that maps an i : α to an f i : E i

Right -- so $f$ is an element of the product $\prod_{i\in\alpha} E_i$, where each $E_i$ is a normed abelian group. Does this help? The predicate says that $\sum_{i\in\alpha}||f_i||^p$ converges, where $f_i$ (which Lean writes as f i, because it's thinking of $i\mapsto f_i$ as a dependent function) is the component at $i$.

Your sorrys will be hard to prove because you have (a) made definitions using tactic mode and (b) not made any API for those definitions before leaping into a big proof. I would recommend not trying to prove them until you've turned the definitions into ones which use only term mode for constructing data. Tactic mode is for proofs, it generates monstrous terms, but this doesn't matter for proofs because proofs are erased in the kernel. Data isn't. simp can generate monstrosities.

[Luigi Massacci]

Incidentally, would it make sense to make a PR changing those $\forall$ into $\prod$? I assume that's an artifact of the lean3 port from when lean4 didn't have $\prod$ as notation

[Adomas Baliuka]

Thanks for the explanation. I will give up on proving the stuff above (just did it to see if I have a correct intuition for what the types mean).

My main question remains: Is this used anywhere? Or is it "just in case" one needs it eventually and all current examples in Mathlib don't need this explicitly built-in product in the definition?

[Yaël Dillies]

Luigi Massacci said:

Incidentally, would it make sense to make a PR changing those $\forall$ into $\prod$? I assume that's an artifact of the lean3 port from when lean4 didn't have $\prod$ as notation

I would be happy with such a PR