Documentation

MIPRE.Background.Repetition.CommutingRepetition.VN.MonotoneLimit

Pointwise limits of uniformly bounded sequences #

source
noncomputable def CommutingRepetition.StrongLimit.pointwiseLimit {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (C : ℝ) (hC : βˆ€ (n : β„•), β€–T nβ€– ≀ C) (hex : βˆ€ (ΞΎ : 𝓗), βˆƒ (l : 𝓗), Filter.Tendsto (fun (n : β„•) => (T n) ΞΎ) Filter.atTop (nhds l)) :
𝓗 β†’L[β„‚] 𝓗

The pointwise limit of a uniformly bounded, pointwise convergent sequence.

Equations
Instances For
    source
    theorem CommutingRepetition.StrongLimit.pointwiseLimit_tendsto {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (C : ℝ) (hC : βˆ€ (n : β„•), β€–T nβ€– ≀ C) (hex : βˆ€ (ΞΎ : 𝓗), βˆƒ (l : 𝓗), Filter.Tendsto (fun (n : β„•) => (T n) ΞΎ) Filter.atTop (nhds l)) (ΞΎ : 𝓗) :
    Filter.Tendsto (fun (n : β„•) => (T n) ΞΎ) Filter.atTop (nhds ((pointwiseLimit T C hC hex) ΞΎ))

    Positive contractions #

    source
    theorem CommutingRepetition.StrongLimit.re_inner_apply_le {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] {T : 𝓗 β†’L[β„‚] 𝓗} (h0 : 0 ≀ T) (h1 : T ≀ 1) (ΞΎ : 𝓗) :
    β€–T ΞΎβ€– ^ 2 ≀ (inner β„‚ ΞΎ (T ΞΎ)).re
    source
    theorem CommutingRepetition.StrongLimit.norm_le_one_of_nonneg_le_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] {T : 𝓗 β†’L[β„‚] 𝓗} (h0 : 0 ≀ T) (h1 : T ≀ 1) :
    β€–Tβ€– ≀ 1

    Monotone sequences #

    source
    theorem CommutingRepetition.StrongLimit.nonneg_of_monotone {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) (n : β„•) :
    0 ≀ T n
    source
    theorem CommutingRepetition.StrongLimit.tendsto_re_inner {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) (ΞΎ : 𝓗) :
    βˆƒ (a : ℝ), Filter.Tendsto (fun (n : β„•) => (inner β„‚ ΞΎ ((T n) ΞΎ)).re) Filter.atTop (nhds a)

    The quadratic forms βŸͺΞΎ, Tβ‚™ ξ⟫ converge.

    source
    theorem CommutingRepetition.StrongLimit.cauchySeq_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) (ΞΎ : 𝓗) :
    CauchySeq fun (n : β„•) => (T n) ΞΎ

    Cauchy property of the orbit Tβ‚™ ΞΎ.

    source
    theorem CommutingRepetition.StrongLimit.exists_tendsto_apply {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) (ΞΎ : 𝓗) :
    βˆƒ (l : 𝓗), Filter.Tendsto (fun (n : β„•) => (T n) ΞΎ) Filter.atTop (nhds l)
    source
    noncomputable def CommutingRepetition.StrongLimit.monotoneLimit {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) :
    𝓗 β†’L[β„‚] 𝓗

    The strong limit of a monotone sequence of positive contractions.

    Equations
    Instances For
      source
      theorem CommutingRepetition.StrongLimit.monotoneLimit_tendsto {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) (ΞΎ : 𝓗) :
      Filter.Tendsto (fun (n : β„•) => (T n) ΞΎ) Filter.atTop (nhds ((monotoneLimit T hmono h0 h1) ΞΎ))
      source
      theorem CommutingRepetition.StrongLimit.monotoneLimit_inner {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) (ΞΎ Ξ· : 𝓗) :
      Filter.Tendsto (fun (n : β„•) => inner β„‚ ΞΎ ((T n) Ξ·)) Filter.atTop (nhds (inner β„‚ ΞΎ ((monotoneLimit T hmono h0 h1) Ξ·)))
      source
      theorem CommutingRepetition.StrongLimit.monotoneLimit_isSelfAdjoint {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) :
      IsSelfAdjoint (monotoneLimit T hmono h0 h1)
      source
      theorem CommutingRepetition.StrongLimit.le_monotoneLimit {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) (n : β„•) :
      T n ≀ monotoneLimit T hmono h0 h1
      source
      theorem CommutingRepetition.StrongLimit.monotoneLimit_nonneg {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) :
      0 ≀ monotoneLimit T hmono h0 h1
      source
      theorem CommutingRepetition.StrongLimit.monotoneLimit_le_one {𝓗 : Type u_1} [NormedAddCommGroup 𝓗] [InnerProductSpace β„‚ 𝓗] [CompleteSpace 𝓗] (T : β„• β†’ 𝓗 β†’L[β„‚] 𝓗) (hmono : Monotone T) (h0 : 0 ≀ T 0) (h1 : βˆ€ (n : β„•), T n ≀ 1) :
      monotoneLimit T hmono h0 h1 ≀ 1