Fredholm analysis of canonical graph operators #

This file combines strict singularity, block extraction, and compact-factorization arguments to establish the main Fredholm results for canonical operators on the Kalton--Peck space.

source

theorem KaltonPeck.Support.GraphFredholm.hasInfiniteDimensionalCompactRestriction_of_infiniteDimensional_kernel {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] (T : X →L[ℝ ] Y) (hker : ¬FiniteDimensional ℝ ↥(↑T).ker) :

HasInfiniteDimensionalCompactRestriction T

An operator with infinite-dimensional kernel has an infinite-dimensional compact restriction. Blueprint label: lem:infinite-kernel-compact-restriction.

source

theorem KaltonPeck.Support.GraphFredholm.exists_summableApproximateKernelSequence_of_finiteDimensional_ker {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] (T : X →L[ℝ ] Y) (hkerT : FiniteDimensional ℝ ↥(↑T).ker) (hrangeT : ¬IsClosed ↑(↑T).range) :

∃ (Z : Submodule ℝ X), IsClosed ↑Z ∧ Submodule.IsTopCompl (↑T).ker Z ∧ ¬FiniteDimensional ℝ ↥Z ∧ ∃ (z : ℕ → ↥Z), (∀ (n : ℕ), ‖z n‖ = 1) ∧ Summable fun (n : ℕ) => ‖(T ∘SL Z.subtypeL) (z n)‖

If an operator has finite-dimensional kernel and nonclosed range, then on a closed infinite-dimensional complement of its kernel it admits a normalized approximate-kernel sequence whose image norms are summable. Blueprint label: lem:nonclosed-range-approximate-kernel.

source

theorem KaltonPeck.Support.GraphFredholm.compactRestriction_or_summableApproximateKernelSequence {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] [CompleteSpace Y] (T : X →L[ℝ ] Y) (hT : ¬IsUpperSemiFredholm T) :

HasInfiniteDimensionalCompactRestriction T ∨ ∃ (Z : Submodule ℝ X), IsClosed ↑Z ∧ Submodule.IsTopCompl (↑T).ker Z ∧ ¬FiniteDimensional ℝ ↥Z ∧ ∃ (z : ℕ → ↥Z), (∀ (n : ℕ), ‖z n‖ = 1) ∧ Summable fun (n : ℕ) => ‖(T ∘SL Z.subtypeL) (z n)‖

Failure of upper semi-Fredholmness yields either an infinite-dimensional compact restriction or a summable normalized approximate-kernel sequence on a closed kernel complement. Blueprint label: lem:not-upper-semi-dichotomy.

source

def KaltonPeck.Support.GraphFredholm.HasBoundedCentralizerLift {Z : Type u_1} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (Q : Z →L[ℝ ] ↥Coordinates.CanonicalL2) :

Prop

A linear lift of Q whose error from the Kalton--Peck centralizer is square-summable and uniformly bounded. Blueprint label: def:bounded-centralizer-lift.

Equations

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

Instances For

source

def KaltonPeck.Support.GraphFredholm.HasBoundedCentralizerApproximation (M : Submodule ℝ ↥Coordinates.CanonicalL2) :

Prop

A bounded linear approximation to the Kalton--Peck centralizer on a Hilbert subspace. Blueprint label: def:bounded-centralizer-approximation.

Equations

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

Instances For

source

theorem KaltonPeck.Support.GraphFredholm.hasBoundedCentralizerLift_canonicalL2Quotient_comp {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] (S : Z →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) :

HasBoundedCentralizerLift (Coordinates.canonicalL2Quotient ∘SL S)

Every bounded operator into the canonical Kalton--Peck model supplies a bounded centralizer lift of its second-coordinate map. Blueprint label: lem:canonical-centralizer-lift.

source

