Coarse-graining support: Support.Sobolev.Foundations.H10Graph

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

The H¹₀ graph inside the typed L² product

This file starts the closed-range bridge needed to remove the last Sobolev realization hypothesis from the coarse Poincare theorem surface.

The carrier is the graph of the map

u ↦ (u, ∇u) : H¹₀(U) → L²(U) × L²(U; ℝᵈ).

We immediately close this graph in the Hilbert product. The zero-trace Poincare estimate extends to that closed graph by a closed-set argument; this is the coercive ingredient needed for the eventual closed-range theorem for the gradient projection.

@[simp]

theorem HCPolySupport.H1Function.toScalarL2_zero {d : ℕ} {U : Set (Vec d)} : toScalarL2 0 = 0

@[simp]

theorem HCPolySupport.H1Function.gradToHilbertVectorL2_zero {d : ℕ} {U : Set (Vec d)} : gradToHilbertVectorL2 0 = 0

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

The graph of the typed H¹₀(U) realization inside L²(U) × L²(U; ℝᵈ).

Equations

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

theorem HCPolySupport.h10_pair_mem_h10GraphSubmodule {d : ℕ} {U : Set (Vec d)} (u : H10Function U) : (u.toScalarL2, u.gradToHilbertVectorL2) ∈ h10GraphSubmodule U

An H¹₀ function determines a point of the H¹₀ graph.

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

The closed H¹₀ graph in the typed Hilbert product.

Equations

• HCPolySupport.h10GraphClosedSubmodule U = (HCPolySupport.h10GraphSubmodule U).closure

theorem HCPolySupport.h10GraphSubmodule_le_h1GraphClosedSubmodule {d : ℕ} {U : Set (Vec d)} : h10GraphSubmodule U ≤ ↑h1GraphClosedSubmodule

The H¹₀ graph is contained in the weak H¹ graph.

theorem HCPolySupport.h10GraphClosedSubmodule_le_h1GraphClosedSubmodule {d : ℕ} {U : Set (Vec d)} : ↑(h10GraphClosedSubmodule U) ≤ ↑h1GraphClosedSubmodule

The closed H¹₀ graph stays inside the weak H¹ graph.

theorem HCPolySupport.h10GraphClosedSubmodule_norm_value_le_of_forall_h10 {d : ℕ} {U : Set (Vec d)} {C : ℝ} (hC : ∀ (u : H10Function U), ‖u.toScalarL2‖ ≤ C * ‖u.gradToHilbertVectorL2‖) {z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)} (hz : z ∈ h10GraphClosedSubmodule U) : ‖z.1‖ ≤ C * ‖z.2‖

If a Poincare estimate holds on honest H¹₀ functions, it extends to the closed H¹₀ graph.

theorem HCPolySupport.h10GraphClosedSubmodule_exists_norm_value_le_mul_norm_gradient {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsOpenBoundedConvexDomain U) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ z ∈ h10GraphClosedSubmodule U, ‖z.1‖ ≤ C * ‖z.2‖

On bounded open convex domains, the zero-trace Poincare estimate extends to the closed H¹₀ graph.

theorem HCPolySupport.h10GraphClosedSubmodule_norm_value_le_of_isOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsOpenBoundedConvexDomain U) {z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)} (hz : z ∈ h10GraphClosedSubmodule U) : ∃ (C : ℝ), 0 ≤ C ∧ ‖z.1‖ ≤ C * ‖z.2‖

Curried form of h10GraphClosedSubmodule_exists_norm_value_le_mul_norm_gradient.

@[reducible, inline]

noncomputable abbrev HCPolySupport.H10GraphClosedSpace {d : ℕ} (U : Set (Vec d)) : Type

The closed H¹₀ graph as a normed carrier.

Equations

• HCPolySupport.H10GraphClosedSpace U = ↥↑(HCPolySupport.h10GraphClosedSubmodule U)

Representative upgrade for the closed H¹₀ graph

The missing analytic ingredient for the potential-zero-trace realization theorem is that every point of the closed H¹₀ graph is the pair (u.toScalarL2, u.gradToHilbertVectorL2) for an actual H¹₀ function. The construction diagonalises the closure approximation sequence against each graph approximant's internal smooth compactly supported approximation data using the approxH1 packaging from CoerciveH10.

