Finite coefficient matrices as continuous linear maps

A Galerkin weak form starts as a finite matrix of scalar time coefficients. This module assembles those entries as a bounded operator on the real PiLp coefficient space and transfers entrywise a.e. strong measurability to that operator-valued coefficient.

def AVenhance.Infra.Parabolic.FourierGalerkin.matrixRankOne {n : ℕ} (i j : Fin n) : Coefficients n →L[ℝ] Coefficients n

The rank-one coefficient map that sends coordinate j to coordinate i.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.matrixRankOne i j = (PiLp.proj 2 (fun (x : Fin n) => ℝ) j).smulRight (PiLp.single 2 i 1)

def AVenhance.Infra.Parabolic.FourierGalerkin.matrixCoefficientCLM {n : ℕ} (A : Fin n → Fin n → ℝ) : Coefficients n →L[ℝ] Coefficients n

Assemble a scalar real matrix as an operator on the Euclidean coefficient space.

Equations

• AVenhance.Infra.Parabolic.FourierGalerkin.matrixCoefficientCLM A = ∑ i : Fin n, ∑ j : Fin n, A i j • AVenhance.Infra.Parabolic.FourierGalerkin.matrixRankOne i j

@[simp]

theorem AVenhance.Infra.Parabolic.FourierGalerkin.matrixRankOne_apply {n : ℕ} (i j : Fin n) (c : Coefficients n) : (matrixRankOne i j) c = c.ofLp j • PiLp.single 2 i 1

@[simp]

theorem AVenhance.Infra.Parabolic.FourierGalerkin.matrixCoefficientCLM_apply {n : ℕ} (A : Fin n → Fin n → ℝ) (c : Coefficients n) (i : Fin n) : ((matrixCoefficientCLM A) c).ofLp i = ∑ j : Fin n, A i j * c.ofLp j

theorem AVenhance.Infra.Parabolic.FourierGalerkin.MatrixOperator.matrixProjection_norm_le {n : ℕ} (j : Fin n) : ‖PiLp.proj 2 (fun (x : Fin n) => ℝ) j‖ ≤ 1

theorem AVenhance.Infra.Parabolic.FourierGalerkin.MatrixOperator.matrixRankOne_norm_le {n : ℕ} (i j : Fin n) : ‖matrixRankOne i j‖ ≤ 1

theorem AVenhance.Infra.Parabolic.FourierGalerkin.matrixCoefficientCLM_norm_le {n : ℕ} (A : Fin n → Fin n → ℝ) : ‖matrixCoefficientCLM A‖ ≤ ∑ i : Fin n, ∑ j : Fin n, |A i j|

The matrix operator norm is at most the sum of the absolute values of its entries.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.matrixCoefficientCLM_norm_le_uniform {n : ℕ} (A : Fin n → Fin n → ℝ) {K : ℝ} (hA : ∀ (i j : Fin n), |A i j| ≤ K) : ‖matrixCoefficientCLM A‖ ≤ ↑n ^ 2 * K

A uniform scalar bound on every matrix entry gives a dimension-explicit operator bound.

theorem AVenhance.Infra.Parabolic.FourierGalerkin.MatrixOperator.aestronglyMeasurable_finset_sum {ι : Type u_1} {β : Type u_2} [NormedAddCommGroup β] {μ : MeasureTheory.Measure ℝ} (s : Finset ι) (f : ι → ℝ → β) (hf : ∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => ∑ i ∈ s, f i t) μ

theorem AVenhance.Infra.Parabolic.FourierGalerkin.matrixCoefficientCLM_aestronglyMeasurable {n : ℕ} {A : ℝ → Fin n → Fin n → ℝ} {μ : MeasureTheory.Measure ℝ} (hA : ∀ (i j : Fin n), MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => A t i j) μ) : MeasureTheory.AEStronglyMeasurable (fun (t : ℝ) => matrixCoefficientCLM (A t)) μ

Entrywise a.e. strong measurability passes to the finite operator matrix.