[GOAL]
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f p
[PROOFSTEP]
rcases p.trichotomy with (rfl | rfl | _h)
[GOAL]
case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f 0
[PROOFSTEP]
exact memℓp_zero_iff.mpr {i : α | f i ≠ 0}.toFinite
[GOAL]
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Finite α
f : (i : α) → E i
⊢ Memℓp f ⊤
[PROOFSTEP]
exact memℓp_infty_iff.mpr (Set.Finite.bddAbove (Set.range fun i : α => ‖f i‖).toFinite)
[GOAL]
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < ENNReal.toReal p
⊢ Memℓp f p
[PROOFSTEP]
cases nonempty_fintype α
[GOAL]
case inr.inr.intro
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Finite α
f : (i : α) → E i
_h : 0 < ENNReal.toReal p
val✝ : Fintype α
⊢ Memℓp f p
[PROOFSTEP]
exact memℓp_gen ⟨Finset.univ.sum _, hasSum_fintype _⟩
[GOAL]
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
[PROOFSTEP]
rcases p.trichotomy with (rfl | rfl | h)
[GOAL]
case inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E 0 }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
[PROOFSTEP]
rw [PiLp.norm_eq_card, lp.norm_eq_card_dsupport]
[GOAL]
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E ⊤ }
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
[PROOFSTEP]
rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]
[GOAL]
case inr.inl
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
inst✝ : Fintype α
f : { x // x ∈ lp E ⊤ }
⊢ ⨆ (i : α), ‖↑Equiv.lpPiLp f i‖ = ⨆ (i : α), ‖↑f i‖
[PROOFSTEP]
rfl
[GOAL]
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
h : 0 < ENNReal.toReal p
⊢ ‖↑Equiv.lpPiLp f‖ = ‖f‖
[PROOFSTEP]
rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]
[GOAL]
case inr.inr
α : Type u_1
E : α → Type u_2
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
p : ℝ≥0∞
inst✝ : Fintype α
f : { x // x ∈ lp E p }
h : 0 < ENNReal.toReal p
⊢ (Finset.sum Finset.univ fun i => ‖↑Equiv.lpPiLp f i‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p) =
    (Finset.sum Finset.univ fun b => ‖↑f b‖ ^ ENNReal.toReal p) ^ (1 / ENNReal.toReal p)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
E : Type u_2
R : Type u_3
A : Type u_4
𝕜 : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : DiscreteTopology α
inst✝⁶ : NormedRing A
inst✝⁵ : NormOneClass A
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NonUnitalNormedRing R
src✝ : { x // x ∈ lp (fun x => E) ⊤ } ≃+ (α →ᵇ E) := AddEquiv.lpBcf
f : { x // x ∈ lp (fun x => E) ⊤ }
⊢ ‖↑{
            toLinearMap :=
              {
                toAddHom :=
                  { toFun := src✝.toFun,
                    map_add' :=
                      (_ :
                        ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                          Equiv.toFun src✝.toEquiv (x + y) = Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) },
                map_smul' :=
                  (_ :
                    ∀ (k : 𝕜) (f : { x // x ∈ lp (fun x => E) ⊤ }),
                      AddHom.toFun
                          { toFun := src✝.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                  Equiv.toFun src✝.toEquiv (x + y) =
                                    Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
                          (k • f) =
                        AddHom.toFun
                          { toFun := src✝.toFun,
                            map_add' :=
                              (_ :
                                ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                  Equiv.toFun src✝.toEquiv (x + y) =
                                    Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
                          (k • f)) },
            invFun := src✝.invFun, left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
            right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
        f‖ =
    ‖f‖
[PROOFSTEP]
simp only [norm_eq_iSup_norm, lp.norm_eq_ciSup]
[GOAL]
α : Type u_1
E : Type u_2
R : Type u_3
A : Type u_4
𝕜 : Type u_5
inst✝⁸ : TopologicalSpace α
inst✝⁷ : DiscreteTopology α
inst✝⁶ : NormedRing A
inst✝⁵ : NormOneClass A
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAlgebra 𝕜 A
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : NonUnitalNormedRing R
src✝ : { x // x ∈ lp (fun x => E) ⊤ } ≃+ (α →ᵇ E) := AddEquiv.lpBcf
f : { x // x ∈ lp (fun x => E) ⊤ }
⊢ ⨆ (x : α),
      ‖↑(↑{
                  toLinearMap :=
                    {
                      toAddHom :=
                        { toFun := AddEquiv.lpBcf.toEquiv.toFun,
                          map_add' :=
                            (_ :
                              ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                Equiv.toFun src✝.toEquiv (x + y) =
                                  Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) },
                      map_smul' :=
                        (_ :
                          ∀ (k : 𝕜) (f : { x // x ∈ lp (fun x => E) ⊤ }),
                            AddHom.toFun
                                { toFun := src✝.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                        Equiv.toFun src✝.toEquiv (x + y) =
                                          Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
                                (k • f) =
                              AddHom.toFun
                                { toFun := src✝.toFun,
                                  map_add' :=
                                    (_ :
                                      ∀ (x y : { x // x ∈ lp (fun x => E) ⊤ }),
                                        Equiv.toFun src✝.toEquiv (x + y) =
                                          Equiv.toFun src✝.toEquiv x + Equiv.toFun src✝.toEquiv y) }
                                (k • f)) },
                  invFun := AddEquiv.lpBcf.toEquiv.invFun,
                  left_inv := (_ : Function.LeftInverse src✝.invFun src✝.toFun),
                  right_inv := (_ : Function.RightInverse src✝.invFun src✝.toFun) }
              f)
          x‖ =
    ⨆ (i : α), ‖↑f i‖
[PROOFSTEP]
rfl
