Coarse-graining support: Support.Sobolev.Foundations.H1Graph.Graph

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

noncomputable def HCPolySupport.h1WeakConstraintCLM {d : ℕ} {U : Set (Vec d)} (i : Fin d) (φ : H1WeakTestFunction U) : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U) →L[ℝ] ℝ

The weak-gradient constraint attached to a coordinate i and a smooth compactly supported test function φ. Its kernel consists of pairs (u, Du) ∈ L²(U) × L²(U; HilbertVec d) satisfying the corresponding integration-by-parts identity.

Equations

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

@[simp]

theorem HCPolySupport.h1WeakConstraintCLM_apply {d : ℕ} {U : Set (Vec d)} (i : Fin d) (φ : H1WeakTestFunction U) (z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)) : (h1WeakConstraintCLM i φ) z = inner ℝ z.1 (φ.derivToScalarL2 i) + inner ℝ ((hilbertVectorCoordToScalarL2 i) z.2) φ.toScalarL2

theorem HCPolySupport.h1WeakConstraintCLM_apply_eq_integral {d : ℕ} {U : Set (Vec d)} (i : Fin d) (φ : H1WeakTestFunction U) (z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)) : (h1WeakConstraintCLM i φ) z = (∫ (x : Vec d) in U, ↑↑z.1 x * φ.deriv i x) + ∫ (x : Vec d) in U, (↑↑z.2 x).ofLp i * φ.toFun x

noncomputable def HCPolySupport.h1GraphClosedSubmodule {d : ℕ} {U : Set (Vec d)} : ClosedSubmodule ℝ (↥(ScalarL2 U) × ↥(HilbertVectorL2 U))

The closed ambient subspace cut out by the weak-gradient constraints.

Equations

• HCPolySupport.h1GraphClosedSubmodule = ⨅ (i : Fin d), ⨅ (φ : HCPolySupport.H1WeakTestFunction U), ClosedSubmodule.comap (HCPolySupport.h1WeakConstraintCLM i φ) ⊥

theorem HCPolySupport.mem_h1GraphClosedSubmodule_iff {d : ℕ} {U : Set (Vec d)} (z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)) : z ∈ h1GraphClosedSubmodule ↔ ∀ (i : Fin d) (φ : H1WeakTestFunction U), (h1WeakConstraintCLM i φ) z = 0

theorem HCPolySupport.h1_pair_mem_h1GraphClosedSubmodule {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : (u.toScalarL2, u.gradToHilbertVectorL2) ∈ h1GraphClosedSubmodule

noncomputable def HCPolySupport.toH1FunctionOfMemH1Graph {d : ℕ} {U : Set (Vec d)} (z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)) (hz : z ∈ h1GraphClosedSubmodule) : H1Function U

Recover an H¹ witness from a point of the closed weak-gradient graph.

Equations

• HCPolySupport.toH1FunctionOfMemH1Graph z hz = { toFun := ↑↑z.1, grad := ↑↑(HCPolySupport.hilbertVectorL2ToVectorL2 z.2), memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }

theorem HCPolySupport.mem_h1GraphClosedSubmodule_iff_exists_h1Function {d : ℕ} {U : Set (Vec d)} (z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)) : z ∈ h1GraphClosedSubmodule ↔ ∃ (u : H1Function U), u.toScalarL2 = z.1 ∧ u.gradToHilbertVectorL2 = z.2

theorem HCPolySupport.exists_h1Function_of_toScalarL2_toHilbertVectorL2OfVecField_mem_h1GraphClosedSubmodule {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} {G : Vec d → Vec d} (hu : MemScalarL2 U u) (hG : MemVectorL2 U G) (hz : (toScalarL2 hu, toHilbertVectorL2OfVecField hG) ∈ h1GraphClosedSubmodule) : ∃ (w : H1Function U), w.toFun = u ∧ w.grad = G

Exact representative form of toH1FunctionOfMemH1Graph.

