High-contrast homogenization: Consistency.ConvexDilation

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

Dilation of a convex domain, and global smooth realization

This module checks the defining predicate MemH1a of H¹_a(V) of s.introduction, and its zero-trace variant MemH1a0. It checks the requirement in those classes that a member be approximated in the H¹_a norm by functions smooth on all of ℝ^d, where the paper's coefficient-weighted spaces are completions of C^∞(U), the functions smooth on U: a function smooth on U is carried, by dilation and a cutoff, to a globally smooth function agreeing with its dilate exactly on closure U, and exact agreement on an open set makes the two share their coordinate gradients.

Were that check to fail — were the homothety of closure U not to land in interior U, or the dilate not to have a globally smooth representative agreeing with it exactly on closure U with the same coordinate gradients — then the printed completions could not be represented by the globally smooth approximants that MemH1a demands; the predicate would encode a class smaller than the space the paper prints, and every statement that assumes a member of MemH1a, among them the estimates for weak solutions, would be vacuous precisely where the paper means it to apply. This module is a consistency check of that definition and is not a result of the paper.

The classical route between the two dilates the domain and then mollifies the function. This module supplies the dilation step and removes the need for the mollification.

The first section is the geometric core: for a convex U carrying an interior ball around c, the homothety x ↦ c + lam • (x - c) of ratio lam < 1 maps closure U into interior U, so a function smooth on U becomes, after dilation, smooth on an open set containing closure U. Neither boundedness nor openness of U is used; the interior ball is the only nondegeneracy input.

The second section replaces mollification. Because the dilate is smooth on an open neighbourhood of closure U, a smooth Urysohn cutoff turns it into a genuinely globally smooth function agreeing with it exactly on closure U, not merely approximately, and exact agreement on an open set transfers to the coordinate gradients.

One classical, coefficient-free statement is not settled here: that dilation is continuous at lam = 1 in L¹(U) × L²(U). Until it is available the membership classes used here are not known to agree with the printed completions, in either direction.

The convex dilation lemma

For a convex U carrying an interior ball around c, the homothety x ↦ c + lam • (x - c) of ratio lam < 1 centred at c pulls the whole closure strictly inside: its image lands in interior U. No boundedness of U and no openness of U is used; the interior ball is the only nondegeneracy input.

theorem HCPolySupport.HighContrast.contDiff_dilate {d : ℕ} (c : Vec d) (lam : ℝ) : ContDiff ℝ ↑⊤ fun (x : Vec d) => c + lam • (x - c)

The homothety of ratio lam centred at c is smooth.

theorem HCPolySupport.HighContrast.dilate_closure_subset_interior_of_convex {d : ℕ} {U : Set (Vec d)} (hconv : Convex ℝ U) {c : Vec d} {ρ : ℝ} (hρ : 0 < ρ) (hball : Metric.ball c ρ ⊆ U) {lam : ℝ} (hlam : lam ∈ Set.Ico 0 1) : (fun (x : Vec d) => c + lam • (x - c)) '' closure U ⊆ interior U

The convex dilation lemma. If U is convex and contains the ball of radius ρ > 0 about c, then for every ratio lam ∈ [0, 1) the homothety x ↦ c + lam • (x - c) maps closure U into interior U.

theorem HCPolySupport.HighContrast.smul_closure_subset_of_convex {d : ℕ} {U : Set (Vec d)} (hconv : Convex ℝ U) {c : Vec d} {ρ : ℝ} (hρ : 0 < ρ) (hball : Metric.ball c ρ ⊆ U) {lam : ℝ} (hlam : lam ∈ Set.Ico 0 1) : (fun (x : Vec d) => c + lam • (x - c)) '' closure U ⊆ U

The dilated closure lands in U itself.

def HCPolySupport.HighContrast.dilationDomain {d : ℕ} (c : Vec d) (lam : ℝ) (U : Set (Vec d)) : Set (Vec d)

The open set on which the dilated function inherits smoothness: the homothety preimage of interior U.

Equations

• HCPolySupport.HighContrast.dilationDomain c lam U = (fun (x : HCPolySupport.Vec d) => c + lam • (x - c)) ⁻¹' interior U

theorem HCPolySupport.HighContrast.isOpen_dilationDomain {d : ℕ} (c : Vec d) (lam : ℝ) (U : Set (Vec d)) : IsOpen (dilationDomain c lam U)

