Coarse-graining support: Support.CoarseGraining.MuWellPosedness

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

This file records the Hilbert-space well-posedness package behind the doubled \mu problem.

The notes minimize a uniformly convex quadratic energy over the affine space P + \Lpoto(U) × \Lsolo(U) inside the Hilbert space L²(U; \R^{2d}). At the current stage of the formalization, we package that setup abstractly: an ambient real Hilbert space, a closed subspace modeling \mathcal{H}(U), a linear embedding of the parameter P ∈ \R^{2d}, and a coercive symmetric bilinear form.

This does not replace the note's definition of \mu(U,P;\a). It isolates the analytic theorem surface needed to turn the doubled minimization problem into a canonical linear minimizer map P ↦ X_P.

noncomputable def HCPolySupport.energyBilinOfOperator {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : H →L[ℝ] H) : H →L[ℝ] H →L[ℝ] ℝ

The bilinear form induced by a continuous operator on a real Hilbert space.

Equations

• HCPolySupport.energyBilinOfOperator T = innerSL ℝ ∘SL T

@[simp]

theorem HCPolySupport.energyBilinOfOperator_apply {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : H →L[ℝ] H) (X Y : H) : ((energyBilinOfOperator T) X) Y = inner ℝ (T X) Y

theorem HCPolySupport.energyBilinOfOperator_symm {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℝ H] (T : H →L[ℝ] H) (hT : (↑T).IsSymmetric) (X Y : H) : ((energyBilinOfOperator T) X) Y = ((energyBilinOfOperator T) Y) X