theorem HCPolySupport.exists_h10Function_of_mem_h10GraphClosedSubmodule {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {z : ↥(ScalarL2 U) × ↥(HilbertVectorL2 U)} (hz : z ∈ ↑(h10GraphClosedSubmodule U)) : ∃ (u : H10Function U), u.toScalarL2 = z.1 ∧ u.gradToHilbertVectorL2 = z.2

Every point of the closed H¹₀ graph is realized by an honest H¹₀ function on bounded open convex domains. The witness is obtained by diagonalising closure approximations against each graph approximant's internal smooth compactly supported approximation data.

instance HCPolySupport.H10GraphClosed.instCompleteSpaceH10GraphClosedSpace {d : ℕ} {U : Set (Vec d)} : CompleteSpace (H10GraphClosedSpace U)

@[reducible, inline]

abbrev HCPolySupport.H10GraphClosed.value {d : ℕ} {U : Set (Vec d)} (z : H10GraphClosedSpace U) : ↥(ScalarL2 U)

Scalar value component of a closed H¹₀ graph point.

Equations

• HCPolySupport.H10GraphClosed.value z = (↑z).1

@[reducible, inline]

abbrev HCPolySupport.H10GraphClosed.gradient {d : ℕ} {U : Set (Vec d)} (z : H10GraphClosedSpace U) : ↥(HilbertVectorL2 U)

Gradient component of a closed H¹₀ graph point.

Equations

• HCPolySupport.H10GraphClosed.gradient z = (↑z).2

noncomputable def HCPolySupport.H10GraphClosed.valueCLM {d : ℕ} {U : Set (Vec d)} : H10GraphClosedSpace U →L[ℝ] ↥(ScalarL2 U)

Continuous scalar-value projection from the closed H¹₀ graph.

Equations

• HCPolySupport.H10GraphClosed.valueCLM = ContinuousLinearMap.fst ℝ ↥(HCPolySupport.ScalarL2 U) ↥(HCPolySupport.HilbertVectorL2 U) ∘SL (↑(HCPolySupport.h10GraphClosedSubmodule U)).subtypeL

@[simp]

theorem HCPolySupport.H10GraphClosed.valueCLM_apply {d : ℕ} {U : Set (Vec d)} (z : H10GraphClosedSpace U) : valueCLM z = value z

noncomputable def HCPolySupport.H10GraphClosed.gradientCLM {d : ℕ} {U : Set (Vec d)} : H10GraphClosedSpace U →L[ℝ] ↥(HilbertVectorL2 U)

Continuous gradient projection from the closed H¹₀ graph.

Equations

• HCPolySupport.H10GraphClosed.gradientCLM = ContinuousLinearMap.snd ℝ ↥(HCPolySupport.ScalarL2 U) ↥(HCPolySupport.HilbertVectorL2 U) ∘SL (↑(HCPolySupport.h10GraphClosedSubmodule U)).subtypeL

@[simp]

theorem HCPolySupport.H10GraphClosed.gradientCLM_apply {d : ℕ} {U : Set (Vec d)} (z : H10GraphClosedSpace U) : gradientCLM z = gradient z

theorem HCPolySupport.H10GraphClosed.exists_norm_value_le_mul_norm_gradient {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsOpenBoundedConvexDomain U) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (z : H10GraphClosedSpace U), ‖value z‖ ≤ C * ‖gradient z‖

The zero-trace Poincare estimate on the closed graph, stated on the graph carrier.

theorem HCPolySupport.H10GraphClosed.exists_norm_le_mul_norm_gradient {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsOpenBoundedConvexDomain U) : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (z : H10GraphClosedSpace U), ‖z‖ ≤ M * ‖gradient z‖

The closed graph norm is controlled by the gradient norm on bounded open convex domains.

theorem HCPolySupport.H10GraphClosed.exists_antilipschitzWith_gradientCLM {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsOpenBoundedConvexDomain U) : ∃ (K : NNReal), AntilipschitzWith K ⇑gradientCLM

The gradient projection from the closed H¹₀ graph is anti-Lipschitz on bounded open convex domains.

theorem HCPolySupport.H10GraphClosed.isClosed_range_gradientCLM {d : ℕ} {U : Set (Vec d)} [NeZero d] (hU : IsOpenBoundedConvexDomain U) : IsClosed (Set.range ⇑gradientCLM)

The range of the gradient projection from the closed H¹₀ graph is closed.