If explicit scalar/vector representatives define a point of the closed H¹ graph, then they themselves can be used as the toFun and grad fields of an H1Function. This avoids losing pointwise control to arbitrary Lp representatives.

theorem HCPolySupport.mem_h1GraphClosedSubmodule_of_tendsto_h1Function {d : ℕ} {U : Set (Vec d)} {ι : Type u_1} {l : Filter ι} [l.NeBot] (w : ι → H1Function U) {z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)} (hval : Filter.Tendsto (fun (n : ι) => (w n).toScalarL2) l (nhds z.1)) (hgrad : Filter.Tendsto (fun (n : ι) => (w n).gradToHilbertVectorL2) l (nhds z.2)) : z ∈ h1GraphClosedSubmodule

Closedness of the H¹ graph, stated as a sequential/filter handoff for honest H1Function approximants.

@[simp]

theorem HCPolySupport.toH1FunctionOfMemH1Graph_toScalarL2 {d : ℕ} {U : Set (Vec d)} (z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)) (hz : z ∈ h1GraphClosedSubmodule) : (toH1FunctionOfMemH1Graph z hz).toScalarL2 = z.1

@[simp]

theorem HCPolySupport.toH1FunctionOfMemH1Graph_gradToHilbertVectorL2 {d : ℕ} {U : Set (Vec d)} (z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)) (hz : z ∈ h1GraphClosedSubmodule) : (toH1FunctionOfMemH1Graph z hz).gradToHilbertVectorL2 = z.2

noncomputable def HCPolySupport.oneScalarL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ↥(ScalarL2 U)

The constant-one class in scalar L²(U).

Equations

• HCPolySupport.oneScalarL2 = HCPolySupport.toScalarL2 ⋯

@[simp]

theorem HCPolySupport.coeFn_oneScalarL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ↑↑oneScalarL2 =ᵐ[volumeMeasureOn U] fun (x : Vec d) => 1

noncomputable def HCPolySupport.scalarIntegralCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ↥(ScalarL2 U) →L[ℝ] ℝ

The scalar integral on L²(U) for finite-measure domains.

Equations

• HCPolySupport.scalarIntegralCLM = (InnerProductSpace.toDual ℝ ↥(HCPolySupport.ScalarL2 U)) HCPolySupport.oneScalarL2

@[simp]

theorem HCPolySupport.scalarIntegralCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (s : ↥(ScalarL2 U)) : scalarIntegralCLM s = ∫ (x : Vec d) in U, ↑↑s x

noncomputable def HCPolySupport.constScalarL2CLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ℝ →L[ℝ] ↥(ScalarL2 U)

The constant-value embedding ℝ → L²(U) attached to the constant-one class.

Equations

• HCPolySupport.constScalarL2CLM = ContinuousLinearMap.smulRight 1 HCPolySupport.oneScalarL2

@[simp]

theorem HCPolySupport.constScalarL2CLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (c : ℝ) : constScalarL2CLM c = c • oneScalarL2

noncomputable def HCPolySupport.integralAverageCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ↥(ScalarL2 U) →L[ℝ] ℝ

The average functional on scalar L²(U).

Equations

• HCPolySupport.integralAverageCLM = (MeasureTheory.volume U).toReal⁻¹ • HCPolySupport.scalarIntegralCLM

@[simp]

theorem HCPolySupport.integralAverageCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (s : ↥(ScalarL2 U)) : integralAverageCLM s = (MeasureTheory.volume U).toReal⁻¹ * ∫ (x : Vec d) in U, ↑↑s x

noncomputable def HCPolySupport.subAverageValueCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ↥(ScalarL2 U) →L[ℝ] ↥(ScalarL2 U)

The scalar-value operator that subtracts the average.

Equations

• HCPolySupport.subAverageValueCLM = ContinuousLinearMap.id ℝ ↥(HCPolySupport.ScalarL2 U) - HCPolySupport.integralAverageCLM.smulRight HCPolySupport.oneScalarL2