theorem HCPolySupport.HighContrast.closure_subset_dilationDomain {d : ℕ} {U : Set (Vec d)} (hconv : Convex ℝ U) {c : Vec d} {ρ : ℝ} (hρ : 0 < ρ) (hball : Metric.ball c ρ ⊆ U) {lam : ℝ} (hlam : lam ∈ Set.Ico 0 1) : closure U ⊆ dilationDomain c lam U

The dilation domain is a neighbourhood of the closure: this is the dilation lemma read as an inclusion of sets.

theorem HCPolySupport.HighContrast.contDiffOn_comp_dilate {d : ℕ} {U : Set (Vec d)} {c : Vec d} {lam : ℝ} {v : Vec d → ℝ} (hv : ContDiffOn ℝ (↑⊤) v U) : ContDiffOn ℝ (↑⊤) (fun (x : Vec d) => v (c + lam • (x - c))) (dilationDomain c lam U)

Smoothness of the dilate on a neighbourhood of the closure. A function smooth on U only becomes, after dilation, smooth on the open set dilationDomain c lam U, which by closure_subset_dilationDomain contains closure U.

theorem HCPolySupport.HighContrast.exists_isOpen_contDiffOn_comp_dilate {d : ℕ} {U : Set (Vec d)} (hconv : Convex ℝ U) {c : Vec d} {ρ : ℝ} (hρ : 0 < ρ) (hball : Metric.ball c ρ ⊆ U) {lam : ℝ} (hlam : lam ∈ Set.Ico 0 1) {v : Vec d → ℝ} (hv : ContDiffOn ℝ (↑⊤) v U) : ∃ (S : Set (Vec d)), IsOpen S ∧ closure U ⊆ S ∧ ContDiffOn ℝ (↑⊤) (fun (x : Vec d) => v (c + lam • (x - c))) S

The conclusion of this section: from smoothness on U alone one gets a genuine open neighbourhood of closure U on which the dilate is smooth.

The mollification step is unnecessary

The classical route to the density converse dilates and then mollifies, and mollification in L² is the expensive part: the ambient library carries no Lp-convergence statement for mollifiers. It is not needed here. Because the previous section delivers smoothness on an open set containing closure U, a smooth Urysohn cutoff turns the dilate into a genuinely globally smooth function that agrees with it exactly on closure U, not merely approximately. The cutoff is exists_contMDiffMap_zero_one_nhds_of_isClosed read through contMDiff_iff_contDiff for the model modelWithCornersSelf ℝ (Vec d).

theorem HCPolySupport.HighContrast.exists_contDiff_eqOn_of_contDiffOn_isOpen {d : ℕ} {S : Set (Vec d)} (hS : IsOpen S) {K : Set (Vec d)} (hK : IsClosed K) (hKS : K ⊆ S) {w : Vec d → ℝ} (hw : ContDiffOn ℝ (↑⊤) w S) : ∃ (g : Vec d → ℝ), ContDiff ℝ (↑⊤) g ∧ Set.EqOn g w K

Global smooth realization. A function smooth on an open S is realized exactly on any closed K ⊆ S by a function smooth on all of ℝ^d. This is the step that replaces mollification.

theorem HCPolySupport.HighContrast.exists_contDiff_eqOn_dilate_of_convex {d : ℕ} {U : Set (Vec d)} (hconv : Convex ℝ U) {c : Vec d} {ρ : ℝ} (hρ : 0 < ρ) (hball : Metric.ball c ρ ⊆ U) {lam : ℝ} (hlam : lam ∈ Set.Ico 0 1) {v : Vec d → ℝ} (hv : ContDiffOn ℝ (↑⊤) v U) : ∃ (g : Vec d → ℝ), ContDiff ℝ (↑⊤) g ∧ Set.EqOn g (fun (x : Vec d) => v (c + lam • (x - c))) (closure U)

The two sections combined. On a convex U with an interior ball, a function smooth on U alone has a dilate that is realized on all of closure U by a globally smooth function. No mollification, no Lp convergence, no approximation: the agreement is exact.

theorem HCPolySupport.HighContrast.smoothGrad_congr_of_eqOn_isOpen {d : ℕ} {S : Set (Vec d)} (hS : IsOpen S) {f g : Vec d → ℝ} (h : Set.EqOn f g S) {x : Vec d} (hx : x ∈ S) : smoothGrad f x = smoothGrad g x

Exact agreement on an open set transfers to the coordinate gradients, so the realization of the previous theorem has the same smoothGrad as the dilate throughout U. Both summands of h1sNormSqOn therefore see the globally smooth g and the dilate v ∘ T as the same object on U.