Douglas factorization lemma

TheoremAdjoint preserves the operator norm#✓fully proved

Adjoints preserve operator norm.

theorem norm_adjoint (T : E →L[𝕜] F) : ‖T†‖ = ‖T‖

Used by 2

Used byDouglas' lemma: majorization gives a norm-bounded factor · Factorization implies majorization

TheoremInjectivity of an operator on the orthogonal complement of its kernel#✓fully proved

Two points of (ker B)ᗮ with the same image under B are equal, since their difference lies in ker B ∩ (ker B)ᗮ.

theorem eq_of_mem_orthogonal_and_apply {z₁ z₂ : E} (h₁ : z₁ ∈ B.kerᗮ)
    (h₂ : z₂ ∈ B.kerᗮ) (hB : B z₁ = B z₂) : z₁ = z₂

Used by 3

Used byContinuity of the Douglas factor via the closed graph theorem · Uniqueness of the Douglas factor · Douglas factor as a linear map

TheoremPreimages in the orthogonal complement of the kernel under range inclusion#✓fully proved

If A.range ≤ B.range, every A x has a preimage under B in (ker B)ᗮ.

theorem exists_mem_orthogonal_apply (h : A.range ≤ B.range) (x : E) :
    ∃ z : E, z ∈ B.kerᗮ ∧ B z = A x

Used by 2

Used byUnderlying function of the Douglas factor · Defining properties of the Douglas preimage

DefinitionUnderlying function of the Douglas factor#✓fully proved

The underlying function of the canonical factor: the chosen preimage of A x in (ker B)ᗮ.

noncomputable def douglasFactorFun (h : A.range ≤ B.range) (x : E) : E :=
  Classical.choose (exists_mem_orthogonal_apply A B h x)

Uses 1 · Used by 6

Statement usesPreimages in the orthogonal complement of the kernel under range inclusion

Used byDouglas factor gives a preimage under B · Continuity of the Douglas factor via the closed graph theorem · Uniqueness of the Douglas factor · Defining properties of the Douglas preimage · Douglas factor as a linear map · Douglas factor takes values in the kernel's orthogonal complement

TheoremDefining properties of the Douglas preimage#✓fully proved

The defining properties of the chosen preimage.

theorem douglasFactorFun_spec (h : A.range ≤ B.range) (x : E) :
    douglasFactorFun A B h x ∈ B.kerᗮ ∧ B (douglasFactorFun A B h x) = A x

Uses 2 · Used by 5

Statement usesUnderlying function of the Douglas factor

Proof usesPreimages in the orthogonal complement of the kernel under range inclusion

Used byDouglas factor gives a preimage under B · Continuity of the Douglas factor via the closed graph theorem · Uniqueness of the Douglas factor · Douglas factor as a linear map · Douglas factor takes values in the kernel's orthogonal complement

DefinitionDouglas factor as a linear map#✓fully proved

The canonical factor as a linear map.

MathlibExt.Analysis.InnerProductSpace.DouglasLemma.douglasFactorLin · 21 lines

noncomputable def douglasFactorLin (h : A.range ≤ B.range) : E →ₗ[𝕜] E where
  toFun := douglasFactorFun A B h
  map_add' x y := by
    apply eq_of_mem_orthogonal_and_apply B (douglasFactorFun_spec A B h (x + y)).1
    · exact B.kerᗮ.add_mem (douglasFactorFun_spec A B h x).1
        (douglasFactorFun_spec A B h y).1
    · calc B (douglasFactorFun A B h (x + y)) = A (x + y) :=
          (douglasFactorFun_spec A B h (x + y)).2
        _ = A x + A y := map_add _ _ _
        _ = B (douglasFactorFun A B h x) + B (douglasFactorFun A B h y) := by
          rw [← (douglasFactorFun_spec A B h x).2, ← (douglasFactorFun_spec A B h y).2]
        _ = B (douglasFactorFun A B h x + douglasFactorFun A B h y) := (map_add _ _ _).symm
  map_smul' c x := by
    apply eq_of_mem_orthogonal_and_apply B (douglasFactorFun_spec A B h (c • x)).1
    · exact B.kerᗮ.smul_mem c (douglasFactorFun_spec A B h x).1
    · calc B (douglasFactorFun A B h (c • x)) = A (c • x) :=
          (douglasFactorFun_spec A B h (c • x)).2
        _ = c • A x := map_smul _ _ _
        _ = c • B (douglasFactorFun A B h x) := by
          rw [← (douglasFactorFun_spec A B h x).2]
        _ = B (c • douglasFactorFun A B h x) := (map_smul _ _ _).symm

Uses 3 · Used by 2

Statement usesUnderlying function of the Douglas factor · Defining properties of the Douglas preimage · Injectivity of an operator on the orthogonal complement of its kernel

Used byContinuity of the Douglas factor via the closed graph theorem · Canonical factor in Douglas' lemma

TheoremContinuity of the Douglas factor via the closed graph theorem#✓fully proved

The canonical factor is continuous, by the (sequential) closed graph theorem: if u n → x and C (u n) → y, then y ∈ (ker B)ᗮ (the orthogonal complement is closed) and B y = A x (continuity of A and B), so y = C x by uniqueness of the preimage in (ker B)ᗮ.

theorem continuous_douglasFactorLin (h : A.range ≤ B.range) :
    Continuous (douglasFactorLin A B h)

Uses 4 · Used by 1

Statement usesDouglas factor as a linear map

Proof usesUnderlying function of the Douglas factor · Defining properties of the Douglas preimage · Injectivity of an operator on the orthogonal complement of its kernel