@[simp]

theorem HCPolySupport.subAverageValueCLM_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (s : ↥(ScalarL2 U)) : subAverageValueCLM s = s - integralAverageCLM s • oneScalarL2

@[simp]

theorem HCPolySupport.H1Function.toScalarL2_const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (c : ℝ) : (const c).toScalarL2 = c • oneScalarL2

theorem HCPolySupport.H1Function.integralAverage_eq_integralAverageCLM_toScalarL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : integralAverage U u.toFun = integralAverageCLM u.toScalarL2

theorem HCPolySupport.H1Function.toScalarL2_subAverage_eq_subAverageValueCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : u.subAverage.toScalarL2 = subAverageValueCLM u.toScalarL2

theorem HCPolySupport.H1Function.tendsto_integralAverage_of_tendsto_toScalarL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {α : Type u_1} {l : Filter α} {f : α → H1Function U} {u : H1Function U} (h : Filter.Tendsto (fun (a : α) => (f a).toScalarL2) l (nhds u.toScalarL2)) : Filter.Tendsto (fun (a : α) => integralAverage U (f a).toFun) l (nhds (integralAverage U u.toFun))

theorem HCPolySupport.H1Function.tendsto_toScalarL2_subAverage_of_tendsto_toScalarL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {α : Type u_1} {l : Filter α} {f : α → H1Function U} {u : H1Function U} (h : Filter.Tendsto (fun (a : α) => (f a).toScalarL2) l (nhds u.toScalarL2)) : Filter.Tendsto (fun (a : α) => (f a).subAverage.toScalarL2) l (nhds u.subAverage.toScalarL2)

@[simp]

theorem HCPolySupport.H1Function.gradCoordToScalarL2_subAverage_eq {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) (i : Fin d) : u.subAverage.gradCoordToScalarL2 i = u.gradCoordToScalarL2 i

@[simp]

theorem HCPolySupport.H1Function.gradientCoordL2NormSum_subAverage_eq {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1Function U) : u.subAverage.gradientCoordL2NormSum = u.gradientCoordL2NormSum

theorem HCPolySupport.H1Function.tendsto_gradientCoordL2NormSum_subAverage_of_tendsto_gradCoordToScalarL2 {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {α : Type u_1} {l : Filter α} {f : α → H1Function U} {u : H1Function U} (hgrad : ∀ (i : Fin d), Filter.Tendsto (fun (a : α) => (f a).gradCoordToScalarL2 i) l (nhds (u.gradCoordToScalarL2 i))) : Filter.Tendsto (fun (a : α) => (f a).subAverage.gradientCoordL2NormSum) l (nhds u.subAverage.gradientCoordL2NormSum)

noncomputable def HCPolySupport.h1MeanZeroGraphClosedSubmodule {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] : ClosedSubmodule ℝ (↥(ScalarL2 U) × ↥(HilbertVectorL2 U))

The closed mean-zero weak-gradient graph in L²(U) × L²(U; HilbertVec d).

Equations

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

theorem HCPolySupport.mem_h1MeanZeroGraphClosedSubmodule_iff {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)) : z ∈ h1MeanZeroGraphClosedSubmodule ↔ z ∈ h1GraphClosedSubmodule ∧ scalarIntegralCLM z.1 = 0

theorem HCPolySupport.h1MeanZero_pair_mem_h1MeanZeroGraphClosedSubmodule {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H1MeanZeroFunction U) : (u.toScalarL2, u.gradToHilbertVectorL2) ∈ h1MeanZeroGraphClosedSubmodule

theorem HCPolySupport.mem_h1MeanZeroGraphClosedSubmodule_iff_exists_h1MeanZeroFunction {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)) : z ∈ h1MeanZeroGraphClosedSubmodule ↔ ∃ (u : H1MeanZeroFunction U), u.toScalarL2 = z.1 ∧ u.gradToHilbertVectorL2 = z.2