theorem KaltonPeck.Support.GraphFredholm.no_boundedCentralizerLift_of_subspace_obstruction (hSubspace : ∀ (M : Submodule ℝ ↥Coordinates.CanonicalL2), IsClosed ↑M → ¬FiniteDimensional ℝ ↥M → ¬HasBoundedCentralizerApproximation M) {Z : Type u} [NormedAddCommGroup Z] [NormedSpace ℝ Z] [CompleteSpace Z] (hZ : ¬FiniteDimensional ℝ Z) (Q : Z →L[ℝ ] ↥Coordinates.CanonicalL2) (hQ : ∃ (K : NNReal), AntilipschitzWith K ⇑Q) :

¬HasBoundedCentralizerLift Q

A bounded-below map with a bounded centralizer lift produces a bounded approximation on its closed infinite-dimensional Hilbert range. Blueprint label: lem:centralizer-lift-to-subspace.

source

theorem KaltonPeck.Support.GraphFredholm.canonicalL2Quotient_strictlySingular_of_centralizer_obstruction (hKP : ∀ (Z : Type u) [inst : NormedAddCommGroup Z] [inst_1 : NormedSpace ℝ Z] [CompleteSpace Z], ¬FiniteDimensional ℝ Z → ∀ (Q : Z →L[ℝ ] ↥Coordinates.CanonicalL2), (∃ (K : NNReal), AntilipschitzWith K ⇑Q) → ¬HasBoundedCentralizerLift Q) :

StrictlySingular.IsStrictlySingular Coordinates.canonicalL2Quotient

Strict singularity of the canonical quotient reduces to the analytic Kalton--Peck centralizer obstruction. Blueprint label: lem:canonical-quotient-strictly-singular-reduction.

source

theorem KaltonPeck.Support.GraphFredholm.canonicalL2Quotient_strictlySingular_of_subspace_obstruction (hSubspace : ∀ (M : Submodule ℝ ↥Coordinates.CanonicalL2), IsClosed ↑M → ¬FiniteDimensional ℝ ↥M → ¬HasBoundedCentralizerApproximation M) :

StrictlySingular.IsStrictlySingular Coordinates.canonicalL2Quotient

The canonical quotient is strictly singular once the centralizer obstruction is known on every closed infinite-dimensional Hilbert subspace. Blueprint label: lem:canonical-quotient-strictly-singular-reduction.

source

theorem KaltonPeck.Support.GraphFredholm.no_boundedCentralizerApproximation (M : Submodule ℝ ↥Coordinates.CanonicalL2) (_hMclosed : IsClosed ↑M) (hM : ¬FiniteDimensional ℝ ↥M) :

¬HasBoundedCentralizerApproximation M

No infinite-dimensional Hilbert subspace admits a uniformly bounded linear approximation to the Kalton--Peck centralizer.

The proof is the direct p = 2 logarithmic obstruction: a gliding-hump sequence gives bounded signed block averages, while the corresponding second-coordinate vectors have quasi-norm log N + 1. Blueprint label: thm:canonical-centralizer-obstruction.

source

theorem KaltonPeck.Support.GraphFredholm.canonicalL2Quotient_isStrictlySingular :

StrictlySingular.IsStrictlySingular Coordinates.canonicalL2Quotient

The canonical quotient Z₂ → ℓ₂ is strictly singular. Blueprint label: thm:canonical-centralizer-obstruction.

source

theorem KaltonPeck.Support.GraphFredholm.canonical_isStrictlySingular_of_inclusion (T : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) (hTi : StrictlySingular.IsStrictlySingular (T ∘SL Symplectic.canonicalL2Inclusion)) :

StrictlySingular.IsStrictlySingular T

CGP Proposition 5.3(b): strict singularity on the canonical Hilbert kernel forces strict singularity on the whole canonical Kalton--Peck space.

source

theorem KaltonPeck.Support.GraphFredholm.canonical_not_upperSemi_comp_canonicalL2Inclusion_of_not_upper (B : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) (hB : ¬IsUpperSemiFredholm B) :

¬IsUpperSemiFredholm (B ∘SL Symplectic.canonicalL2Inclusion)

