This file provides finite-dimensional Hilbert realizations of \R^d and \R^{2d} that stay compatible with the project's anti-EuclideanSpace architecture.

The ambient algebraic carriers remain

• Vec d = Fin d → ℝ,
• BlockVec d = Vec d × Vec d.

Those are excellent lightweight types for most of the development, but their default normed-space instances are not the Euclidean L² ones needed for the Hilbert-space part of the coarse-graining theory. For that role we introduce separate wrappers built from PiLp 2.

@[reducible, inline]

abbrev Homogenization.HilbertVec (d : ℕ) : Type

The Euclidean Hilbert realization of \R^d, presented without exposing EuclideanSpace in the public API.

Equations

• Homogenization.HilbertVec d = PiLp 2 fun (x : Fin d) => ℝ

@[reducible, inline]

abbrev Homogenization.HilbertVec.ofVec {d : ℕ} (x : Vec d) : HilbertVec d

Promote the project's algebraic vector carrier into the Euclidean Hilbert carrier.

Equations

• Homogenization.HilbertVec.ofVec x = WithLp.toLp 2 x

@[reducible, inline]

abbrev Homogenization.HilbertVec.toVec {d : ℕ} (x : HilbertVec d) : Vec d

Forget the Hilbert structure and return to the project's algebraic vector carrier.

Equations

• x.toVec i = x.ofLp i

@[simp]

theorem Homogenization.HilbertVec.toVec_ofVec {d : ℕ} (x : Vec d) : (ofVec x).toVec = x

@[simp]

theorem Homogenization.HilbertVec.ofVec_toVec {d : ℕ} (x : HilbertVec d) : ofVec x.toVec = x

theorem Homogenization.HilbertVec.ext {d : ℕ} {x y : HilbertVec d} (h : ∀ (i : Fin d), x.ofLp i = y.ofLp i) : x = y

theorem Homogenization.HilbertVec.ext_iff {d : ℕ} {x y : HilbertVec d} : x = y ↔ ∀ (i : Fin d), x.ofLp i = y.ofLp i

def Homogenization.HilbertVec.linearEquivVec (d : ℕ) : HilbertVec d ≃ₗ[ℝ] Vec d

Algebraic identification between the Euclidean Hilbert carrier and the project's lightweight vector carrier.

Equations

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

noncomputable def Homogenization.HilbertVec.continuousLinearEquivVec (d : ℕ) : HilbertVec d ≃L[ℝ] Vec d

Continuous linear identification between the Euclidean Hilbert carrier and the project's lightweight vector carrier.

Equations

• Homogenization.HilbertVec.continuousLinearEquivVec d = (Homogenization.HilbertVec.linearEquivVec d).toContinuousLinearEquiv

@[simp]

theorem Homogenization.HilbertVec.continuousLinearEquivVec_apply {d : ℕ} (x : HilbertVec d) : (continuousLinearEquivVec d) x = x.toVec

@[simp]

theorem Homogenization.HilbertVec.continuousLinearEquivVec_symm_apply {d : ℕ} (x : Vec d) : (continuousLinearEquivVec d).symm x = ofVec x

@[simp]

theorem Homogenization.HilbertVec.inner_def {d : ℕ} (x y : HilbertVec d) : inner ℝ x y = vecDot x.toVec y.toVec

@[simp]

theorem Homogenization.HilbertVec.norm_sq_eq_sum_sq {d : ℕ} (x : HilbertVec d) : ‖x‖ ^ 2 = ∑ i : Fin d, x.ofLp i ^ 2

theorem Homogenization.HilbertVec.abs_apply_le_norm {d : ℕ} (x : HilbertVec d) (i : Fin d) : |x.ofLp i| ≤ ‖x‖

theorem Homogenization.HilbertVec.norm_toVec_le_norm {d : ℕ} (x : HilbertVec d) : ‖x.toVec‖ ≤ ‖x‖

theorem Homogenization.HilbertVec.norm_le_norm_ofVec {d : ℕ} (x : Vec d) : ‖x‖ ≤ ‖ofVec x‖

theorem Homogenization.HilbertVec.norm_ofVec_le_mul_norm {d : ℕ} (x : Vec d) : ‖ofVec x‖ ≤ ↑d * ‖x‖

