case refine'_1
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.47553
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ Real.IsConjugateExponent (ENNReal.toReal 2) (ENNReal.toReal 2)

case refine'_2
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.47553
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ ∀ (i : ι), ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.47553
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ Summable fun i => inner (↑f i) (↑g i)
refine' summable_of_norm_bounded (fun i => ‖f i‖ * ‖g i‖) (lp.summable_mul _ f g) _
case refine'_2
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.47553
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
i : ι
⊢ ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i
case refine'_2
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.47553
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ ∀ (i : ι), ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i
intro i
no goals
case refine'_2
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.47553
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
i : ι
⊢ ‖inner (↑f i) (↑g i)‖ ≤ (fun i => ‖↑f i‖ * ‖↑g i‖) i
exact norm_inner_le_norm (𝕜 := 𝕜) _ _
no goals
case refine'_1
ι : Type u_1
𝕜 : Type u_3
inst✝⁴ : IsROrC 𝕜
E : Type ?u.47553
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
cplt : CompleteSpace E
G : ι → Type u_2
inst✝¹ : (i : ι) → NormedAddCommGroup (G i)
inst✝ : (i : ι) → InnerProductSpace 𝕜 (G i)
f g : { x // x ∈ lp G 2 }
⊢ Real.IsConjugateExponent (ENNReal.toReal 2) (ENNReal.toReal 2)
rw [Real.isConjugateExponent_iff] <;> norm_num