Used byCanonical factor in Douglas' lemma

DefinitionCanonical factor in Douglas' lemma#✓fully proved

The canonical factor in Douglas' lemma: for x : E, the unique element of (ker B)ᗮ mapped by B to A x.

noncomputable def douglasFactor (h : A.range ≤ B.range) : E →L[𝕜] E where
  toLinearMap := douglasFactorLin A B h
  cont := continuous_douglasFactorLin A B h

Uses 2 · Used by 5

Statement usesContinuity of the Douglas factor via the closed graph theorem · Douglas factor as a linear map

Used byDouglas factor gives a preimage under B · Uniqueness of the Douglas factor · Douglas factor takes values in the kernel's orthogonal complement · Douglas factor factors A through B · Douglas' lemma: range inclusion iff factorization

TheoremDouglas factor takes values in the kernel's orthogonal complement#✓fully proved

The canonical factor lands in (ker B)ᗮ.

theorem douglasFactor_mem_orthogonal (h : A.range ≤ B.range) (x : E) :
    douglasFactor A B h x ∈ B.kerᗮ

Uses 3

Statement usesCanonical factor in Douglas' lemma

Proof usesUnderlying function of the Douglas factor · Defining properties of the Douglas preimage

TheoremDouglas factor gives a preimage under B#✓fully proved

The canonical factor is a preimage: B (C x) = A x.

theorem apply_douglasFactor (h : A.range ≤ B.range) (x : E) :
    B (douglasFactor A B h x) = A x

Uses 3 · Used by 2

Statement usesCanonical factor in Douglas' lemma

Proof usesUnderlying function of the Douglas factor · Defining properties of the Douglas preimage

Used byUniqueness of the Douglas factor · Douglas factor factors A through B

TheoremDouglas factor factors A through B#✓fully proved

The canonical factor factors A through B.

theorem eq_comp_douglasFactor (h : A.range ≤ B.range) : A = B ∘L douglasFactor A B h

Uses 2 · Used by 1

Statement usesCanonical factor in Douglas' lemma

Proof usesDouglas factor gives a preimage under B

Used byDouglas' lemma: range inclusion iff factorization

TheoremUniqueness of the Douglas factor#✓fully proved

The canonical factor is the unique operator with the two defining properties.

theorem douglasFactor_eq_of_mem_orthogonal_and_apply {C : E →L[𝕜] E}
    (hC : ∀ x, C x ∈ B.kerᗮ ∧ B (C x) = A x) (h : A.range ≤ B.range) :
    C = douglasFactor A B h

Uses 5

Statement usesCanonical factor in Douglas' lemma

Proof usesDouglas factor gives a preimage under B · Underlying function of the Douglas factor · Defining properties of the Douglas preimage · Injectivity of an operator on the orthogonal complement of its kernel

TheoremDouglas' lemma: range inclusion iff factorization#✓fully proved

Douglas' lemma, range form: A.range ≤ B.range iff A = B ∘L C for some bounded C.

theorem range_le_iff_exists_factorization :
    A.range ≤ B.range ↔ ∃ C : E →L[𝕜] E, A = B ∘L C

Uses 2 · Used by 1

Proof usesCanonical factor in Douglas' lemma · Douglas factor factors A through B

Used byDouglas' lemma: range inclusion iff majorization

TheoremFactorization implies majorization#✓fully proved

If A = B ∘L C, then majorization holds with constant ‖C‖.

theorem majorization_of_factorization {C : E →L[𝕜] E} (hC : A = B ∘L C) (y : F) :
    ‖(A†) y‖ ≤ ‖C‖ * ‖(B†) y‖

Uses 1 · Used by 1

Proof usesAdjoint preserves the operator norm

Used byDouglas' lemma: majorization iff factorization

TheoremDouglas' lemma: majorization gives a norm-bounded factor#✓fully proved

Douglas' lemma, factorization form with a norm bound: majorization with constant c yields a factor C with A = B ∘L C and ‖C‖ ≤ c.

theorem exists_factorization_of_majorization {c : ℝ} (hc : 0 ≤ c)
    (hmaj : ∀ y : F, ‖(A†) y‖ ≤ c * ‖(B†) y‖) :
    ∃ C : E →L[𝕜] E, A = B ∘L C ∧ ‖C‖ ≤ c

Uses 1 · Used by 1

Proof usesAdjoint preserves the operator norm

Used byDouglas' lemma: majorization iff factorization

TheoremDouglas' lemma: majorization iff factorization#✓fully proved

Douglas' lemma, majorization form: majorization holds iff A factors through B.

theorem majorization_iff_exists_factorization :
    (∃ c : ℝ, 0 ≤ c ∧ ∀ y : F, ‖(A†) y‖ ≤ c * ‖(B†) y‖) ↔
      ∃ C : E →L[𝕜] E, A = B ∘L C

Uses 2 · Used by 1

Proof usesDouglas' lemma: majorization gives a norm-bounded factor · Factorization implies majorization

Used byDouglas' lemma: range inclusion iff majorization

TheoremDouglas' lemma: range inclusion iff majorization#✓fully proved

Douglas' lemma, range/majorization form: A.range ≤ B.range iff majorization holds.

theorem range_le_iff_majorization :
    A.range ≤ B.range ↔ ∃ c : ℝ, 0 ≤ c ∧ ∀ y : F, ‖(A†) y‖ ≤ c * ‖(B†) y‖

Uses 2

Proof usesDouglas' lemma: majorization iff factorization · Douglas' lemma: range inclusion iff factorization

17 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.