@[reducible, inline]

noncomputable abbrev Homogenization.HilbertVec.ofVecL (d : ℕ) : Vec d →L[ℝ] HilbertVec d

Continuous linear promotion from the project's algebraic vector carrier to the Euclidean Hilbert carrier.

Equations

• Homogenization.HilbertVec.ofVecL d = ↑(Homogenization.HilbertVec.continuousLinearEquivVec d).symm

@[simp]

theorem Homogenization.HilbertVec.ofVecL_apply {d : ℕ} (x : Vec d) : (ofVecL d) x = ofVec x

theorem Homogenization.HilbertVec.norm_ofVecL_le (d : ℕ) : ‖ofVecL d‖ ≤ ↑d

theorem Homogenization.HilbertVec.norm_continuousLinearEquivVec_le (d : ℕ) : ‖↑(continuousLinearEquivVec d)‖ ≤ 1

@[reducible, inline]

abbrev Homogenization.HilbertMat (d : ℕ) : Type

The Euclidean Hilbert realization of d × d real matrices. The algebraic carrier Mat d keeps its lightweight pointwise role; this wrapper is for Hilbert-space measurability and L² arguments.

Equations

• Homogenization.HilbertMat d = PiLp 2 fun (x : Fin d) => Homogenization.HilbertVec d

@[reducible, inline]

abbrev Homogenization.HilbertMat.ofMat {d : ℕ} (A : Mat d) : HilbertMat d

Promote the project's algebraic matrix carrier into the Euclidean Hilbert matrix carrier.

Equations

• Homogenization.HilbertMat.ofMat A = WithLp.toLp 2 fun (i : Fin d) => Homogenization.HilbertVec.ofVec fun (j : Fin d) => A i j

@[reducible, inline]

abbrev Homogenization.HilbertMat.toMat {d : ℕ} (A : HilbertMat d) : Mat d

Forget the Hilbert structure and return to the project's algebraic matrix carrier.

Equations

• A.toMat i j = (A.ofLp i).ofLp j

@[simp]

theorem Homogenization.HilbertMat.toMat_ofMat {d : ℕ} (A : Mat d) : (ofMat A).toMat = A

@[simp]

theorem Homogenization.HilbertMat.ofMat_toMat {d : ℕ} (A : HilbertMat d) : ofMat A.toMat = A

theorem Homogenization.HilbertMat.ext {d : ℕ} {A B : HilbertMat d} (h : ∀ (i j : Fin d), (A.ofLp i).ofLp j = (B.ofLp i).ofLp j) : A = B

theorem Homogenization.HilbertMat.ext_iff {d : ℕ} {A B : HilbertMat d} : A = B ↔ ∀ (i j : Fin d), (A.ofLp i).ofLp j = (B.ofLp i).ofLp j

def Homogenization.HilbertMat.linearEquivMat (d : ℕ) : HilbertMat d ≃ₗ[ℝ] Mat d

Algebraic identification between the Euclidean Hilbert matrix carrier and the project's lightweight matrix carrier.

Equations

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

noncomputable def Homogenization.HilbertMat.continuousLinearEquivMat (d : ℕ) : HilbertMat d ≃L[ℝ] Mat d

Continuous linear identification between the Euclidean Hilbert matrix carrier and the project's lightweight matrix carrier.

Equations

• Homogenization.HilbertMat.continuousLinearEquivMat d = (Homogenization.HilbertMat.linearEquivMat d).toContinuousLinearEquiv

@[simp]

theorem Homogenization.HilbertMat.continuousLinearEquivMat_apply {d : ℕ} (A : HilbertMat d) : (continuousLinearEquivMat d) A = A.toMat

@[simp]

theorem Homogenization.HilbertMat.continuousLinearEquivMat_symm_apply {d : ℕ} (A : Mat d) : (continuousLinearEquivMat d).symm A = ofMat A

noncomputable def Homogenization.HilbertMat.entryL {d : ℕ} (i j : Fin d) : HilbertMat d →L[ℝ] ℝ

The (i,j) matrix coordinate as a continuous linear functional on the Hilbert matrix carrier.

Equations