Corrected CGP Proposition 5.3(c), in contrapositive form: failure of upper semi-Fredholmness persists on the canonical Hilbert kernel.

source

theorem KaltonPeck.Support.GraphFredholm.canonical_factor_through_quotient (R : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) (hR : R ∘SL Symplectic.canonicalL2Inclusion = 0) :

∃ (L : ↥Coordinates.CanonicalL2 →L[ℝ ] Coordinates.CanonicalRealKaltonPeck), R = L ∘SL Coordinates.canonicalL2Quotient

Every bounded operator vanishing on the canonical kernel factors continuously through the canonical quotient.

source

theorem KaltonPeck.Support.GraphFredholm.canonical_symplecticAdjoint_range_le_quotientKernel (R : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) (hR : R ∘SL Symplectic.canonicalL2Inclusion = 0) :

(↑(Symplectic.canonicalKaltonSwansonForm.adjoint R)).range ≤ (↑Coordinates.canonicalL2Quotient).ker

If a canonical operator vanishes on the canonical kernel, then the range of its symplectic adjoint lies in that kernel.

source

theorem KaltonPeck.Support.GraphFredholm.canonical_symplecticAdjoint_factor_through_inclusion (R : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) (hR : R ∘SL Symplectic.canonicalL2Inclusion = 0) :

∃ (L : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] ↥Coordinates.CanonicalL2), Symplectic.canonicalKaltonSwansonForm.adjoint R = Symplectic.canonicalL2Inclusion ∘SL L

If a canonical operator vanishes on the canonical kernel, then its symplectic adjoint factors continuously through the inclusion of that kernel.

source

The adjoint cross-term of a quotient-factorized remainder and a kernel-intertwining operator is the included Hilbert adjoint of its quotient compression.

source

theorem KaltonPeck.Support.GraphFredholm.canonical_symplecticAdjoint_kernelCompression (T : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) :

Coordinates.canonicalL2Quotient ∘SL Symplectic.canonicalKaltonSwansonForm.adjoint T ∘SL Symplectic.canonicalL2Inclusion = -ContinuousLinearMap.adjoint (Coordinates.canonicalL2Quotient ∘SL T ∘SL Symplectic.canonicalL2Inclusion)

Compression of the symplectic adjoint to the canonical kernel and quotient is the negative Hilbert-space adjoint of the corresponding compression.

source

theorem KaltonPeck.Support.GraphFredholm.canonical_quotient_operator_inclusion_isStrictlySingular (T : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) :

StrictlySingular.IsStrictlySingular (Coordinates.canonicalL2Quotient ∘SL T ∘SL Symplectic.canonicalL2Inclusion)

Every kernel-to-quotient compression of a canonical operator is strictly singular.

source

theorem KaltonPeck.Support.GraphFredholm.canonical_quotient_symplecticAdjoint_inclusion_isStrictlySingular (T : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) :

StrictlySingular.IsStrictlySingular (Coordinates.canonicalL2Quotient ∘SL Symplectic.canonicalKaltonSwansonForm.adjoint T ∘SL Symplectic.canonicalL2Inclusion)

The kernel-to-quotient compression of a canonical symplectic adjoint is strictly singular.

source

theorem KaltonPeck.Support.GraphFredholm.canonicalBlockOperator_isUpperSemiFredholm (w : ℕ → ℕ → ℝ) (hw : Symplectic.IsSuccessiveNormalizedBlockSequence w) :

IsUpperSemiFredholm (Symplectic.canonicalBlockOperator w hw)

Every canonical normalized block operator is upper semi-Fredholm. Blueprint label: lem:cgp-primary-reduction.

source

def KaltonPeck.Support.GraphFredholm.HasUpperCompactGramFactorization :

Prop

The exact retained output of the upper-specific Kalton block factorization needed by the compact-Gram proof.

Equations

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

Instances For

source

theorem KaltonPeck.Support.GraphFredholm.canonical_pairing_inclusion_secondBasis (x : ↥Coordinates.CanonicalL2) (k : ℕ) :

