ZeroExtension

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: extension by zero across an inclusion of domains

This file supplies the analytic ingredient needed to glue competitors in the variational subadditivity argument of ABK26, l.subadd.betterer: if V ⊆ U then the extension by zero of an element of H¹₀(V) is an element of H¹₀(U), hence

• L²_{pot,0}(V) ∋ f ↦ 1_V f ∈ L²_{pot,0}(U), and
• L²_{sol,0}(V) ∋ g ↦ 1_V g ∈ L²_{sol,0}(U).

The L²_{pot,0} half is the substantial one: the approximating sequence of an H¹₀(V) element consists of smooth functions with tsupport ⊆ V ⊆ U, so it is also an admissible approximating sequence in U, and CoarseGraining's L²-closedness of weak gradients (HasWeakGradientOn.of_tendsto_eLpNorm_two) identifies the weak gradient of the extension as the extension of the weak gradient. The L²_{sol,0} half is elementary: an H¹(U) test function restricts to an H¹(V) test function with the same gradient.

Everything is stated for CoarseGraining's a.e.-robust Chapter 1 predicates Homogenization.Book.Ch01.PotentialZeroTraceFieldOn and Homogenization.Book.Ch01.SolenoidalZeroNormalTraceFieldOn, which are the ones appearing in Homogenization.Book.Ch02.IsDoubledMuAdmissible.

L² bookkeeping for functions supported in a subset

theorem Algsuperdiff.Section3.Provider.Whitney.eLpNorm_two_restrict_eq_of_zero_outside {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (hVU : V ⊆ U) {h : HCPolySupport.Vec d → ℝ} (hzero : ∀ x ∉ V, h x = 0) : MeasureTheory.eLpNorm h 2 (MeasureTheory.volume.restrict U) = MeasureTheory.eLpNorm h 2 (MeasureTheory.volume.restrict V)

A function vanishing off V ⊆ U has the same L² norm over U and over V.

theorem Algsuperdiff.Section3.Provider.Whitney.memL2On_indicator_of_subset {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (hVU : V ⊆ U) {h : HCPolySupport.Vec d → ℝ} (hh : HCPolySupport.MemL2On V h) : HCPolySupport.MemL2On U (V.indicator h)

Extension by zero preserves scalar L² membership across an inclusion.

theorem Algsuperdiff.Section3.Provider.Whitney.memVectorL2_indicator_of_subset {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hV : MeasurableSet V) (hVU : V ⊆ U) {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.MemVectorL2 V f) : HCPolySupport.MemVectorL2 U (V.indicator f)

Extension by zero preserves vector L² membership across an inclusion.

theorem Algsuperdiff.Section3.Provider.Whitney.indicator_apply_coord {d : ℕ} (V : Set (HCPolySupport.Vec d)) (f : HCPolySupport.Vec d → HCPolySupport.Vec d) (i : Fin d) (x : HCPolySupport.Vec d) : V.indicator f x i = V.indicator (fun (y : HCPolySupport.Vec d) => f y i) x

Coordinates of a vector indicator are indicators of the coordinates.

Extension by zero of H¹₀

noncomputable def Algsuperdiff.Section3.Provider.Whitney.extendZeroH10 {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hV : MeasurableSet V) (hVU : V ⊆ U) (u : HCPolySupport.H10Function V) : HCPolySupport.H10Function U

Extension by zero of an H¹₀ function across an inclusion. For V ⊆ U with V measurable and U open, the function 1_V u, with gradient 1_V ∇u, belongs to H¹₀(U).

Equations

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

@[simp]

theorem Algsuperdiff.Section3.Provider.Whitney.extendZeroH10_grad {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hV : MeasurableSet V) (hVU : V ⊆ U) (u : HCPolySupport.H10Function V) : (extendZeroH10 hU hV hVU u).grad = V.indicator u.grad

Extension by zero of the Chapter 1 field spaces

theorem Algsuperdiff.Section3.Provider.Whitney.potentialZeroTraceFieldOn_indicator_of_subset {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hU : IsOpen U) (hV : MeasurableSet V) (hVU : V ⊆ U) {f : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn V f) : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U (V.indicator f)

Extension by zero maps L²_{pot,0}(V) into L²_{pot,0}(U) for V ⊆ U.

theorem Algsuperdiff.Section3.Provider.Whitney.solenoidalZeroNormalTraceFieldOn_indicator_of_subset {d : ℕ} {U V : Set (HCPolySupport.Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hg : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn V g) : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U (V.indicator g)

Extension by zero maps L²_{sol,0}(V) into L²_{sol,0}(U) for V ⊆ U.

Closure of the Chapter 1 field spaces under sums

theorem Algsuperdiff.Section3.Provider.Whitney.potentialZeroTraceFieldOn_add {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U f) (hg : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U g) : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U fun (x : HCPolySupport.Vec d) => f x + g x

theorem Algsuperdiff.Section3.Provider.Whitney.solenoidalZeroNormalTraceFieldOn_add {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hf : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U f) (hg : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U g) : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U fun (x : HCPolySupport.Vec d) => f x + g x

theorem Algsuperdiff.Section3.Provider.Whitney.potentialZeroTraceFieldOn_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U fun (x : HCPolySupport.Vec d) => 0

theorem Algsuperdiff.Section3.Provider.Whitney.solenoidalZeroNormalTraceFieldOn_zero {d : ℕ} {U : Set (HCPolySupport.Vec d)} : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U fun (x : HCPolySupport.Vec d) => 0

theorem Algsuperdiff.Section3.Provider.Whitney.potentialZeroTraceFieldOn_sum {d : ℕ} {ι : Type} (s : Finset ι) {U : Set (HCPolySupport.Vec d)} (F : ι → HCPolySupport.Vec d → HCPolySupport.Vec d) (h : ∀ i ∈ s, HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U (F i)) : HCPolySupport.Book.Ch01.PotentialZeroTraceFieldOn U fun (x : HCPolySupport.Vec d) => ∑ i ∈ s, F i x

theorem Algsuperdiff.Section3.Provider.Whitney.solenoidalZeroNormalTraceFieldOn_sum {d : ℕ} {ι : Type} (s : Finset ι) {U : Set (HCPolySupport.Vec d)} (F : ι → HCPolySupport.Vec d → HCPolySupport.Vec d) (h : ∀ i ∈ s, HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U (F i)) : HCPolySupport.Book.Ch01.SolenoidalZeroNormalTraceFieldOn U fun (x : HCPolySupport.Vec d) => ∑ i ∈ s, F i x