• Homogenization.HilbertMat.entryL i j = PiLp.proj 2 (fun (x : Fin d) => ℝ) j ∘SL PiLp.proj 2 (fun (x : Fin d) => Homogenization.HilbertVec d) i

@[simp]

theorem Homogenization.HilbertMat.entryL_apply {d : ℕ} (i j : Fin d) (A : HilbertMat d) : (entryL i j) A = (A.ofLp i).ofLp j

@[simp]

theorem Homogenization.HilbertMat.entryL_ofMat {d : ℕ} (i j : Fin d) (A : Mat d) : (entryL i j) (ofMat A) = A i j

theorem Homogenization.HilbertMat.abs_apply_sub_apply_le_norm {d : ℕ} (A B : HilbertMat d) (i j : Fin d) : |(A.ofLp i).ofLp j - (B.ofLp i).ofLp j| ≤ ‖A - B‖

theorem Homogenization.HilbertMat.lipschitzWith_entry {d : ℕ} (i j : Fin d) : LipschitzWith 1 fun (A : HilbertMat d) => (A.ofLp i).ofLp j

@[simp]

theorem Homogenization.HilbertMat.inner_def {d : ℕ} (A B : HilbertMat d) : inner ℝ A B = ∑ i : Fin d, ∑ j : Fin d, (A.ofLp i).ofLp j * (B.ofLp i).ofLp j

@[reducible, inline]

abbrev Homogenization.HilbertBlockVec (d : ℕ) : Type

The Euclidean Hilbert realization of \R^{2d}, viewed as a doubled potential/flux carrier.

Equations

• Homogenization.HilbertBlockVec d = PiLp 2 fun (x : Fin 2) => Homogenization.HilbertVec d

@[reducible, inline]

abbrev Homogenization.HilbertBlockVec.potential {d : ℕ} (X : HilbertBlockVec d) : HilbertVec d

The potential component of a doubled Hilbert vector.

Equations

• X.potential = X.ofLp 0

@[reducible, inline]

abbrev Homogenization.HilbertBlockVec.flux {d : ℕ} (X : HilbertBlockVec d) : HilbertVec d

The flux component of a doubled Hilbert vector.

Equations

• X.flux = X.ofLp 1

@[reducible, inline]

abbrev Homogenization.HilbertBlockVec.ofBlockVec {d : ℕ} (X : BlockVec d) : HilbertBlockVec d

Promote the project's algebraic doubled vector carrier into the Euclidean Hilbert carrier.

Equations

• Homogenization.HilbertBlockVec.ofBlockVec X = !₂[Homogenization.HilbertVec.ofVec X.1, Homogenization.HilbertVec.ofVec X.2]

@[reducible, inline]

abbrev Homogenization.HilbertBlockVec.toBlockVec {d : ℕ} (X : HilbertBlockVec d) : BlockVec d

Forget the Hilbert structure and return to the project's algebraic doubled vector carrier.

Equations

• X.toBlockVec = (X.potential.toVec, X.flux.toVec)

@[simp]

theorem Homogenization.HilbertBlockVec.potential_ofBlockVec {d : ℕ} (X : BlockVec d) : (ofBlockVec X).potential = HilbertVec.ofVec X.1

@[simp]

theorem Homogenization.HilbertBlockVec.flux_ofBlockVec {d : ℕ} (X : BlockVec d) : (ofBlockVec X).flux = HilbertVec.ofVec X.2

@[simp]

theorem Homogenization.HilbertBlockVec.toBlockVec_ofBlockVec {d : ℕ} (X : BlockVec d) : (ofBlockVec X).toBlockVec = X

@[simp]

theorem Homogenization.HilbertBlockVec.ofBlockVec_toBlockVec {d : ℕ} (X : HilbertBlockVec d) : ofBlockVec X.toBlockVec = X

theorem Homogenization.HilbertBlockVec.ext {d : ℕ} {X Y : HilbertBlockVec d} (hpot : X.potential = Y.potential) (hflux : X.flux = Y.flux) : X = Y

theorem Homogenization.HilbertBlockVec.ext_iff {d : ℕ} {X Y : HilbertBlockVec d} : X = Y ↔ X.potential = Y.potential ∧ X.flux = Y.flux