(Symplectic.canonicalKaltonSwansonForm.toDual (Symplectic.canonicalL2Inclusion x)) (Symplectic.canonicalSecondBasisVector k) = ↑x k

Pairing a canonical kernel vector with the kth quotient-basis vector evaluates its kth Hilbert coordinate.

source

theorem KaltonPeck.Support.GraphFredholm.tendsto_canonical_pairing_apply_block_zero (A : ↥Coordinates.CanonicalL2 →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) (w : ℕ → ℕ → ℝ) (hw : Symplectic.IsSuccessiveNormalizedBlockSequence w) (z : Coordinates.CanonicalRealKaltonPeck) :

Filter.Tendsto (fun (n : ℕ) => (Symplectic.canonicalKaltonSwansonForm.toDual (A ((Symplectic.canonicalL2BlockEmbedding w hw) (lp.single 2 n 1)))) z) Filter.atTop (nhds 0)

Applying a fixed canonical symplectic functional after a bounded operator to successive normalized Hilbert blocks tends to zero.

source

def KaltonPeck.Support.GraphFredholm.HasUpperSummableKernelBlockApproximation :

Prop

The sequence-selection output needed from the upper-specific Kalton block argument: after passing to canonical normalized source and target blocks, the kernel-column error is absolutely summable.

Equations

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

Instances For

source

theorem KaltonPeck.Support.GraphFredholm.hasUpperSummableKernelBlockApproximation :

HasUpperSummableKernelBlockApproximation

Every upper semi-Fredholm canonical operator admits an absolutely summable kernel-column approximation between normalized successive source and target blocks.

source

theorem KaltonPeck.Support.GraphFredholm.hasUpperCompactGramFactorization_of_summableKernelBlockApproximation (hBlock : HasUpperSummableKernelBlockApproximation) :

HasUpperCompactGramFactorization

An absolutely summable canonical kernel-block approximation supplies exactly the retained upper factorization used by the compact-Gram contradiction.

source

theorem KaltonPeck.Support.GraphFredholm.upperSemi_gramKernel_not_compact_of_factorization (hFactor : HasUpperCompactGramFactorization) (T : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) (hT : IsUpperSemiFredholm T) :

¬IsCompactOperator ⇑((Symplectic.canonicalKaltonSwansonForm.adjoint T * T) ∘SL Symplectic.canonicalL2Inclusion)

The retained-output block factorization forces the Gram restriction of every upper semi-Fredholm operator to be noncompact.

source

IsUpperSemiFredholm (Symplectic.canonicalKaltonSwansonForm.adjoint A * A)

The formal operator-theoretic reduction in CGP Lemma 5.4. Its three hypotheses are precisely Proposition 5.3(c), Proposition 5.3(b), and Proposition 5.3(a), respectively. Blueprint label: lem:cgp-primary-reduction.

source

A target-specific CGP reduction which avoids the global strictly-singular Proposition 5.3 calculus. It needs only the upper-semi restriction implication and noncompactness of the Gram restriction for upper semi-Fredholm operators. Blueprint label: lem:cgp-primary-reduction.

source

def KaltonPeck.Support.GraphFredholm.HasCanonicalKernelCompactBlockExtraction :

Prop

The target-minimal compact-block extraction statement: failure of upper semi-Fredholmness already produces a compact canonical Hilbert-kernel block.

Equations

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

Instances For

source

theorem KaltonPeck.Support.GraphFredholm.hasCanonicalKernelCompactBlockExtraction :

HasCanonicalKernelCompactBlockExtraction

The corrected compact perturbation argument in CGP Proposition 5.3(c), combined with canonical Hilbert block extraction, establishes the target-minimal compact-block premise.

source

The shortest formal CGP reduction: compact block extraction for a failed Gram operator and noncompactness of Gram restrictions for upper semi-Fredholm operators suffice.

source

