Coarse-graining support: Support.Sobolev.PotentialSolenoidalL2Recovery

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

This file adds a representative-level recovery interface for the abstract Hilbert correction space \Lpoto(U) × \Lsolo(U).

MuCorrectionSpaceData packages the correction space as a closed Hilbert subspace of L²(U; \R^{2d}), which is the right level for minimization. The results downstream that recover the note-faithful pointwise minimizers need a converse interface: a way to choose actual potential/solenoidal vector fields representing abstract elements of that closed subspace.

structure HCPolySupport.CorrectionFieldData {d : ℕ} (U : Set (Vec d)) : Type

A pointwise representative of an element of \Lpoto(U) × \Lsolo(U).

• potential : Vec d → Vec d

  The potential component.

• flux : Vec d → Vec d

  The solenoidal component.

• potential_memL2 : MemVectorL2 U self.potential

  L² control of the potential component.

• flux_memL2 : MemVectorL2 U self.flux

  L² control of the solenoidal component.

• isPotentialZeroTrace : IsPotentialZeroTraceOn U self.potential

  Zero-trace potential witness.

• isSolenoidalZeroNormalTrace : IsSolenoidalZeroNormalTraceOn U self.flux

  Zero-normal-trace solenoidal witness.

theorem HCPolySupport.CorrectionFieldData.memScalarL2_coord_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (i : Fin d) : MemScalarL2 U fun (x : Vec d) => f x i

theorem HCPolySupport.CorrectionFieldData.integrableOn_coord_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {f : Vec d → Vec d} (hf : MemVectorL2 U f) (i : Fin d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => f x i) U MeasureTheory.volume

theorem HCPolySupport.CorrectionFieldData.integrableOn_vecDot_const_left_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (p : Vec d) {f : Vec d → Vec d} (hf : MemVectorL2 U f) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot p (f x)) U MeasureTheory.volume

theorem HCPolySupport.CorrectionFieldData.integrableOn_vecDot_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (f x) (g x)) U MeasureTheory.volume

