def RCLike.Components {𝕂 : Type u_1} [RCLike 𝕂] : Finset 𝕂

TODO: check whether this is the right approach

Equations

• RCLike.Components = {1, -1, RCLike.I, -RCLike.I}

theorem RCLike.Components.norm_eq_one {𝕂 : Type u_1} [RCLike 𝕂] {c : 𝕂} (hc : c ∈ Components) (hc' : c ≠ 0) : ‖c‖ = 1

theorem RCLike.Components.norm_le_one {𝕂 : Type u_1} [RCLike 𝕂] {c : 𝕂} (hc : c ∈ Components) : ‖c‖ ≤ 1

def RCLike.component {𝕂 : Type u_1} [RCLike 𝕂] (c a : 𝕂) : NNReal

TODO: check whether this is the right approach

Equations

• RCLike.component c a = (RCLike.re (a * (starRingEnd 𝕂) c)).toNNReal

theorem RCLike.component_le_norm {𝕂 : Type u_1} [RCLike 𝕂] {c a : 𝕂} (hc : c ∈ Components) : ↑(component c a) ≤ ‖a‖

theorem RCLike.component_le_nnnorm {𝕂 : Type u_1} [RCLike 𝕂] {c a : 𝕂} (hc : c ∈ Components) : component c a ≤ ‖a‖₊

theorem RCLike.decomposition {𝕂 : Type u_1} [RCLike 𝕂] {a : 𝕂} : 1 * (algebraMap ℝ 𝕂) ↑(component 1 a) + -1 * (algebraMap ℝ 𝕂) ↑(component (-1) a) + I * (algebraMap ℝ 𝕂) ↑(component I a) + -I * (algebraMap ℝ 𝕂) ↑(component (-I) a) = a

theorem RCLike.nnnorm_ofReal {𝕂 : Type u_1} [RCLike 𝕂] {a : NNReal} : a = ‖↑↑a‖₊

theorem RCLike.enorm_ofReal {𝕂 : Type u_1} [RCLike 𝕂] {a : NNReal} : ‖a‖ₑ = ‖↑↑a‖ₑ

Helper lemmas for the RCLike component decomposition norm bounds

theorem RCLike.induction {α : Type u_1} {𝕂 : Type u_2} [RCLike 𝕂] {β : Type u_3} [Mul β] {a b : β} {P : (α → 𝕂) → Prop} (P_add : ∀ {f g : α → 𝕂}, P f → P g → P (f + g)) (P_components : ∀ {f : α → 𝕂} {c : 𝕂}, c ∈ Components → P f → P (⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ component c ∘ f)) (P_mul_unit : ∀ {f : α → 𝕂} {c : 𝕂}, c ∈ Components → P f → P (c • f)) {motive : (α → 𝕂) → β → Prop} (motive_nnreal : ∀ {f : α → NNReal}, P (⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ f) → motive (⇑(algebraMap ℝ 𝕂) ∘ NNReal.toReal ∘ f) a) (motive_add' : ∀ {n : β} {f g : α → 𝕂}, (∀ {x : α}, ‖f x‖ ≤ ‖f x + g x‖) → (∀ {x : α}, ‖g x‖ ≤ ‖f x + g x‖) → P f → P g → motive f n → motive g n → motive (f + g) (n * b)) (motive_mul_unit : ∀ {f : α → 𝕂} {c : 𝕂} {n : β}, c ∈ Components → P f → motive f n → motive (c • f) n) ⦃f : α → 𝕂⦄ (hf : P f) : motive f (a * b * b)