Imports
module
public import Mathlib.Analysis.InnerProductSpace.Calculus
public import Mathlib.Analysis.InnerProductSpace.ProdL2
Inner product space
In this module we define the type class InnerProductSpace' 𝕜 E which is a
generalization of InnerProductSpace 𝕜 E, as it does not require the condition ‖x‖^2 = ⟪x,x⟫
but instead the condition ∃ (c > 0) (d > 0), c • ‖x‖^2 ≤ ⟪x,x⟫ ≤ d • ‖x‖^2.
Instead E is equipped with a L₂ norm ‖x‖₂ which satisfies ‖x‖₂ = √⟪x,x⟫.
This allows us to define the inner product space structure on product types E × F and
pi types ι → E, which would otherwise not be possible due to the use of max norm on these types.
We define the following maps:
InnerProductSpace 𝕜 E → InnerProductSpace' 𝕜 E which sets ‖x‖₂ = ‖x‖.
InnerProductSpace' 𝕜 E → InnerProductSpace 𝕜 (WithLp 2 E) which uses the fact that the norm
defined on WithLp 2 E is L₂ norm.
@[ expose ] public section
L₂ norm on E.
In particular, on product types X×Y and pi types ι → X this class provides L₂ norm unlike ‖·‖.
class Norm₂ ( E : Type* ) where
norm₂ : E → ℝ
Effectively as InnerProductSpace 𝕜 E but it does not requires that ‖x‖^2 = ⟪x,x⟫. It is
only required that they are equivalent ∃ (c > 0) (d > 0), c • ‖x‖^2 ≤ ⟪x,x⟫ ≤ d • ‖x‖^2. The main
purpose of this class is to provide inner product space structure on product types ExF and
pi types ι → E without using WithLp gadget.
If you want to access L₂ norm use ‖x‖₂ := √⟪x,x⟫.
This class induces InnerProductSpace 𝕜 (WithLp 2 E) which equips ‖·‖ on X with L₂ norm.
This is very useful when translating results from InnerProductSpace to InnerProductSpace'
together with toL2 : E →L[𝕜] (WithLp 2 E) and fromL2 : (WithL2 2 E) →L[𝕜] E.
In short we have these implications:
InnerProductSpace 𝕜 E → InnerProductSpace' 𝕜 E
InnerProductSpace' 𝕜 E → InnerProductSpace 𝕜 (WithLp 2 E)
The reason behind this type class is that with current mathlib design the requirement
‖x‖^2 = ⟪x,x⟫ prevents us to give inner product space structure on product type E×F and pi
type ι → E as they are equipped with max norm. One has to work with WithLp 2 (E×F) and
WithLp 2 (ι → E). This places quite a bit inconvenience on users in certain scenarios.
In particular, the main motivation behind this class is to make computations of adjFDeriv and
gradient easy.
Core inner product properties.
The inner product induces the L₂ norm.
Norm induced by inner product is topologically equivalent to the given norm on E.
class InnerProductSpace' ( 𝕜 : Type* ) ( E : Type* ) [ RCLike 𝕜 ] [ NormedAddCommGroup E ] [ NormedSpace 𝕜 E ]
extends Norm₂ E where core : InnerProductSpace.Core 𝕜 E norm₂_sq_eq_re_inner : ∀ x : E , ‖ x ‖₂ ^ 2 = re ( core . inner x x ) inner_top_equiv_norm : ∃ c d : ℝ ,
0 < c ∧ 0 < d ∧
∀ x : E , ( c • ‖ x ‖ ^ 2 ≤ re ( core . inner x x ) ) ∧ ( re ( core . inner x x ) ≤ d • ‖ x ‖ ^ 2 )
B. Deriving the inner product structure on WithLp 2 E from InnerProductSpace' 𝕜 E
lemma norm_withLp2_eq_norm2 ( x : WithLp 2 E ) :
‖ x ‖ = | norm₂ ( WithLp.equiv 2 E x ) | := by 𝕜 : Type u_1 inst✝² : RCLike 𝕜 E : Type u_2 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E x : WithLp 2 E ⊢ ‖ x ‖ = | ‖ ( WithLp.equiv 2 E ) x ‖₂ |
rw [ show ‖ x ‖ = √ ( RCLike.re ⟪ WithLp.equiv 2 E x , WithLp.equiv 2 E x ⟫ ) from rfl , 𝕜 : Type u_1 inst✝² : RCLike 𝕜 E : Type u_2 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E x : WithLp 2 E ⊢ √ ( re ⟪ ( WithLp.equiv 2 E ) x , ( WithLp.equiv 2 E ) x ⟫ ) = | ‖ ( WithLp.equiv 2 E ) x ‖₂ | All goals completed! 🐙
← norm₂_sq_eq_re_inner ( 𝕜 := 𝕜 ) ( WithLp.equiv 2 E x ) , 𝕜 : Type u_1 inst✝² : RCLike 𝕜 E : Type u_2 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E x : WithLp 2 E ⊢ √ ( ‖ ( WithLp.equiv 2 E ) x ‖₂ ^ 2 ) = | ‖ ( WithLp.equiv 2 E ) x ‖₂ | All goals completed! 🐙 Real.sqrt_sq_eq_abs 𝕜 : Type u_1 inst✝² : RCLike 𝕜 E : Type u_2 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E x : WithLp 2 E ⊢ | ‖ ( WithLp.equiv 2 E ) x ‖₂ | = | ‖ ( WithLp.equiv 2 E ) x ‖₂ | All goals completed! 🐙 ] All goals completed! 🐙 lemma fromL2_inner_left ( x : WithLp 2 E ) ( y : E ) : ⟪ fromL2 𝕜 x , y ⟫ = ⟪ x , toL2 𝕜 y ⟫ := rfl lemma ofLp_inner_left ( x : E ) ( y : WithLp 2 E ) : ⟪ WithLp.ofLp y , x ⟫ = ⟪ y , WithLp.toLp 2 x ⟫ :=
fromL2_inner_left y x lemma toL2_inner_left ( x : E ) ( y : WithLp 2 E ) : ⟪ toL2 𝕜 x , y ⟫ = ⟪ x , fromL2 𝕜 y ⟫ := rfl lemma toLp_inner_left ( x : WithLp 2 E ) ( y : E ) : ⟪ WithLp.toLp 2 y , x ⟫ = ⟪ y , WithLp.ofLp x ⟫ :=
toL2_inner_left y x @[ simp ]
lemma toL2_fromL2 ( x : WithLp 2 E ) : toL2 𝕜 ( fromL2 𝕜 x ) = x := rfl @[ simp ]
lemma fromL2_toL2 ( x : E ) : fromL2 𝕜 ( toL2 𝕜 x ) = x := rfl instance [ CompleteSpace E ] : CompleteSpace ( WithLp 2 E ) := by 𝕜 : Type u_1 inst✝⁹ : RCLike 𝕜 E : Type u_2 inst✝⁸ : NormedAddCommGroup E inst✝⁷ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E F : Type u_3 inst✝⁶ : NormedAddCommGroup F inst✝⁵ : NormedSpace 𝕜 F inst✝⁴ : InnerProductSpace' 𝕜 F G : Type u_4 inst✝³ : NormedAddCommGroup G inst✝² : NormedSpace 𝕜 G inst✝¹ : InnerProductSpace' 𝕜 G inst✝ : CompleteSpace E ⊢ CompleteSpace ( WithLp 2 E )
have e := ( equivL2 𝕜 E ) 𝕜 : Type u_1 inst✝⁹ : RCLike 𝕜 E : Type u_2 inst✝⁸ : NormedAddCommGroup E inst✝⁷ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E F : Type u_3 inst✝⁶ : NormedAddCommGroup F inst✝⁵ : NormedSpace 𝕜 F inst✝⁴ : InnerProductSpace' 𝕜 F G : Type u_4 inst✝³ : NormedAddCommGroup G inst✝² : NormedSpace 𝕜 G inst✝¹ : InnerProductSpace' 𝕜 G inst✝ : CompleteSpace E e : WithLp 2 E ≃L[ 𝕜 ] E ⊢ CompleteSpace ( WithLp 2 E )
have he := ContinuousLinearEquiv.isUniformEmbedding e 𝕜 : Type u_1 inst✝⁹ : RCLike 𝕜 E : Type u_2 inst✝⁸ : NormedAddCommGroup E inst✝⁷ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E F : Type u_3 inst✝⁶ : NormedAddCommGroup F inst✝⁵ : NormedSpace 𝕜 F inst✝⁴ : InnerProductSpace' 𝕜 F G : Type u_4 inst✝³ : NormedAddCommGroup G inst✝² : NormedSpace 𝕜 G inst✝¹ : InnerProductSpace' 𝕜 G inst✝ : CompleteSpace E e : WithLp 2 E ≃L[ 𝕜 ] E he : IsUniformEmbedding ⇑ e ⊢ CompleteSpace ( WithLp 2 E )
apply ( completeSpace_congr ( α := WithLp 2 E ) ( β := E ) ( e := e ) he ) . 2 𝕜 : Type u_1 inst✝⁹ : RCLike 𝕜 E : Type u_2 inst✝⁸ : NormedAddCommGroup E inst✝⁷ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E F : Type u_3 inst✝⁶ : NormedAddCommGroup F inst✝⁵ : NormedSpace 𝕜 F inst✝⁴ : InnerProductSpace' 𝕜 F G : Type u_4 inst✝³ : NormedAddCommGroup G inst✝² : NormedSpace 𝕜 G inst✝¹ : InnerProductSpace' 𝕜 G inst✝ : CompleteSpace E e : WithLp 2 E ≃L[ 𝕜 ] E he : IsUniformEmbedding ⇑ e ⊢ CompleteSpace E
infer_instance All goals completed! 🐙 lemma ext_inner_left' { x y : E } ( h : ∀ v , ⟪ v , x ⟫ = ⟪ v , y ⟫ ) : x = y :=
( WithLp.equiv 2 E ) . symm . injective <| ext_inner_left ( E := WithLp 2 E ) 𝕜 <| by 𝕜 : Type u_1 inst✝² : RCLike 𝕜 E : Type u_2 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E x : E y : E h : ∀ ( v : E ), ⟪ v , x ⟫ = ⟪ v , y ⟫ ⊢ ∀ ( v : WithLp 2 E ), ⟪ v , ( WithLp.equiv 2 E ) . symm x ⟫ = ⟪ v , ( WithLp.equiv 2 E ) . symm y ⟫
simpa [ ← ofLp_inner_left ] using fun v => h ( WithLp.ofLp v ) All goals completed! 🐙 @[ simp ]
lemma inner_conj_symm' ( x y : E ) : ⟪ y , x ⟫ † = ⟪ x , y ⟫ :=
inner_conj_symm ( E := WithLp 2 E ) _ _ lemma inner_smul_left' ( x y : E ) ( r : 𝕜 ) : ⟪ r • x , y ⟫ = r † * ⟪ x , y ⟫ :=
inner_smul_left ( E := WithLp 2 E ) _ _ r lemma inner_smul_right' ( x y : E ) ( r : 𝕜 ) : ⟪ x , r • y ⟫ = r * ⟪ x , y ⟫ :=
inner_smul_right ( E := WithLp 2 E ) _ _ r @[ simp ]
lemma inner_zero_left' ( x : E ) : ⟪ 0 , x ⟫ = 0 :=
inner_zero_left ( E := WithLp 2 E ) _ @[ simp ]
lemma inner_zero_right' ( x : E ) : ⟪ x , 0 ⟫ = 0 :=
inner_zero_right ( E := WithLp 2 E ) _ lemma inner_add_left' ( x y z : E ) : ⟪ x + y , z ⟫ = ⟪ x , z ⟫ + ⟪ y , z ⟫ :=
inner_add_left ( E := WithLp 2 E ) _ _ _ lemma inner_add_right' ( x y z : E ) : ⟪ x , y + z ⟫ = ⟪ x , y ⟫ + ⟪ x , z ⟫ :=
inner_add_right ( E := WithLp 2 E ) _ _ _ lemma inner_sub_left' ( x y z : E ) : ⟪ x - y , z ⟫ = ⟪ x , z ⟫ - ⟪ y , z ⟫ :=
inner_sub_left ( E := WithLp 2 E ) _ _ _ lemma inner_sub_right' ( x y z : E ) : ⟪ x , y - z ⟫ = ⟪ x , y ⟫ - ⟪ x , z ⟫ :=
inner_sub_right ( E := WithLp 2 E ) _ _ _ @[ simp ]
lemma inner_neg_left' ( x y : E ) : ⟪ - x , y ⟫ = - ⟪ x , y ⟫ :=
inner_neg_left ( E := WithLp 2 E ) _ _ @[ simp ]
lemma inner_neg_right' ( x y : E ) : ⟪ x , - y ⟫ = - ⟪ x , y ⟫ :=
inner_neg_right ( E := WithLp 2 E ) _ _
@[ simp ]
lemma inner_self_eq_zero' { x : E } : ⟪ x , x ⟫ = 0 ↔ x = 0 := by 𝕜 : Type u_1 inst✝² : RCLike 𝕜 E : Type u_2 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E x : E ⊢ ⟪ x , x ⟫ = 0 ↔ x = 0
rw [ show ( ⟪ x , x ⟫ : 𝕜 ) = inner 𝕜 ( toL2 𝕜 x ) ( toL2 𝕜 x ) from rfl , 𝕜 : Type u_1 inst✝² : RCLike 𝕜 E : Type u_2 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E x : E ⊢ ⟪ ( toL2 𝕜 ) x , ( toL2 𝕜 ) x ⟫ = 0 ↔ x = 0 All goals completed! 🐙 inner_self_eq_zero , 𝕜 : Type u_1 inst✝² : RCLike 𝕜 E : Type u_2 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E x : E ⊢ ( toL2 𝕜 ) x = 0 ↔ x = 0 All goals completed! 🐙
map_eq_zero_iff _ ( Function.LeftInverse.injective fromL2_toL2 ) 𝕜 : Type u_1 inst✝² : RCLike 𝕜 E : Type u_2 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E x : E ⊢ x = 0 ↔ x = 0 All goals completed! 🐙 ] All goals completed! 🐙 @[ simp ]
lemma inner_sum' { ι : Type* } [ Fintype ι ] ( x : E ) ( g : ι → E ) :
⟪ x , ∑ i , g i ⟫ = ∑ i , ⟪ x , g i ⟫ :=
map_sum ( AddMonoidHom.mk' ( fun y => ⟪ x , y ⟫ ) ( inner_add_right' x ) ) g Finset.univ @[ fun_prop ]
lemma Continuous.inner' { α } [ TopologicalSpace α ] ( f g : α → E )
( hf : Continuous f ) ( hg : Continuous g ) : Continuous ( fun a => ⟪ f a , g a ⟫ ) :=
Continuous.inner ( 𝕜 := 𝕜 ) ( E := WithLp 2 E ) ( f := fun x => toL2 𝕜 ( f x ) )
( g := fun x => toL2 𝕜 ( g x ) ) ( by 𝕜 : Type u_1 inst✝³ : RCLike 𝕜 E : Type u_2 inst✝² : NormedAddCommGroup E inst✝¹ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E α : Type u_5 inst✝ : TopologicalSpace α f : α → E g : α → E hf : Continuous f hg : Continuous g ⊢ Continuous fun x => ( toL2 𝕜 ) ( f x ) fun_prop All goals completed! 🐙 ) ( by 𝕜 : Type u_1 inst✝³ : RCLike 𝕜 E : Type u_2 inst✝² : NormedAddCommGroup E inst✝¹ : NormedSpace 𝕜 E hE : InnerProductSpace' 𝕜 E α : Type u_5 inst✝ : TopologicalSpace α f : α → E g : α → E hf : Continuous f hg : Continuous g ⊢ Continuous fun x => ( toL2 𝕜 ) ( g x ) fun_prop All goals completed! 🐙 ) local notation "⟪" x ", " y "⟫" => inner ℝ x y lemma real_inner_self_nonneg' { x : F } : 0 ≤ re ( ⟪ x , x ⟫ ) :=
real_inner_self_nonneg ( F := WithLp 2 F ) lemma real_inner_comm' ( x y : F ) : ⟪ y , x ⟫ = ⟪ x , y ⟫ :=
real_inner_comm ( F := WithLp 2 F ) _ _ @[ fun_prop ]
lemma ContDiffAt.inner' { f g : E → F } { x : E }
( hf : ContDiffAt ℝ n f x ) ( hg : ContDiffAt ℝ n g x ) :
ContDiffAt ℝ n ( fun x => ⟪ f x , g x ⟫ ) x :=
ContDiffAt.inner ℝ ( f := fun x => toL2 ℝ ( f x ) ) ( g := fun x => toL2 ℝ ( g x ) )
( by E : Type u_5 inst✝⁴ : NormedAddCommGroup E inst✝³ : NormedSpace ℝ E F : Type u_6 inst✝² : NormedAddCommGroup F inst✝¹ : NormedSpace ℝ F inst✝ : InnerProductSpace' ℝ F n : WithTop ℕ∞ f : E → F g : E → F x : E hf : ContDiffAt ℝ n f x hg : ContDiffAt ℝ n g x ⊢ ContDiffAt ℝ n (fun x => ( toL2 ℝ ) ( f x ) ) x fun_prop All goals completed! 🐙 ) ( by E : Type u_5 inst✝⁴ : NormedAddCommGroup E inst✝³ : NormedSpace ℝ E F : Type u_6 inst✝² : NormedAddCommGroup F inst✝¹ : NormedSpace ℝ F inst✝ : InnerProductSpace' ℝ F n : WithTop ℕ∞ f : E → F g : E → F x : E hf : ContDiffAt ℝ n f x hg : ContDiffAt ℝ n g x ⊢ ContDiffAt ℝ n (fun x => ( toL2 ℝ ) ( g x ) ) x fun_prop All goals completed! 🐙 ) @[ fun_prop ]
lemma ContDiff.inner' { f g : E → F }
( hf : ContDiff ℝ n f ) ( hg : ContDiff ℝ n g ) :
ContDiff ℝ n ( fun x => ⟪ f x , g x ⟫ ) :=
ContDiff.inner ℝ ( f := fun x => toL2 ℝ ( f x ) ) ( g := fun x => toL2 ℝ ( g x ) )
( by E : Type u_5 inst✝⁴ : NormedAddCommGroup E inst✝³ : NormedSpace ℝ E F : Type u_6 inst✝² : NormedAddCommGroup F inst✝¹ : NormedSpace ℝ F inst✝ : InnerProductSpace' ℝ F n : ℕ∞ω f : E → F g : E → F hf : ContDiff ℝ n f hg : ContDiff ℝ n g ⊢ ContDiff ℝ n fun x => ( toL2 ℝ ) ( f x ) fun_prop All goals completed! 🐙 ) ( by E : Type u_5 inst✝⁴ : NormedAddCommGroup E inst✝³ : NormedSpace ℝ E F : Type u_6 inst✝² : NormedAddCommGroup F inst✝¹ : NormedSpace ℝ F inst✝ : InnerProductSpace' ℝ F n : ℕ∞ω f : E → F g : E → F hf : ContDiff ℝ n f hg : ContDiff ℝ n g ⊢ ContDiff ℝ n fun x => ( toL2 ℝ ) ( g x ) fun_prop All goals completed! 🐙 ) local notation "⟪" x ", " y "⟫" => inner 𝕜 x y
Inner product on product types E×F defined as ⟪x,y⟫ = ⟪x.fst,y.fst⟫ + ⟪x.snd,y.snd⟫.
This is just local instance as it is superseded by the following instance for
InnerProductSpace'.
local instance : Inner 𝕜 ( E × F ) := ⟨ fun ( x , y ) ( x' , y' ) => ⟪ x , x' ⟫ + ⟪ y , y' ⟫ ⟩
@[ simp ]
lemma prod_inner_apply' ( x y : ( E × F ) ) : ⟪ x , y ⟫ = ⟪ x . fst , y . fst ⟫ + ⟪ x . snd , y . snd ⟫ := rfl local notation "⟪" x ", " y "⟫" => inner ℝ x y
lemma _root_.isBoundedBilinearMap_inner' :
IsBoundedBilinearMap ℝ fun p : E × E => ⟪ p . 1 , p . 2 ⟫ where
add_left := inner_add_left'
smul_left := fun r x y => by E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E r : ℝ x : E y : E ⊢ ⟪ ( r • x , y ) .1 , ( r • x , y ) .2 ⟫ = r • ⟪ ( x , y ) .1 , ( x , y ) .2 ⟫
simpa using inner_smul_left' x y r All goals completed! 🐙
add_right := inner_add_right'
smul_right := fun r x y => by E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E r : ℝ x : E y : E ⊢ ⟪ ( x , r • y ) .1 , ( x , r • y ) .2 ⟫ = r • ⟪ ( x , y ) .1 , ( x , y ) .2 ⟫
simpa using inner_smul_right' x y r All goals completed! 🐙
bound := by E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E ⊢ ∃ C > 0 , ∀ ( x y : E ), ‖ ⟪ ( x , y ) .1 , ( x , y ) .2 ⟫ ‖ ≤ C * ‖ x ‖ * ‖ y ‖
obtain ⟨ c , d , hc , hd , h ⟩ := hE . inner_top_equiv_norm E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c • ‖ x ‖ ^ 2 ≤ re ⟪ x , x ⟫ ∧ re ⟪ x , x ⟫ ≤ d • ‖ x ‖ ^ 2 ⊢ ∃ C > 0 , ∀ ( x y : E ), ‖ ⟪ ( x , y ) .1 , ( x , y ) .2 ⟫ ‖ ≤ C * ‖ x ‖ * ‖ y ‖
use d h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c • ‖ x ‖ ^ 2 ≤ re ⟪ x , x ⟫ ∧ re ⟪ x , x ⟫ ≤ d • ‖ x ‖ ^ 2 ⊢ d > 0 ∧ ∀ ( x y : E ), ‖ ⟪ ( x , y ) .1 , ( x , y ) .2 ⟫ ‖ ≤ d * ‖ x ‖ * ‖ y ‖
simp_all h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 ⊢ ∀ ( x y : E ), | ⟪ x , y ⟫ | ≤ d * ‖ x ‖ * ‖ y ‖
intro x y h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E ⊢ | ⟪ x , y ⟫ | ≤ d * ‖ x ‖ * ‖ y ‖
trans | ‖ x ‖₂ | * | ‖ y ‖₂ | E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E ⊢ | ⟪ x , y ⟫ | ≤ | ‖ x ‖₂ | * | ‖ y ‖₂ | E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
· E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E ⊢ | ⟪ x , y ⟫ | ≤ | ‖ x ‖₂ | * | ‖ y ‖₂ | refine ( norm_inner_le_norm ( 𝕜 := ℝ ) ( E := WithLp 2 E ) ( WithLp.toLp 2 x )
( WithLp.toLp 2 y ) ) . trans ? _ E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E ⊢ ‖ WithLp.toLp 2 x ‖ * ‖ WithLp.toLp 2 y ‖ ≤ | ‖ x ‖₂ | * | ‖ y ‖₂ |
simp [ norm_withLp2_eq_norm2 ] All goals completed! 🐙
· E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖ have key ( z : E ) : | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ := by E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E ⊢ ∃ C > 0 , ∀ ( x y : E ), ‖ ⟪ ( x , y ) .1 , ( x , y ) .2 ⟫ ‖ ≤ C * ‖ x ‖ * ‖ y ‖ E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
apply le_of_sq_le_sq h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ | ‖ z ‖₂ | ^ 2 ≤ ( √ d * ‖ z ‖ ) ^ 2 hb E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ 0 ≤ √ d * ‖ z ‖ E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
· h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ | ‖ z ‖₂ | ^ 2 ≤ ( √ d * ‖ z ‖ ) ^ 2 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖ simp [ @ mul_pow ] h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ ‖ z ‖₂ ^ 2 ≤ √ d ^ 2 * ‖ z ‖ ^ 2 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
rw [ norm₂_sq_eq_re_inner ( 𝕜 := ℝ ) h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ re ⟪ z , z ⟫ ≤ √ d ^ 2 * ‖ z ‖ ^ 2 h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ re ⟪ z , z ⟫ ≤ √ d ^ 2 * ‖ z ‖ ^ 2 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖ ] h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ re ⟪ z , z ⟫ ≤ √ d ^ 2 * ‖ z ‖ ^ 2 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
simp only [ re_to_real ] h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ ⟪ z , z ⟫ ≤ √ d ^ 2 * ‖ z ‖ ^ 2 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
rw [ Real.sq_sqrt ( by E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ 0 ≤ d h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ ⟪ z , z ⟫ ≤ d * ‖ z ‖ ^ 2 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖ linarith All goals completed! 🐙 h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ ⟪ z , z ⟫ ≤ d * ‖ z ‖ ^ 2 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖ : ( 0 : ℝ ) ≤ d ) ] h E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ ⟪ z , z ⟫ ≤ d * ‖ z ‖ ^ 2 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
exact ( h z ) . 2 All goals completed! 🐙 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
· hb E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E z : E ⊢ 0 ≤ √ d * ‖ z ‖ E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖ positivity E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖ E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
have h1 := key x E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
have h2 := key y E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ d * ‖ x ‖ * ‖ y ‖
trans ( √ d * ‖ x ‖ ) * ( √ d * ‖ y ‖ ) E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ √ d * ‖ x ‖ * ( √ d * ‖ y ‖ ) E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ √ d * ‖ x ‖ * ( √ d * ‖ y ‖ ) ≤ d * ‖ x ‖ * ‖ y ‖
· E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ | ‖ x ‖₂ | * | ‖ y ‖₂ | ≤ √ d * ‖ x ‖ * ( √ d * ‖ y ‖ ) exact mul_le_mul_of_nonneg h1 h2 ( by E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ 0 ≤ | ‖ x ‖₂ | positivity All goals completed! 🐙 ) ( by E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ 0 ≤ √ d * ‖ y ‖ positivity All goals completed! 🐙 )
· E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ √ d * ‖ x ‖ * ( √ d * ‖ y ‖ ) ≤ d * ‖ x ‖ * ‖ y ‖ apply le_of_eq E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ √ d * ‖ x ‖ * ( √ d * ‖ y ‖ ) = d * ‖ x ‖ * ‖ y ‖
rw [ mul_mul_mul_comm , E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ √ d * √ d * ( ‖ x ‖ * ‖ y ‖ ) = d * ‖ x ‖ * ‖ y ‖ E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ d * ( ‖ x ‖ * ‖ y ‖ ) = d * ‖ x ‖ * ‖ y ‖ Real.mul_self_sqrt ( by E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ 0 ≤ d E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ d * ( ‖ x ‖ * ‖ y ‖ ) = d * ‖ x ‖ * ‖ y ‖ linarith All goals completed! 🐙 E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ d * ( ‖ x ‖ * ‖ y ‖ ) = d * ‖ x ‖ * ‖ y ‖ : ( 0 : ℝ ) ≤ d ) ] E : Type u_5 inst✝¹ : NormedAddCommGroup E inst✝ : NormedSpace ℝ E hE : InnerProductSpace' ℝ E c : ℝ d : ℝ hc : 0 < c hd : 0 < d h : ∀ ( x : E ), c * ‖ x ‖ ^ 2 ≤ ⟪ x , x ⟫ ∧ ⟪ x , x ⟫ ≤ d * ‖ x ‖ ^ 2 x : E y : E key : ∀ ( z : E ), | ‖ z ‖₂ | ≤ √ d * ‖ z ‖ h1 : | ‖ x ‖₂ | ≤ √ d * ‖ x ‖ h2 : | ‖ y ‖₂ | ≤ √ d * ‖ y ‖ ⊢ d * ( ‖ x ‖ * ‖ y ‖ ) = d * ‖ x ‖ * ‖ y ‖
ring All goals completed! 🐙