Wrapper（B(ℋ)）

このファイルは LownerHeinzCore の結果を、L ℋ := ℋ →L[ℂ] ℋ（有界線形作用素）に 特殊化して再公開する薄い wrapper です。

• 証明は simpa using による Core の特殊化のみ（重複証明は書かない）
• B(ℋ) 側では既存の Loewner order の ecosystem を尊重し、spectralOrder は導入しません （spectralOrder が必要な場合は LownerHeinzCore.Spectral を利用）

@[reducible, inline]

abbrev LownerHeinzTheorem.L (ℋ : Type u) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] : Type u

Equations

• LownerHeinzTheorem.L ℋ = (ℋ →L[ℂ] ℋ)

instance LownerHeinzTheorem.instNontrivialL {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [Nontrivial ℋ] : Nontrivial (L ℋ)

theorem LownerHeinzTheorem.instNonnegSpectrumClassRealL {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : NonnegSpectrumClass ℝ (L ℋ)

instance LownerHeinzTheorem.instCFCRealSelfAdjoint {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : ContinuousFunctionalCalculus ℝ (L ℋ) IsSelfAdjoint

@[reducible, inline]

noncomputable abbrev LownerHeinzTheorem.cfcR {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (f : ℝ → ℝ) (A : L ℋ) : L ℋ

Equations

• LownerHeinzTheorem.cfcR f A = LownerHeinzCore.cfcR f A

def LownerHeinzTheorem.OperatorMonotone {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (f : ℝ → ℝ) : Prop

Fixed-space operator monotonicity on the Hilbert space ℋ.

Equations

• LownerHeinzTheorem.OperatorMonotone f = LownerHeinzCore.OperatorMonotone f

def LownerHeinzTheorem.OperatorMonotoneOn {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (s : Set ℝ) (f : ℝ → ℝ) : Prop

Fixed-space operator monotonicity on s for the Hilbert space ℋ.

Equations

• LownerHeinzTheorem.OperatorMonotoneOn s f = LownerHeinzCore.OperatorMonotoneOn s f

def LownerHeinzTheorem.OperatorAntitone {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (f : ℝ → ℝ) : Prop

Fixed-space operator antitonicity on the Hilbert space ℋ.

Equations

• LownerHeinzTheorem.OperatorAntitone f = LownerHeinzCore.OperatorAntitone f

def LownerHeinzTheorem.OperatorAntitoneOn {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (s : Set ℝ) (f : ℝ → ℝ) : Prop

Fixed-space operator antitonicity on s for the Hilbert space ℋ.

Equations

• LownerHeinzTheorem.OperatorAntitoneOn s f = LownerHeinzCore.OperatorAntitoneOn s f

def LownerHeinzTheorem.OperatorConvex {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (f : ℝ → ℝ) : Prop

Fixed-space operator convexity on the Hilbert space ℋ.

Equations

• LownerHeinzTheorem.OperatorConvex f = LownerHeinzCore.OperatorConvex f

def LownerHeinzTheorem.OperatorConvexOn {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (s : Set ℝ) (f : ℝ → ℝ) : Prop

Fixed-space operator convexity on s for the Hilbert space ℋ.

Equations

• LownerHeinzTheorem.OperatorConvexOn s f = LownerHeinzCore.OperatorConvexOn s f

def LownerHeinzTheorem.OperatorConcave {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (f : ℝ → ℝ) : Prop

Fixed-space operator concavity on the Hilbert space ℋ.

Equations

• LownerHeinzTheorem.OperatorConcave f = LownerHeinzCore.OperatorConcave f

def LownerHeinzTheorem.OperatorConcaveOn {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (s : Set ℝ) (f : ℝ → ℝ) : Prop

Fixed-space operator concavity on s for the Hilbert space ℋ.

Equations

• LownerHeinzTheorem.OperatorConcaveOn s f = LownerHeinzCore.OperatorConcaveOn s f

def LownerHeinzTheorem.OperatorMonotoneAll (f : ℝ → ℝ) : Prop

Uniform operator monotonicity over all Hilbert spaces in universe u.

Equations

• One or more equations did not get rendered due to their size.

def LownerHeinzTheorem.OperatorMonotoneOnAll (s : Set ℝ) (f : ℝ → ℝ) : Prop

Uniform operator monotonicity on s over all Hilbert spaces in universe u.

Equations

• One or more equations did not get rendered due to their size.

def LownerHeinzTheorem.OperatorAntitoneAll (f : ℝ → ℝ) : Prop

Uniform operator antitonicity over all Hilbert spaces in universe u.

Equations

• One or more equations did not get rendered due to their size.

def LownerHeinzTheorem.OperatorAntitoneOnAll (s : Set ℝ) (f : ℝ → ℝ) : Prop

Uniform operator antitonicity on s over all Hilbert spaces in universe u.

Equations

• One or more equations did not get rendered due to their size.

def LownerHeinzTheorem.OperatorConvexAll (f : ℝ → ℝ) : Prop

Uniform operator convexity over all Hilbert spaces in universe u.

Equations

• One or more equations did not get rendered due to their size.

def LownerHeinzTheorem.OperatorConvexOnAll (s : Set ℝ) (f : ℝ → ℝ) : Prop

Uniform operator convexity on s over all Hilbert spaces in universe u.

Equations

• One or more equations did not get rendered due to their size.

def LownerHeinzTheorem.OperatorConcaveAll (f : ℝ → ℝ) : Prop

Uniform operator concavity over all Hilbert spaces in universe u.

Equations

• One or more equations did not get rendered due to their size.

def LownerHeinzTheorem.OperatorConcaveOnAll (s : Set ℝ) (f : ℝ → ℝ) : Prop

Uniform operator concavity on s over all Hilbert spaces in universe u.

Equations

• One or more equations did not get rendered due to their size.

theorem LownerHeinzTheorem.operatorConvex_convexOn_univ {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f : ℝ → ℝ} (hf : OperatorConvex f) : ConvexOn ℝ Set.univ f

theorem LownerHeinzTheorem.operatorConvex_continuousOn_univ {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f : ℝ → ℝ} (hf : OperatorConvex f) : ContinuousOn f Set.univ

theorem LownerHeinzTheorem.operatorConvex_continuousOn_spectrum_union {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] {f : ℝ → ℝ} (hf : OperatorConvex f) (A B : L ℋ) : ContinuousOn f (spectrum ℝ A ∪ spectrum ℝ B)

theorem LownerHeinzTheorem.one_div_operatorAntitoneOn_Ioi {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : OperatorAntitoneOn (Set.Ioi 0) fun (x : ℝ) => 1 / x

theorem LownerHeinzTheorem.one_div_operatorConvexOn_Ioi {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] : OperatorConvexOn (Set.Ioi 0) fun (x : ℝ) => 1 / x

theorem LownerHeinzTheorem.one_div_add_t_operatorAntitoneOn_Ici {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (t : ℝ) : 0 < t → OperatorAntitoneOn (Set.Ici 0) fun (x : ℝ) => 1 / (x + t)

theorem LownerHeinzTheorem.one_div_add_t_operatorConvexOn_Ici {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] (t : ℝ) : 0 < t → OperatorConvexOn (Set.Ici 0) fun (x : ℝ) => 1 / (x + t)

theorem LownerHeinzTheorem.ratio_add_t_operatorMonotoneOn_Ici {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (t : ℝ) : 0 < t → OperatorMonotoneOn (Set.Ici 0) fun (x : ℝ) => x / (x + t)

theorem LownerHeinzTheorem.ratio_add_t_operatorConcaveOn_Ici {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] (t : ℝ) : 0 < t → OperatorConcaveOn (Set.Ici 0) fun (x : ℝ) => x / (x + t)

theorem LownerHeinzTheorem.power_Icc_zero_one_operatorMonotoneOn_Ici {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (p : ℝ) : p ∈ Set.Icc 0 1 → OperatorMonotoneOn (Set.Ici 0) fun (x : ℝ) => x ^ p

theorem LownerHeinzTheorem.power_Icc_zero_one_operatorConcaveOn_Ici {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] (p : ℝ) : p ∈ Set.Icc 0 1 → OperatorConcaveOn (Set.Ici 0) fun (x : ℝ) => x ^ p

theorem LownerHeinzTheorem.power_Icc_one_two_operatorConvexOn_Ici {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] (p : ℝ) : p ∈ Set.Icc 1 2 → OperatorConvexOn (Set.Ici 0) fun (x : ℝ) => x ^ p

theorem LownerHeinzTheorem.power_Icc_neg_one_zero_neg_operatorMonotoneOn_Ioi {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] (p : ℝ) : p ∈ Set.Icc (-1) 0 → OperatorMonotoneOn (Set.Ioi 0) fun (x : ℝ) => -x ^ p

theorem LownerHeinzTheorem.power_Icc_neg_one_zero_neg_operatorConcaveOn_Ioi {ℋ : Type u} [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] [Nontrivial ℋ] (p : ℝ) : p ∈ Set.Icc (-1) 0 → OperatorConcaveOn (Set.Ioi 0) fun (x : ℝ) => -x ^ p