def Homogenization.HilbertBlockVec.linearEquivBlockVec (d : ℕ) : HilbertBlockVec d ≃ₗ[ℝ] BlockVec d

Algebraic identification between the Euclidean doubled Hilbert carrier and the project's lightweight block carrier.

Equations

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

noncomputable def Homogenization.HilbertBlockVec.continuousLinearEquivBlockVec (d : ℕ) : HilbertBlockVec d ≃L[ℝ] BlockVec d

Continuous linear identification between the Euclidean doubled Hilbert carrier and the project's lightweight block carrier.

Equations

• Homogenization.HilbertBlockVec.continuousLinearEquivBlockVec d = (Homogenization.HilbertBlockVec.linearEquivBlockVec d).toContinuousLinearEquiv

@[simp]

theorem Homogenization.HilbertBlockVec.continuousLinearEquivBlockVec_apply {d : ℕ} (X : HilbertBlockVec d) : (continuousLinearEquivBlockVec d) X = X.toBlockVec

@[simp]

theorem Homogenization.HilbertBlockVec.continuousLinearEquivBlockVec_symm_apply {d : ℕ} (X : BlockVec d) : (continuousLinearEquivBlockVec d).symm X = ofBlockVec X

noncomputable def Homogenization.HilbertBlockVec.applyBlockMat {d : ℕ} (A : BlockMat d) : HilbertBlockVec d →L[ℝ] HilbertBlockVec d

A block matrix acts continuously on the Euclidean Hilbert realization of \R^{2d} by conjugating the algebraic action through the canonical identification HilbertBlockVec d ≃L[ℝ] BlockVec d.

Equations

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

@[simp]

theorem Homogenization.HilbertBlockVec.applyBlockMat_apply {d : ℕ} (A : BlockMat d) (X : HilbertBlockVec d) : (applyBlockMat A) X = ofBlockVec (blockMatVecMul A X.toBlockVec)

@[simp]

theorem Homogenization.HilbertBlockVec.inner_def {d : ℕ} (X Y : HilbertBlockVec d) : inner ℝ X Y = blockVecDot X.toBlockVec Y.toBlockVec

theorem Homogenization.HilbertBlockVec.inner_ofBlockVec_applyBlockMat {d : ℕ} (A : BlockMat d) (X Y : BlockVec d) : inner ℝ (ofBlockVec X) ((applyBlockMat A) (ofBlockVec Y)) = blockVecDot X (blockMatVecMul A Y)

theorem Homogenization.HilbertBlockVec.norm_sq_ofBlockVec {d : ℕ} (X : BlockVec d) : ‖ofBlockVec X‖ ^ 2 = blockVecDot X X

@[simp]

theorem Homogenization.HilbertBlockVec.norm_sq_eq_blockVecDot {d : ℕ} (X : HilbertBlockVec d) : ‖X‖ ^ 2 = blockVecDot X.toBlockVec X.toBlockVec

theorem Homogenization.HilbertBlockVec.norm_sq_applyBlockMat {d : ℕ} (A : BlockMat d) (X : HilbertBlockVec d) : ‖(applyBlockMat A) X‖ ^ 2 = blockVecDot (blockMatVecMul A X.toBlockVec) (blockMatVecMul A X.toBlockVec)

theorem Homogenization.HilbertBlockVec.opNorm_applyBlockMat_le_of_block_bound {d : ℕ} {A : BlockMat d} {C : ℝ} (hC : 0 ≤ C) (hA : ∀ (X : BlockVec d), blockVecDot (blockMatVecMul A X) (blockMatVecMul A X) ≤ C ^ 2 * blockVecDot X X) : ‖applyBlockMat A‖ ≤ C

theorem Homogenization.HilbertBlockVec.norm_sq_eq_components {d : ℕ} (X : HilbertBlockVec d) : ‖X‖ ^ 2 = ‖X.potential‖ ^ 2 + ‖X.flux‖ ^ 2

theorem Homogenization.HilbertBlockVec.norm_sq_eq_sum_sq {d : ℕ} (X : HilbertBlockVec d) : ‖X‖ ^ 2 = ∑ i : Fin d, X.potential.ofLp i ^ 2 + ∑ i : Fin d, X.flux.ofLp i ^ 2