theorem KaltonPeck.Support.GraphFredholm.canonicalGram_isUpperSemiFredholm_of_targetFactorizations (hExtract : HasCanonicalKernelCompactBlockExtraction) (hFactor : HasUpperCompactGramFactorization) (A : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) (hA : IsUpperSemiFredholm A) :

IsUpperSemiFredholm (Symplectic.canonicalKaltonSwansonForm.adjoint A * A)

The two retained target-specific source inputs imply the Gram upper-semi conclusion.

source

theorem KaltonPeck.Support.GraphFredholm.cgpPrimary (A : Coordinates.CanonicalRealKaltonPeck →L[ℝ ] Coordinates.CanonicalRealKaltonPeck) (hA : IsUpperSemiFredholm A) :

IsFredholm (Symplectic.canonicalKaltonSwansonForm.adjoint A * A)

The pinned canonical Castillo--González--Pino theorem (arXiv:2207.01069v1, Lemma 5.4). Blueprint label: thm:cgp-primary; audit ID EXT-CGP-UPPER-SEMI-PRIMARY.

source

theorem KaltonPeck.Support.GraphFredholm.cgpTransport {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (hX : RealKaltonPeckPresentation X) (A : X →L[ℝ ] X) (hA : IsUpperSemiFredholm A) :

IsFredholm ((Symplectic.transportedKaltonSwansonForm hX).adjoint A * A)

The CGP theorem transported to an arbitrary complete presented real Kalton--Peck model. Blueprint label: thm:cgp-transport; audit ID EXT-CGP-UPPER-SEMI.

source

def KaltonPeck.Support.GraphFredholm.evenBlockSequence :

ℕ → ℕ → ℝ

The normalized sequence n ↦ e₂ₙ. Support definition for blueprint label lem:even-odd-blocks.

Equations

KaltonPeck.Support.GraphFredholm.evenBlockSequence n = KaltonPeck.Support.Symplectic.standardBasisSequence (2 * n)

Instances For

source

def KaltonPeck.Support.GraphFredholm.oddBlockSequence :

ℕ → ℕ → ℝ

The normalized sequence n ↦ e₂ₙ₊₁. Support definition for blueprint label lem:even-odd-blocks.

Equations

KaltonPeck.Support.GraphFredholm.oddBlockSequence n = KaltonPeck.Support.Symplectic.standardBasisSequence (2 * n + 1)

Instances For

source

theorem KaltonPeck.Support.GraphFredholm.evenOddBlockSequences :

Symplectic.IsSuccessiveNormalizedBlockSequence evenBlockSequence ∧ Symplectic.IsSuccessiveNormalizedBlockSequence oddBlockSequence ∧ Symplectic.AreMutuallySupportDisjoint evenBlockSequence oddBlockSequence

The even and odd sequences are successive normalized blocks and mutually support-disjoint. Support theorem for blueprint label lem:even-odd-blocks.

source

noncomputable def KaltonPeck.Support.GraphFredholm.evenBlockEmbedding {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (hX : RealKaltonPeckPresentation X) :

X →L[ℝ ] X

The transported even-coordinate block embedding. Support definition for blueprint label lem:even-odd-blocks.

Equations

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

Instances For

source

noncomputable def KaltonPeck.Support.GraphFredholm.oddBlockEmbedding {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (hX : RealKaltonPeckPresentation X) :

X →L[ℝ ] X

The transported odd-coordinate block embedding. Support definition for blueprint label lem:even-odd-blocks.

Equations

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

Instances For

source

noncomputable def KaltonPeck.Support.GraphFredholm.graphBlockOperator {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (hX : RealKaltonPeckPresentation X) (T : X →L[ℝ ] X) :

X →L[ℝ ] X

The graph operator R₀ + R₁T on a presented model. Support definition for blueprint labels lem:even-odd-blocks and prop:graph-fredholm.

Equations

KaltonPeck.Support.GraphFredholm.graphBlockOperator hX T = KaltonPeck.Support.GraphFredholm.evenBlockEmbedding hX + KaltonPeck.Support.GraphFredholm.oddBlockEmbedding hX * T

Instances For

source

theorem KaltonPeck.Support.GraphFredholm.evenOddBlocks {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (hX : RealKaltonPeckPresentation X) :

have ω := Symplectic.transportedKaltonSwansonForm hX; have R₀ := evenBlockEmbedding hX; have R₁ := oddBlockEmbedding hX; ω.adjoint R₀ * R₀ = 1 ∧ ω.adjoint R₁ * R₁ = 1 ∧ ω.adjoint R₀ * R₁ = 0 ∧ ω.adjoint R₁ * R₀ = 0 ∧ ∀ (T : X →L[ℝ ] X), have W := graphBlockOperator hX T; ω.adjoint R₀ * W = 1 ∧ ω.adjoint W * W = 1 + ω.adjoint T * T ∧ IsUpperSemiFredholm W

The four even--odd adjoint relations and the two graph-operator identities. Blueprint label: lem:even-odd-blocks; audit IDs HID-EVEN-ODD-BLOCK-RELATIONS, HID-LEFT-INVERSE-UPPER-SEMI, and HID-ADJOINT-EXPANSION.

source

theorem KaltonPeck.Support.GraphFredholm.graphFredholm {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (hX : RealKaltonPeckPresentation X) (T : X →L[ℝ ] X) :

IsFredholm (1 + (Symplectic.transportedKaltonSwansonForm hX).adjoint T * T)

Every graph operator I + T⁺T on a complete presented real Kalton--Peck model is Fredholm. Blueprint label: prop:graph-fredholm; audit ID PROP-GRAPH-FREDHOLM.

source

noncomputable def KaltonPeck.Support.GraphFredholm.kaltonPeckAlternatingPath {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (hX : RealKaltonPeckPresentation X) (T : X →L[ℝ ] X) (t : ℝ) :

ContinuousAlternatingForm X

The weak alternating form bₜ(x,y) = Ω(x,y) + t Ω(Tx,Ty). Blueprint label: lem:kp-alternating-path; audit ID HID-ALTERNATING-PATH.

Equations

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

Instances For

source

theorem KaltonPeck.Support.GraphFredholm.kaltonPeckAlternatingPath_spec {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] (hX : RealKaltonPeckPresentation X) (T : X →L[ℝ ] X) :

have ω := Symplectic.transportedKaltonSwansonForm hX; (∀ (t : ℝ) (x y : X), ((kaltonPeckAlternatingPath hX T t).toDual x) y = (ω.toDual x) y + t * (ω.toDual (T x)) (T y)) ∧ (∀ (t : ℝ), (kaltonPeckAlternatingPath hX T t).toDual = ↑ω.toDual ∘SL (1 + t • (ω.adjoint T * T))) ∧ (Continuous fun (t : ↑(Set.Icc 0 1)) => (kaltonPeckAlternatingPath hX T ↑t).toDual) ∧ ∀ (t : ↑(Set.Icc 0 1)), IsFredholm (kaltonPeckAlternatingPath hX T ↑t).toDual

Evaluation, induced-operator formula, norm continuity, and Fredholmness of the path. Blueprint label: lem:kp-alternating-path; audit IDs HID-ALTERNATING-PATH, HID-SQRT-SCALING, and HID-D-COMPOSITION.

source

theorem KaltonPeck.Support.GraphFredholm.evenGraphKernel {X : Type u_1} [NormedAddCommGroup X] [NormedSpace ℝ X] [CompleteSpace X] (hX : RealKaltonPeckPresentation X) (T : X →L[ℝ ] X) :

have G := 1 + (Symplectic.transportedKaltonSwansonForm hX).adjoint T * T; IsFredholm G ∧ Even (nullity G)

The graph Fredholm operator has finite, even-dimensional kernel. Blueprint label: prop:even-kernel; audit ID PROP-EVEN-KERNEL.

Documentation

LeanPool.KaltonPeck.KaltonPeck.Support.GraphFredholm

Fredholm analysis of canonical graph operators #