Coarse-graining support: Support.CoarseGraining.HilbertMinimizationMeasurability

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Measurability primitives for Hilbert minimizers

This file contains generic measurable-operator facts needed to prove measurable dependence of the Hilbert minimizer maps used in the doubled Mu problem. These are upstream primitives, not Chapter 5 wrappers.

theorem HCPolySupport.continuous_clm_inverse_isInvertible {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] : Continuous fun (T : { T : E →L[ℝ] F // T.IsInvertible }) => (↑T).inverse

Inversion of continuous linear maps is continuous on the subtype of invertible maps.

theorem HCPolySupport.Measurable.clm_inverse_of_isInvertible {Ω : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace Ω] [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {L : Ω → E →L[ℝ] F} (hL : Measurable L) (hInv : ∀ (ω : Ω), (L ω).IsInvertible) : Measurable fun (ω : Ω) => (L ω).inverse

A measurable family of invertible continuous linear maps has a measurable family of inverses.

theorem HCPolySupport.Measurable.clm_apply {Ω : Type u_1} {E : Type u_2} {F : Type u_3} [MeasurableSpace Ω] [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [MeasurableSpace F] [BorelSpace F] {L : Ω → E →L[ℝ] F} {x : Ω → E} [OpensMeasurableSpace ((E →L[ℝ] F) × E)] (hL : Measurable L) (hx : Measurable x) : Measurable fun (ω : Ω) => (L ω) (x ω)

Joint measurability of applying a measurable family of continuous linear maps to a measurable family of vectors.

theorem HCPolySupport.measurable_matrix_inv_entry {d : ℕ} {α : Type u_1} [MeasurableSpace α] {A : α → Fin d → Fin d → ℝ} (hA : Measurable A) (i j : Fin d) : Measurable fun (x : α) => (A x)⁻¹ i j

Entries of the total matrix inverse are measurable functions of the matrix entries. This is a finite-dimensional primitive used by Galerkin approximations; invertibility is not needed for measurability because Lean's matrix inverse is total.

noncomputable def HCPolySupport.galerkinMatrix {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (B : V →L[ℝ] V →L[ℝ] ℝ) (e : Fin n → V) : Fin n → Fin n → ℝ

The finite Galerkin Gram matrix for the bilinear form B on a selected finite family of correction vectors.

Equations

• HCPolySupport.galerkinMatrix B e i j = (B (e j)) (e i)

noncomputable def HCPolySupport.galerkinRhs {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (B : V →L[ℝ] V →L[ℝ] ℝ) (x : V) (e : Fin n → V) : Fin n → ℝ

The finite Galerkin right-hand side for the affine shift x.

Equations

• HCPolySupport.galerkinRhs B x e i = -(B x) (e i)

noncomputable def HCPolySupport.galerkinCoeff {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (B : V →L[ℝ] V →L[ℝ] ℝ) (x : V) (e : Fin n → V) : Fin n → ℝ

The coordinate vector obtained from the total inverse of the finite Galerkin Gram matrix. Coercivity later identifies this total inverse with the honest finite-dimensional inverse.

Equations

• HCPolySupport.galerkinCoeff B x e j = ∑ i : Fin n, (HCPolySupport.galerkinMatrix B e)⁻¹ j i * HCPolySupport.galerkinRhs B x e i

noncomputable def HCPolySupport.galerkinCorrection {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (B : V →L[ℝ] V →L[ℝ] ℝ) (x : V) (e : Fin n → V) : V

The finite Galerkin correction vector assembled from its measurable coordinate vector.

Equations

• HCPolySupport.galerkinCorrection B x e = ∑ j : Fin n, HCPolySupport.galerkinCoeff B x e j • e j

noncomputable def HCPolySupport.galerkinAffineMinimizer {V : Type u_2} [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} (B : V →L[ℝ] V →L[ℝ] ℝ) (x : V) (e : Fin n → V) : V

The finite Galerkin affine minimizer.

Equations

• HCPolySupport.galerkinAffineMinimizer B x e = x + HCPolySupport.galerkinCorrection B x e

theorem HCPolySupport.measurable_galerkinMatrix {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {e : Fin n → V} (hB : ∀ (i j : Fin n), Measurable fun (ω : Ω) => ((B ω) (e j)) (e i)) : Measurable fun (ω : Ω) => galerkinMatrix (B ω) e

Measurability of the finite Galerkin Gram matrix from scalar probe measurability of the bilinear form.

theorem HCPolySupport.measurable_galerkinRhs {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {x : Ω → V} {e : Fin n → V} (hBx : ∀ (i : Fin n), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e i)) : Measurable fun (ω : Ω) => galerkinRhs (B ω) (x ω) e

Measurability of the finite Galerkin right-hand side from scalar probe measurability.

theorem HCPolySupport.measurable_galerkinCoeff {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {x : Ω → V} {e : Fin n → V} (hB : ∀ (i j : Fin n), Measurable fun (ω : Ω) => ((B ω) (e j)) (e i)) (hBx : ∀ (i : Fin n), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e i)) : Measurable fun (ω : Ω) => galerkinCoeff (B ω) (x ω) e

Measurability of the finite Galerkin coefficient vector.

theorem HCPolySupport.measurable_galerkinCorrection {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} [MeasurableSpace V] [MeasurableAdd₂ V] [MeasurableSMul ℝ V] {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {x : Ω → V} {e : Fin n → V} (hB : ∀ (i j : Fin n), Measurable fun (ω : Ω) => ((B ω) (e j)) (e i)) (hBx : ∀ (i : Fin n), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e i)) : Measurable fun (ω : Ω) => galerkinCorrection (B ω) (x ω) e

Measurability of each finite Galerkin correction.

theorem HCPolySupport.measurable_galerkinAffineMinimizer {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} [MeasurableSpace V] [MeasurableAdd₂ V] [MeasurableSMul ℝ V] {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {x : Ω → V} {e : Fin n → V} (hx : Measurable x) (hB : ∀ (i j : Fin n), Measurable fun (ω : Ω) => ((B ω) (e j)) (e i)) (hBx : ∀ (i : Fin n), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e i)) : Measurable fun (ω : Ω) => galerkinAffineMinimizer (B ω) (x ω) e

Measurability of each finite Galerkin affine minimizer.

theorem HCPolySupport.stronglyMeasurable_galerkinAffineMinimizer_of_scalar_probes {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [NormedSpace ℝ V] {n : ℕ} {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {x : Ω → V} {e : Fin n → V} (hx : MeasureTheory.StronglyMeasurable x) (hB : ∀ (i j : Fin n), Measurable fun (ω : Ω) => ((B ω) (e j)) (e i)) (hBx : ∀ (i : Fin n), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e i)) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => galerkinAffineMinimizer (B ω) (x ω) e

Strong measurability of each finite Galerkin affine minimizer from scalar Gram/RHS probe measurability. Unlike measurable_galerkinAffineMinimizer, this theorem does not require a second-countable target space; it assembles the finite-dimensional correction from strongly measurable real coordinates.

theorem HCPolySupport.stronglyMeasurable_of_tendsto_galerkinAffineMinimizer {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace V] [SecondCountableTopology V] [OpensMeasurableSpace V] [MeasurableAdd₂ V] [MeasurableSMul ℝ V] {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {x : Ω → V} {e : (m : ℕ) → Fin m → V} {u : Ω → V} (hx : Measurable x) (hB : ∀ (m : ℕ) (i j : Fin m), Measurable fun (ω : Ω) => ((B ω) (e m j)) (e m i)) (hBx : ∀ (m : ℕ) (i : Fin m), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e m i)) (hlim : Filter.Tendsto (fun (m : ℕ) (ω : Ω) => galerkinAffineMinimizer (B ω) (x ω) (e m)) Filter.atTop (nhds u)) : MeasureTheory.StronglyMeasurable u

A pointwise limit of finite Galerkin affine minimizers is strongly measurable. This is the generic measurability bridge for selected Hilbert solutions once convergence of the Galerkin scheme has been proved.

theorem HCPolySupport.stronglyMeasurable_of_tendsto_galerkinAffineMinimizer_of_scalar_probes {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [NormedSpace ℝ V] {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {x : Ω → V} {e : (m : ℕ) → Fin m → V} {u : Ω → V} (hx : MeasureTheory.StronglyMeasurable x) (hB : ∀ (m : ℕ) (i j : Fin m), Measurable fun (ω : Ω) => ((B ω) (e m j)) (e m i)) (hBx : ∀ (m : ℕ) (i : Fin m), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e m i)) (hlim : Filter.Tendsto (fun (m : ℕ) (ω : Ω) => galerkinAffineMinimizer (B ω) (x ω) (e m)) Filter.atTop (nhds u)) : MeasureTheory.StronglyMeasurable u

A pointwise limit of finite Galerkin affine minimizers is strongly measurable, using the finite-dimensional strong-measurability theorem and therefore avoiding any second-countability assumption on the Hilbert target.

theorem HCPolySupport.aestronglyMeasurable_of_tendsto_ae_galerkinAffineMinimizer {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [NormedSpace ℝ V] [MeasurableSpace V] [SecondCountableTopology V] [OpensMeasurableSpace V] [MeasurableAdd₂ V] [MeasurableSMul ℝ V] {μ : MeasureTheory.Measure Ω} {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {x : Ω → V} {e : (m : ℕ) → Fin m → V} {u : Ω → V} (hx : Measurable x) (hB : ∀ (m : ℕ) (i j : Fin m), Measurable fun (ω : Ω) => ((B ω) (e m j)) (e m i)) (hBx : ∀ (m : ℕ) (i : Fin m), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e m i)) (hlim : ∀ᵐ (ω : Ω) ∂μ, Filter.Tendsto (fun (m : ℕ) => galerkinAffineMinimizer (B ω) (x ω) (e m)) Filter.atTop (nhds (u ω))) : MeasureTheory.AEStronglyMeasurable u μ

An a.e. pointwise limit of finite Galerkin affine minimizers is a.e.-strongly measurable.

theorem HCPolySupport.stronglyMeasurable_of_galerkin_energy_approximants {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {hB : ∀ (ω : Ω), IsCoercive (B ω)} (h_symm : ∀ (ω : Ω) (u v : V), ((B ω) u) v = ((B ω) v) u) {x : Ω → V} {e : (m : ℕ) → Fin m → V} {v : Ω → ℕ → V} (hx : MeasureTheory.StronglyMeasurable x) (hB_meas : ∀ (m : ℕ) (i j : Fin m), Measurable fun (ω : Ω) => ((B ω) (e m j)) (e m i)) (hBx_meas : ∀ (m : ℕ) (i : Fin m), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e m i)) (hGalerkin_mem : ∀ (ω : Ω) (m : ℕ), galerkinAffineMinimizer (B ω) (x ω) (e m) - x ω ∈ K) (hv_mem : ∀ (ω : Ω) (m : ℕ), v ω m - x ω ∈ K) (hEnergy : ∀ (ω : Ω) (m : ℕ), quadraticEnergy (B ω) (galerkinAffineMinimizer (B ω) (x ω) (e m)) ≤ quadraticEnergy (B ω) (v ω m)) (hv_tendsto : ∀ (ω : Ω), Filter.Tendsto (fun (m : ℕ) => v ω m) Filter.atTop (nhds ((affineMinimizerMap K (B ω) ⋯) (x ω)))) : MeasureTheory.StronglyMeasurable fun (ω : Ω) => (affineMinimizerMap K (B ω) ⋯) (x ω)

The selected affine Hilbert minimizer is strongly measurable once finite Galerkin minimizers satisfy the deterministic energy-comparison convergence hypotheses. This is the generic "finite Galerkin convergence implies measurable maximizer/minimizer" bridge.

theorem HCPolySupport.aestronglyMeasurable_of_galerkin_energy_approximants {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {μ : MeasureTheory.Measure Ω} (K : ClosedSubmodule ℝ V) {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {hB : ∀ (ω : Ω), IsCoercive (B ω)} (h_symm : ∀ (ω : Ω) (u v : V), ((B ω) u) v = ((B ω) v) u) {x : Ω → V} {e : (m : ℕ) → Fin m → V} {v : Ω → ℕ → V} (hx : MeasureTheory.StronglyMeasurable x) (hB_meas : ∀ (m : ℕ) (i j : Fin m), Measurable fun (ω : Ω) => ((B ω) (e m j)) (e m i)) (hBx_meas : ∀ (m : ℕ) (i : Fin m), Measurable fun (ω : Ω) => ((B ω) (x ω)) (e m i)) (hGalerkin_mem : ∀ (ω : Ω) (m : ℕ), galerkinAffineMinimizer (B ω) (x ω) (e m) - x ω ∈ K) (hv_mem : ∀ (ω : Ω) (m : ℕ), v ω m - x ω ∈ K) (hEnergy : ∀ (ω : Ω) (m : ℕ), quadraticEnergy (B ω) (galerkinAffineMinimizer (B ω) (x ω) (e m)) ≤ quadraticEnergy (B ω) (v ω m)) (hv_tendsto : ∀ (ω : Ω), Filter.Tendsto (fun (m : ℕ) => v ω m) Filter.atTop (nhds ((affineMinimizerMap K (B ω) ⋯) (x ω)))) : MeasureTheory.AEStronglyMeasurable (fun (ω : Ω) => (affineMinimizerMap K (B ω) ⋯) (x ω)) μ

A.e.-strong measurability version of stronglyMeasurable_of_galerkin_energy_approximants.

theorem HCPolySupport.correctionMap_eq_clm_inverse_restrictBilin {V : Type u_2} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (x : V) : (correctionMap K B hB) x = (InnerProductSpace.continuousLinearMapOfBilin (restrictBilin K B)).inverse ((subspaceRhs K B) x)

The Hilbert correction map is the inverse of the Lax-Milgram operator on the restricted correction subspace, applied to the affine right-hand side.

theorem HCPolySupport.Measurable.correctionMap_apply {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [MeasurableSpace V] (K : ClosedSubmodule ℝ V) [BorelSpace ↥↑K] [OpensMeasurableSpace ((↥↑K →L[ℝ] ↥↑K) × ↥↑K)] {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {hB : ∀ (ω : Ω), IsCoercive (B ω)} {x : Ω → V} (hSharp : Measurable fun (ω : Ω) => InnerProductSpace.continuousLinearMapOfBilin (restrictBilin K (B ω))) (hRhs : Measurable fun (ω : Ω) => (subspaceRhs K (B ω)) (x ω)) : Measurable fun (ω : Ω) => (correctionMap K (B ω) ⋯) (x ω)

Measurability of the Hilbert correction map follows from measurability of the restricted Lax-Milgram operator and the affine right-hand side.

theorem HCPolySupport.Measurable.affineMinimizerMap_apply {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] [MeasurableSpace V] [MeasurableAdd₂ V] (K : ClosedSubmodule ℝ V) [BorelSpace ↥↑K] [OpensMeasurableSpace ((↥↑K →L[ℝ] ↥↑K) × ↥↑K)] {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {hB : ∀ (ω : Ω), IsCoercive (B ω)} {x : Ω → V} (hx : Measurable x) (hSharp : Measurable fun (ω : Ω) => InnerProductSpace.continuousLinearMapOfBilin (restrictBilin K (B ω))) (hRhs : Measurable fun (ω : Ω) => (subspaceRhs K (B ω)) (x ω)) : Measurable fun (ω : Ω) => (affineMinimizerMap K (B ω) ⋯) (x ω)

Measurability of the affine Hilbert minimizer follows from measurability of the affine shift, the restricted Lax-Milgram operator, and the affine right-hand side.

theorem HCPolySupport.Measurable.parameterAffineMinimizerMap_apply {Ω : Type u_1} {V : Type u_2} [MeasurableSpace Ω] [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [OpensMeasurableSpace E] [MeasurableSpace V] [BorelSpace V] [MeasurableAdd₂ V] (K : ClosedSubmodule ℝ V) [BorelSpace ↥↑K] [OpensMeasurableSpace ((↥↑K →L[ℝ] ↥↑K) × ↥↑K)] {B : Ω → V →L[ℝ] V →L[ℝ] ℝ} {hB : ∀ (ω : Ω), IsCoercive (B ω)} (ι : E →L[ℝ] V) {p : Ω → E} (hp : Measurable p) (hSharp : Measurable fun (ω : Ω) => InnerProductSpace.continuousLinearMapOfBilin (restrictBilin K (B ω))) (hRhs : Measurable fun (ω : Ω) => (subspaceRhs K (B ω)) (ι (p ω))) : Measurable fun (ω : Ω) => (parameterAffineMinimizerMap K (B ω) ⋯ ι) (p ω)

Measurability of the parameterized affine Hilbert minimizer.