Coarse-graining support: Support.CoarseGraining.HilbertMinimization

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

This file records the abstract Hilbert-space minimization step behind the construction of the doubled \mu-minimizers in the coarse-graining notes.

The setup is a real Hilbert space V, a coercive continuous bilinear form B : V →L[ℝ] V →L[ℝ] ℝ, and a closed subspace K. For each affine shift x : V, we build the unique correction k(x) ∈ K such that x + k(x) is stationary against variations in K. Under symmetry of B, this stationary point minimizes the quadratic energy on the affine space x + K.

instance HCPolySupport.closedSubmodule_completeSpace {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) : CompleteSpace ↥↑K

noncomputable def HCPolySupport.quadraticEnergy {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (B : V →L[ℝ] V →L[ℝ] ℝ) (u : V) : ℝ

The quadratic energy attached to a continuous bilinear form.

Equations

• HCPolySupport.quadraticEnergy B u = 1 / 2 * (B u) u

theorem HCPolySupport.quadraticEnergy_nonneg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (u : V) : 0 ≤ quadraticEnergy B u

theorem HCPolySupport.quadraticEnergy_add {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {B : V →L[ℝ] V →L[ℝ] ℝ} (h_symm : ∀ (u v : V), (B u) v = (B v) u) (u v : V) : quadraticEnergy B (u + v) = quadraticEnergy B u + (B u) v + quadraticEnergy B v

theorem HCPolySupport.quadraticEnergy_continuous {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (B : V →L[ℝ] V →L[ℝ] ℝ) : Continuous (quadraticEnergy B)

noncomputable def HCPolySupport.linearQuadraticResponse {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (B : V →L[ℝ] V →L[ℝ] ℝ) (ℓ : V →L[ℝ] ℝ) (u : V) : ℝ

The concave quadratic response ℓ(u) - 1 / 2 B(u,u) attached to a continuous linear functional and a coercive bilinear form.

Equations

• HCPolySupport.linearQuadraticResponse B ℓ u = ℓ u - HCPolySupport.quadraticEnergy B u

theorem HCPolySupport.linearQuadraticResponse_le_of_firstVariation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {B : V →L[ℝ] V →L[ℝ] ℝ} {ℓ : V →L[ℝ] ℝ} (hB : IsCoercive B) (h_symm : ∀ (u v : V), (B u) v = (B v) u) {u v : V} (hfirst : ∀ (w : V), (B u) w = ℓ w) : linearQuadraticResponse B ℓ v ≤ linearQuadraticResponse B ℓ u

noncomputable def HCPolySupport.rieszRep {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (ℓ : V →L[ℝ] ℝ) : V

The Riesz representative of a continuous linear functional.

Equations

• HCPolySupport.rieszRep ℓ = (InnerProductSpace.toDual ℝ V).symm ℓ

@[simp]

theorem HCPolySupport.inner_rieszRep_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (ℓ : V →L[ℝ] ℝ) (w : V) : inner ℝ (rieszRep ℓ) w = ℓ w

noncomputable def HCPolySupport.linearQuadraticResponseMaximizer {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (ℓ : V →L[ℝ] ℝ) : V

The unique stationary point for the concave quadratic response associated to a coercive bilinear form.

Equations

• HCPolySupport.linearQuadraticResponseMaximizer B hB ℓ = hB.continuousLinearEquivOfBilin.symm (HCPolySupport.rieszRep ℓ)

theorem HCPolySupport.linearQuadraticResponseMaximizer_firstVariation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (ℓ : V →L[ℝ] ℝ) (w : V) : (B (linearQuadraticResponseMaximizer B hB ℓ)) w = ℓ w

theorem HCPolySupport.linearQuadraticResponse_le_maximizer {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (h_symm : ∀ (u v : V), (B u) v = (B v) u) (ℓ : V →L[ℝ] ℝ) (v : V) : linearQuadraticResponse B ℓ v ≤ linearQuadraticResponse B ℓ (linearQuadraticResponseMaximizer B hB ℓ)

theorem HCPolySupport.isBoundedBilinearMap_restrict {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {B : V →L[ℝ] V →L[ℝ] ℝ} (K : ClosedSubmodule ℝ V) : IsBoundedBilinearMap ℝ fun (p : ↥↑K × ↥↑K) => (B ↑p.1) ↑p.2

noncomputable def HCPolySupport.restrictBilin {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) : ↥↑K →L[ℝ] ↥↑K →L[ℝ] ℝ

Restrict a continuous bilinear form to a closed subspace.

Equations

• HCPolySupport.restrictBilin K B = ⋯.toContinuousLinearMap

@[simp]

theorem HCPolySupport.restrictBilin_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (u w : ↥↑K) : ((restrictBilin K B) u) w = (B ↑u) ↑w

theorem HCPolySupport.isCoercive_restrictBilin {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {B : V →L[ℝ] V →L[ℝ] ℝ} (K : ClosedSubmodule ℝ V) (hB : IsCoercive B) : IsCoercive (restrictBilin K B)

theorem HCPolySupport.isBoundedBilinearMap_subspaceRhs {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {B : V →L[ℝ] V →L[ℝ] ℝ} (K : ClosedSubmodule ℝ V) : IsBoundedBilinearMap ℝ fun (p : V × ↥↑K) => -(B p.1) ↑p.2

noncomputable def HCPolySupport.subspaceRhsBilin {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) : V →L[ℝ] ↥↑K →L[ℝ] ℝ

The continuous family of linear functionals w ↦ -B x w on the closed subspace K.

Equations

• HCPolySupport.subspaceRhsBilin K B = ⋯.toContinuousLinearMap

@[simp]

theorem HCPolySupport.subspaceRhsBilin_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (x : V) (w : ↥↑K) : ((subspaceRhsBilin K B) x) w = -(B x) ↑w

noncomputable def HCPolySupport.subspaceRieszMap {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) : (↥↑K →L[ℝ] ℝ) →L[ℝ] ↥↑K

Riesz representation on the closed subspace K.

Equations

• HCPolySupport.subspaceRieszMap K = ↑↑(InnerProductSpace.toDual ℝ ↥↑K).symm

theorem HCPolySupport.inner_subspaceRieszMap_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (ℓ : ↥↑K →L[ℝ] ℝ) (w : ↥↑K) : inner ℝ ((subspaceRieszMap K) ℓ) w = ℓ w

noncomputable def HCPolySupport.subspaceRhs {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) : V →L[ℝ] ↥↑K

The Riesz representatives of the functionals w ↦ -B x w on K.

Equations

• HCPolySupport.subspaceRhs K B = HCPolySupport.subspaceRieszMap K ∘SL HCPolySupport.subspaceRhsBilin K B

theorem HCPolySupport.inner_subspaceRhs_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (x : V) (w : ↥↑K) : inner ℝ ((subspaceRhs K B) x) w = -(B x) ↑w

noncomputable def HCPolySupport.correctionMap {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) : V →L[ℝ] ↥↑K

The unique correction in K solving the affine first-variation equation.

Equations

• HCPolySupport.correctionMap K B hB = ↑⋯.continuousLinearEquivOfBilin.symm ∘SL HCPolySupport.subspaceRhs K B

theorem HCPolySupport.restrictBilin_correctionMap_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (x : V) (w : ↥↑K) : ((restrictBilin K B) ((correctionMap K B hB) x)) w = -(B x) ↑w

noncomputable def HCPolySupport.affineMinimizerMap {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) : V →L[ℝ] V

The affine stationary point x + k(x) in the affine space x + K.

Equations

• HCPolySupport.affineMinimizerMap K B hB = ContinuousLinearMap.id ℝ V + (↑K).subtypeL ∘SL HCPolySupport.correctionMap K B hB

@[simp]

theorem HCPolySupport.affineMinimizerMap_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (x : V) : (affineMinimizerMap K B hB) x = x + ↑((correctionMap K B hB) x)

theorem HCPolySupport.sub_affineMinimizerMap_apply_mem {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (x : V) : (affineMinimizerMap K B hB) x - x ∈ K

theorem HCPolySupport.affineMinimizerMap_firstVariation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (x : V) (w : ↥↑K) : (B ((affineMinimizerMap K B hB) x)) ↑w = 0

theorem HCPolySupport.affineMinimizerMap_minimizes_quadraticEnergy {V : Type u_1} [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 y : V) (hy : y - x ∈ K) : quadraticEnergy B ((affineMinimizerMap K B hB) x) ≤ quadraticEnergy B y

theorem HCPolySupport.eq_affineMinimizerMap_of_quadraticEnergy_le {V : Type u_1} [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 y : V) (hy : y - x ∈ K) (hle : quadraticEnergy B y ≤ quadraticEnergy B ((affineMinimizerMap K B hB) x)) : y = (affineMinimizerMap K B hB) x

The affine minimizer is the unique point in the affine subspace whose quadratic energy is no larger than the canonical minimized energy.

theorem HCPolySupport.quadraticEnergy_eq_affineMinimizerMap_add_diff {V : Type u_1} [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 y : V) (hy : y - x ∈ K) : quadraticEnergy B y = quadraticEnergy B ((affineMinimizerMap K B hB) x) + quadraticEnergy B (y - (affineMinimizerMap K B hB) x)

The quadratic energy splits into the minimized affine energy plus the energy of the displacement from the affine minimizer.

theorem HCPolySupport.tendsto_galerkin_of_quadraticEnergy_le_approximants {V : Type u_1} [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) {u v : ℕ → V} (hu_mem : ∀ (n : ℕ), u n - x ∈ K) (hv_mem : ∀ (n : ℕ), v n - x ∈ K) (hEnergy : ∀ (n : ℕ), quadraticEnergy B (u n) ≤ quadraticEnergy B (v n)) (hv : Filter.Tendsto v Filter.atTop (nhds ((affineMinimizerMap K B hB) x))) : Filter.Tendsto u Filter.atTop (nhds ((affineMinimizerMap K B hB) x))

Deterministic Galerkin/Cea convergence: if approximate minimizers in the affine space have energy no larger than admissible comparison points converging to the true Hilbert minimizer, then the approximate minimizers converge to the true minimizer.

theorem HCPolySupport.tendsto_of_quadraticEnergy_le_min_add_eps {V : Type u_1} [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) {u : ℕ → V} {ε : ℕ → ℝ} (hu_mem : ∀ (n : ℕ), u n - x ∈ K) (hε_tendsto : Filter.Tendsto ε Filter.atTop (nhds 0)) (hEnergy : ∀ (n : ℕ), quadraticEnergy B (u n) ≤ quadraticEnergy B ((affineMinimizerMap K B hB) x) + ε n) : Filter.Tendsto u Filter.atTop (nhds ((affineMinimizerMap K B hB) x))

Deterministic convergence from near-minimal energy. If points in the affine correction space have quadratic energy within ε n of the selected Hilbert minimizer and ε n → 0, then the points converge to that minimizer.

noncomputable def HCPolySupport.parameterAffineMinimizerMap {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (ι : E →L[ℝ] V) : E →L[ℝ] V

The affine minimizer map pulled back along a continuous linear parameter map.

Equations

• HCPolySupport.parameterAffineMinimizerMap K B hB ι = HCPolySupport.affineMinimizerMap K B hB ∘SL ι

@[simp]

theorem HCPolySupport.parameterAffineMinimizerMap_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (ι : E →L[ℝ] V) (p : E) : (parameterAffineMinimizerMap K B hB ι) p = (affineMinimizerMap K B hB) (ι p)

theorem HCPolySupport.sub_parameterAffineMinimizerMap_apply_mem {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (ι : E →L[ℝ] V) (p : E) : (parameterAffineMinimizerMap K B hB ι) p - ι p ∈ K

theorem HCPolySupport.parameterAffineMinimizerMap_firstVariation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ClosedSubmodule ℝ V) (B : V →L[ℝ] V →L[ℝ] ℝ) (hB : IsCoercive B) (ι : E →L[ℝ] V) (p : E) (w : ↥↑K) : (B ((parameterAffineMinimizerMap K B hB ι) p)) ↑w = 0

theorem HCPolySupport.parameterAffineMinimizerMap_minimizes_quadraticEnergy {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [CompleteSpace V] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] (K : ClosedSubmodule ℝ V) {B : V →L[ℝ] V →L[ℝ] ℝ} (hB : IsCoercive B) (h_symm : ∀ (u v : V), (B u) v = (B v) u) (ι : E →L[ℝ] V) (p : E) (y : V) (hy : y - ι p ∈ K) : quadraticEnergy B ((parameterAffineMinimizerMap K B hB ι) p) ≤ quadraticEnergy B y