structure HCPolySupport.MuHilbertProblem {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Type (u_1 + 1)

Black-box Hilbert-space data for the doubled \mu problem on U.

The intended future instantiation is:

• ambient = L²(U; \R^{2d}) or an equivalent Hilbert realization;
• hilbertSubspace = \Lpoto(U) × \Lsolo(U);
• constantField P = the constant field with value P;
• energyBilin X Y = \fint_U X \cdot \mathbf{A}(\a) Y.

• ambient : Type u_1

  The ambient Hilbert space modeling L²(U; \R^{2d}).

• instNormedAddCommGroup : NormedAddCommGroup self.ambient
• instInnerProductSpace : InnerProductSpace ℝ self.ambient
• instCompleteSpace : CompleteSpace self.ambient
• hilbertSubspace : ClosedSubmodule ℝ self.ambient

  The closed subspace modeling \mathcal{H}(U) = \Lpoto(U) × \Lsolo(U).

• constantField : BlockVec d →L[ℝ] self.ambient

  The embedding of the parameter P ∈ \R^{2d} as a constant ambient field.

• energyBilin : self.ambient →L[ℝ] self.ambient →L[ℝ] ℝ

  The averaged doubled energy bilinear form.

• energySymm (X Y : self.ambient) : (self.energyBilin X) Y = (self.energyBilin Y) X

  Symmetry of the energy bilinear form.

• energyCoercive : IsCoercive self.energyBilin

  Coercivity of the energy bilinear form.

noncomputable def HCPolySupport.MuHilbertProblem.minimizerMap {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertProblem U a) : BlockVec d →L[ℝ] M.ambient

The canonical minimizer in the affine space P + \mathcal{H}(U).

Equations

• M.minimizerMap = HCPolySupport.parameterAffineMinimizerMap M.hilbertSubspace M.energyBilin ⋯ M.constantField

@[simp]

theorem HCPolySupport.MuHilbertProblem.minimizerMap_apply {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertProblem U a) (P : BlockVec d) : M.minimizerMap P = (affineMinimizerMap M.hilbertSubspace M.energyBilin ⋯) (M.constantField P)

theorem HCPolySupport.MuHilbertProblem.sub_minimizerMap_apply_mem {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertProblem U a) (P : BlockVec d) : M.minimizerMap P - M.constantField P ∈ M.hilbertSubspace

The correction from P to the minimizer lies in \mathcal{H}(U).

theorem HCPolySupport.MuHilbertProblem.minimizerMap_firstVariation {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertProblem U a) (P : BlockVec d) (Y : ↥↑M.hilbertSubspace) : (M.energyBilin (M.minimizerMap P)) ↑Y = 0

First variation of the minimized energy against all directions in \mathcal{H}(U).

noncomputable def HCPolySupport.MuHilbertProblem.muCandidate {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertProblem U a) (P : BlockVec d) : ℝ

The minimized quadratic energy attached to the Hilbert-space package.

Equations

• M.muCandidate P = HCPolySupport.quadraticEnergy M.energyBilin (M.minimizerMap P)

theorem HCPolySupport.MuHilbertProblem.muCandidate_le_quadraticEnergy {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertProblem U a) (P : BlockVec d) (X : M.ambient) (hX : X - M.constantField P ∈ M.hilbertSubspace) : M.muCandidate P ≤ quadraticEnergy M.energyBilin X

The canonical minimizer minimizes the quadratic energy over the whole affine space P + \mathcal{H}(U).

theorem HCPolySupport.MuHilbertProblem.eq_minimizerMap_of_quadraticEnergy_le_muCandidate {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertProblem U a) (P : BlockVec d) (X : M.ambient) (hX : X - M.constantField P ∈ M.hilbertSubspace) (hle : quadraticEnergy M.energyBilin X ≤ M.muCandidate P) : X = M.minimizerMap P

Uniqueness of the Hilbert minimizer in the affine correction space.

structure HCPolySupport.MuHilbertRealization {d : ℕ} (U : Set (Vec d)) (a : CoeffField d) : Type

A realization of the doubled \mu problem in the actual ambient Hilbert space L²(U; \R^{2d}).

This keeps the abstract minimization engine of MuHilbertProblem, but now the ambient type is fixed to the concrete Hilbert-valued L² space built in the Sobolev layer.

• correctionSpace : MuCorrectionSpaceData U

  The closed correction space \Lpoto(U) × \Lsolo(U) inside the concrete Hilbert ambient space.

• constantField : BlockVec d →L[ℝ] ↥(HilbertBlockL2 U)

  The constant field embedding of P ∈ \R^{2d} into L²(U; \R^{2d}).

• energyBilin : ↥(HilbertBlockL2 U) →L[ℝ] ↥(HilbertBlockL2 U) →L[ℝ] ℝ

  The averaged doubled energy bilinear form on the concrete ambient space.

• energySymm (X Y : ↥(HilbertBlockL2 U)) : (self.energyBilin X) Y = (self.energyBilin Y) X

  Symmetry of the energy bilinear form.

• energyCoercive : IsCoercive self.energyBilin

  Coercivity of the energy bilinear form.

noncomputable def HCPolySupport.MuHilbertRealization.ofOperator {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (correctionSpace : MuCorrectionSpaceData U) (operator : ↥(HilbertBlockL2 U) →L[ℝ] ↥(HilbertBlockL2 U)) (operatorSymm : (↑operator).IsSymmetric) (operatorCoercive : IsCoercive (energyBilinOfOperator operator)) : MuHilbertRealization U a

Package the doubled \mu problem from a symmetric coercive operator on the concrete Hilbert ambient space L²(U; \R^{2d}).

Equations

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

noncomputable def HCPolySupport.MuHilbertRealization.toProblem {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertRealization U a) : MuHilbertProblem U a

Forget the concrete ambient realization and view it as an abstract MuHilbertProblem.

Equations

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

noncomputable def HCPolySupport.MuHilbertRealization.minimizerMap {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertRealization U a) : BlockVec d →L[ℝ] ↥(HilbertBlockL2 U)

The canonical minimizer map in the actual ambient Hilbert space L²(U; \R^{2d}).

Equations

• M.minimizerMap = M.toProblem.minimizerMap

@[simp]

theorem HCPolySupport.MuHilbertRealization.minimizerMap_apply {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertRealization U a) (P : BlockVec d) : M.minimizerMap P = M.toProblem.minimizerMap P

theorem HCPolySupport.MuHilbertRealization.sub_minimizerMap_apply_mem {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertRealization U a) (P : BlockVec d) : M.minimizerMap P - M.constantField P ∈ M.correctionSpace.correctionSpace

The minimizer correction lies in the concrete correction space \Lpoto(U) × \Lsolo(U).

theorem HCPolySupport.MuHilbertRealization.minimizerMap_firstVariation {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertRealization U a) (P : BlockVec d) (Y : ↥↑M.correctionSpace.correctionSpace) : (M.energyBilin (M.minimizerMap P)) ↑Y = 0

First variation of the minimized energy against all concrete correction directions.

noncomputable def HCPolySupport.MuHilbertRealization.muCandidate {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertRealization U a) (P : BlockVec d) : ℝ

The minimized quadratic energy attached to the concrete Hilbert realization.

Equations

• M.muCandidate P = M.toProblem.muCandidate P

theorem HCPolySupport.MuHilbertRealization.muCandidate_le_quadraticEnergy {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertRealization U a) (P : BlockVec d) (X : ↥(HilbertBlockL2 U)) (hX : X - M.constantField P ∈ M.correctionSpace.correctionSpace) : M.muCandidate P ≤ quadraticEnergy M.energyBilin X

The canonical minimizer minimizes the quadratic energy over the concrete affine space P + \Lpoto(U) × \Lsolo(U).

theorem HCPolySupport.MuHilbertRealization.eq_minimizerMap_of_quadraticEnergy_le_muCandidate {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} (M : MuHilbertRealization U a) (P : BlockVec d) (X : ↥(HilbertBlockL2 U)) (hX : X - M.constantField P ∈ M.correctionSpace.correctionSpace) (hle : quadraticEnergy M.energyBilin X ≤ M.muCandidate P) : X = M.minimizerMap P

Uniqueness of the concrete Hilbert minimizer in the affine correction space.