theorem HCPolySupport.CorrectionFieldData.integral_vecDot_const_left_eq_zero_of_integral_eq_zero_coords {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (p : Vec d) {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hzero : (fun (i : Fin d) => ∫ (x : Vec d) in U, f x i) = 0) : ∫ (x : Vec d) in U, vecDot p (f x) = 0

def HCPolySupport.CorrectionFieldData.toBlockField {d : ℕ} {U : Set (Vec d)} (X : CorrectionFieldData U) : Vec d → BlockVec d

The block-valued field represented by the two components.

Equations

• X.toBlockField = HCPolySupport.blockField X.potential X.flux

@[simp]

theorem HCPolySupport.CorrectionFieldData.toBlockField_fst {d : ℕ} {U : Set (Vec d)} (X : CorrectionFieldData U) (x : Vec d) : (X.toBlockField x).1 = X.potential x

@[simp]

theorem HCPolySupport.CorrectionFieldData.toBlockField_snd {d : ℕ} {U : Set (Vec d)} (X : CorrectionFieldData U) (x : Vec d) : (X.toBlockField x).2 = X.flux x

theorem HCPolySupport.CorrectionFieldData.memBlockL2_toBlockField {d : ℕ} {U : Set (Vec d)} (X : CorrectionFieldData U) : MemBlockL2 U X.toBlockField

The represented block field is in L²(U; \R^{2d}).

noncomputable def HCPolySupport.CorrectionFieldData.toBlockL2 {d : ℕ} {U : Set (Vec d)} (X : CorrectionFieldData U) : ↥(BlockL2 U)

The represented correction field as an element of the plain block ambient space.

Equations

• X.toBlockL2 = HCPolySupport.toBlockL2 ⋯

theorem HCPolySupport.CorrectionFieldData.coeFn_toBlockL2 {d : ℕ} {U : Set (Vec d)} (X : CorrectionFieldData U) : ↑↑X.toBlockL2 =ᵐ[volumeMeasureOn U] X.toBlockField

The plain block L² representative agrees almost everywhere with the pointwise block field.

noncomputable def HCPolySupport.CorrectionFieldData.toHilbertBlockL2 {d : ℕ} {U : Set (Vec d)} (X : CorrectionFieldData U) : ↥(HilbertBlockL2 U)

The represented correction field as an element of the Hilbert ambient space.

Equations

• X.toHilbertBlockL2 = HCPolySupport.toHilbertBlockL2OfComponents ⋯ ⋯

theorem HCPolySupport.CorrectionFieldData.coeFn_toHilbertBlockL2 {d : ℕ} {U : Set (Vec d)} (X : CorrectionFieldData U) : ↑↑X.toHilbertBlockL2 =ᵐ[volumeMeasureOn U] hilbertBlockField X.potential X.flux

theorem HCPolySupport.CorrectionFieldData.blockL2ToHilbertBlockL2_toBlockL2 {d : ℕ} {U : Set (Vec d)} (X : CorrectionFieldData U) : blockL2ToHilbertBlockL2 X.toBlockL2 = X.toHilbertBlockL2

theorem HCPolySupport.CorrectionFieldData.integrableOn_pairing_affine {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (X : CorrectionFieldData U) (p q : Vec d) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (p + X.potential x) (q + X.flux x)) U MeasureTheory.volume

theorem HCPolySupport.CorrectionFieldData.integral_pairing_affine_eq_volume_mul_vecDot_of_integral_eq_zero {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (X : CorrectionFieldData U) (p q : Vec d) (hpotZero : (fun (i : Fin d) => ∫ (x : Vec d) in U, X.potential x i) = 0) (hfluxZero : (fun (i : Fin d) => ∫ (x : Vec d) in U, X.flux x i) = 0) : ∫ (x : Vec d) in U, vecDot (p + X.potential x) (q + X.flux x) = (MeasureTheory.volume U).toReal * vecDot p q

noncomputable def HCPolySupport.blockFstCLM {d : ℕ} {U : Set (Vec d)} : ↥(BlockL2 U) →L[ℝ] ↥(VectorL2 U)

The continuous linear projection of a block L² field onto its first vector component.

Equations

• HCPolySupport.blockFstCLM = ContinuousLinearMap.compLpL 2 (HCPolySupport.volumeMeasureOn U) (ContinuousLinearMap.fst ℝ (HCPolySupport.Vec d) (HCPolySupport.Vec d))

noncomputable def HCPolySupport.blockSndCLM {d : ℕ} {U : Set (Vec d)} : ↥(BlockL2 U) →L[ℝ] ↥(VectorL2 U)

The continuous linear projection of a block L² field onto its second vector component.

Equations

• HCPolySupport.blockSndCLM = ContinuousLinearMap.compLpL 2 (HCPolySupport.volumeMeasureOn U) (ContinuousLinearMap.snd ℝ (HCPolySupport.Vec d) (HCPolySupport.Vec d))

theorem HCPolySupport.PotentialSolenoidalL2Data.potentialZeroTrace_mem_of_blockZeroTraceSolenoidal {d : ℕ} {U : Set (Vec d)} (X : ↥(BlockL2 U)) (hX : X ∈ (ofSubmoduleClosures U).blockPotentialZeroTraceSolenoidalZeroNormalTrace) : blockFstCLM X ∈ (ofSubmoduleClosures U).potentialZeroTrace

theorem HCPolySupport.PotentialSolenoidalL2Data.mem_solenoidalZeroNormalTrace_of_submoduleClosure {d : ℕ} {U : Set (Vec d)} (X : ↥(BlockL2 U)) (hX : X ∈ (ofSubmoduleClosures U).blockPotentialZeroTraceSolenoidalZeroNormalTrace) : blockSndCLM X ∈ (ofSubmoduleClosures U).solenoidalZeroNormalTrace

def HCPolySupport.correctionFieldSubmodule {d : ℕ} (U : Set (Vec d)) : Submodule ℝ (Vec d → BlockVec d)

The pointwise block correction fields with exact zero-trace / zero-normal-trace admissibility. This is the ambient vector space used to choose linear representatives of the closed L² correction space.

Equations

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

theorem HCPolySupport.correctionFieldSubmodule.mem_potential_memVectorL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : F ∈ correctionFieldSubmodule U) : MemVectorL2 U fun (x : Vec d) => (F x).1

theorem HCPolySupport.correctionFieldSubmodule.mem_flux_memVectorL2 {d : ℕ} {U : Set (Vec d)} {F : Vec d → BlockVec d} (hF : F ∈ correctionFieldSubmodule U) : MemVectorL2 U fun (x : Vec d) => (F x).2

noncomputable def HCPolySupport.correctionFieldSubmodule.toCorrectionFieldData {d : ℕ} {U : Set (Vec d)} (F : ↥(correctionFieldSubmodule U)) : CorrectionFieldData U

Convert an exact pointwise block correction field into bundled CorrectionFieldData.

Equations

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

@[simp]

theorem HCPolySupport.correctionFieldSubmodule.toCorrectionFieldData_toBlockField {d : ℕ} {U : Set (Vec d)} (F : ↥(correctionFieldSubmodule U)) : (toCorrectionFieldData F).toBlockField = ↑F

noncomputable def HCPolySupport.PotentialSolenoidalL2RecoveryData.correctionFieldSubmoduleToBlockSubmodule {d : ℕ} {U : Set (Vec d)} : ↥(correctionFieldSubmodule U) →ₗ[ℝ] ↥↑(PotentialSolenoidalL2Data.ofSubmoduleClosures U).blockPotentialZeroTraceSolenoidalZeroNormalTrace

The natural quotient map from exact pointwise correction fields to the canonical closed block correction space.

Equations

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

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.correctionToBlock_surjective_of_traceClosure {d : ℕ} {U : Set (Vec d)} (hRealize : PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization U) : Function.Surjective ⇑correctionFieldSubmoduleToBlockSubmodule

theorem HCPolySupport.memVectorL2_const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (p : Vec d) : MemVectorL2 U fun (x : Vec d) => p

theorem HCPolySupport.IsSolenoidalOn.of_test_of_contDiff_of_memVectorL2 {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : MemVectorL2 U g) (hU : IsOpen U) (htest : ∀ (ψ : Vec d → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → tsupport ψ ⊆ U → (∫ (x : Vec d) in U, vecDot (g x) fun (i : Fin d) => (fderiv ℝ ψ x) (basisVec i)) = 0) : IsSolenoidalOn U g

theorem HCPolySupport.IsSolenoidalOn.restrict_of_isOpen_of_memVectorL2 {d : ℕ} {U V : Set (Vec d)} {g : Vec d → Vec d} (hg : IsSolenoidalOn U g) (hU : IsOpen U) (hV : IsOpen V) (hVU : V ⊆ U) (hgV : MemVectorL2 V g) : IsSolenoidalOn V g

structure HCPolySupport.MuCorrectionSpaceRecoveryData {d : ℕ} (U : Set (Vec d)) extends HCPolySupport.MuCorrectionSpaceData U : Type

Recovery data for the abstract Hilbert correction space \Lpoto(U) × \Lsolo(U).

This extends MuCorrectionSpaceData by choosing pointwise representatives of all abstract correction fields, together with the linearity and realization statements needed later for minimizer recovery.

• correctionSpace : ClosedSubmodule ℝ ↥(HilbertBlockL2 U)
• mem_correctionSpace {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : IsPotentialZeroTraceOn U f → IsSolenoidalZeroNormalTraceOn U g → toHilbertBlockL2OfComponents hf hg ∈ self.correctionSpace
• repr : ↥↑self.correctionSpace → CorrectionFieldData U

  A pointwise representative of each abstract correction field.

• repr_add (X Y : ↥↑self.correctionSpace) : (self.repr (X + Y)).toBlockField = (self.repr X).toBlockField + (self.repr Y).toBlockField

  Additivity of the chosen representatives at the level of block fields.

• repr_smul (c : ℝ) (X : ↥↑self.correctionSpace) : (self.repr (c • X)).toBlockField = c • (self.repr X).toBlockField

  Homogeneity of the chosen representatives at the level of block fields.

• repr_eq (X : ↥↑self.correctionSpace) : (self.repr X).toHilbertBlockL2 = ↑X

  The chosen representative realizes the abstract correction field in the Hilbert ambient space.

structure HCPolySupport.PotentialSolenoidalL2RecoveryData {d : ℕ} (U : Set (Vec d)) extends HCPolySupport.PotentialSolenoidalL2Data U : Type

Representative-level recovery data on the plain block ambient space BlockL²(U), anchored to the packaged block correction space \Lpoto(U) × \Lsolo(U).

• potential : ClosedSubmodule ℝ ↥(VectorL2 U)
• potentialZeroTrace : ClosedSubmodule ℝ ↥(VectorL2 U)
• solenoidal : ClosedSubmodule ℝ ↥(VectorL2 U)
• solenoidalZeroNormalTrace : ClosedSubmodule ℝ ↥(VectorL2 U)
• blockPotentialSolenoidal : ClosedSubmodule ℝ ↥(BlockL2 U)
• blockPotentialZeroTraceSolenoidalZeroNormalTrace : ClosedSubmodule ℝ ↥(BlockL2 U)
• mem_potential {f : Vec d → Vec d} (hf : MemVectorL2 U f) : IsPotentialOn U f → toVectorL2 hf ∈ self.potential
• mem_potentialZeroTrace {f : Vec d → Vec d} (hf : MemVectorL2 U f) : IsPotentialZeroTraceOn U f → toVectorL2 hf ∈ self.potentialZeroTrace
• mem_solenoidal {g : Vec d → Vec d} (hg : MemVectorL2 U g) : IsSolenoidalOn U g → toVectorL2 hg ∈ self.solenoidal
• mem_solenoidalZeroNormalTrace {g : Vec d → Vec d} (hg : MemVectorL2 U g) : IsSolenoidalZeroNormalTraceOn U g → toVectorL2 hg ∈ self.solenoidalZeroNormalTrace
• mem_blockPotentialSolenoidal {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : IsPotentialOn U f → IsSolenoidalOn U g → toBlockL2OfComponents hf hg ∈ self.blockPotentialSolenoidal
• mem_blockPotentialZeroTraceSolenoidalZeroNormalTrace {f g : Vec d → Vec d} (hf : MemVectorL2 U f) (hg : MemVectorL2 U g) : IsPotentialZeroTraceOn U f → IsSolenoidalZeroNormalTraceOn U g → toBlockL2OfComponents hf hg ∈ self.blockPotentialZeroTraceSolenoidalZeroNormalTrace
• potentialZeroTrace_le_potential : self.potentialZeroTrace ≤ self.potential
• solenoidalZeroNormalTrace_le_solenoidal : self.solenoidalZeroNormalTrace ≤ self.solenoidal
• blockPotentialZeroTraceSolenoidalZeroNormalTrace_le_blockPotentialSolenoidal : self.blockPotentialZeroTraceSolenoidalZeroNormalTrace ≤ self.blockPotentialSolenoidal
• repr : ↥↑self.blockPotentialZeroTraceSolenoidalZeroNormalTrace → CorrectionFieldData U

  A pointwise representative of each block correction field.

• repr_add (X Y : ↥↑self.blockPotentialZeroTraceSolenoidalZeroNormalTrace) : (self.repr (X + Y)).toBlockField = (self.repr X).toBlockField + (self.repr Y).toBlockField

  Additivity of the chosen representatives at the level of block fields.

• repr_smul (c : ℝ) (X : ↥↑self.blockPotentialZeroTraceSolenoidalZeroNormalTrace) : (self.repr (c • X)).toBlockField = c • (self.repr X).toBlockField

  Homogeneity of the chosen representatives at the level of block fields.

• repr_eq (X : ↥↑self.blockPotentialZeroTraceSolenoidalZeroNormalTrace) : (self.repr X).toBlockL2 = ↑X

  The chosen representative realizes the abstract block correction field in BlockL²(U).

noncomputable def HCPolySupport.PotentialSolenoidalL2RecoveryData.toBlockCorrectionSubmodule {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2RecoveryData U) : ↥↑M.toMuCorrectionSpaceData.correctionSpace → ↥↑M.blockPotentialZeroTraceSolenoidalZeroNormalTrace

View a Hilbert-block correction field in the transported correction space as the corresponding element of the original block correction subspace.

Equations

• M.toBlockCorrectionSubmodule X = ⟨HCPolySupport.hilbertBlockL2ToBlockL2 ↑X, ⋯⟩

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.toBlockCorrectionSubmodule_add {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2RecoveryData U) (X Y : ↥↑M.toMuCorrectionSpaceData.correctionSpace) : M.toBlockCorrectionSubmodule (X + Y) = M.toBlockCorrectionSubmodule X + M.toBlockCorrectionSubmodule Y

theorem HCPolySupport.PotentialSolenoidalL2RecoveryData.toBlockCorrectionSubmodule_smul {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2RecoveryData U) (c : ℝ) (X : ↥↑M.toMuCorrectionSpaceData.correctionSpace) : M.toBlockCorrectionSubmodule (c • X) = c • M.toBlockCorrectionSubmodule X

noncomputable def HCPolySupport.PotentialSolenoidalL2RecoveryData.toMuCorrectionSpaceRecoveryData {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2RecoveryData U) : MuCorrectionSpaceRecoveryData U

Lift block-side recovery data to the Hilbert correction space used by the doubled μ minimization problem.

Equations

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

noncomputable def HCPolySupport.potentialSolenoidalL2RecoveryDataOfClosureRealization {d : ℕ} {U : Set (Vec d)} (hRealize : PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization U) : PotentialSolenoidalL2RecoveryData U

Canonical representative-level recovery data obtained from the closed predicate-generated block correction space, assuming the zero-trace potential closure has honest H¹₀ representatives.

Equations

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