Basic Lemmas

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem Homogenization.memL2On_mono {d : ℕ} {U V : Set (Vec d)} {u : Vec d → ℝ} (hVU : V ⊆ U) (hu : MemL2On U u) : MemL2On V u

theorem Homogenization.gradMemL2On_mono {d : ℕ} {U V : Set (Vec d)} {Du : Vec d → Vec d} (hVU : V ⊆ U) (hDu : GradMemL2On U Du) : GradMemL2On V Du

theorem Homogenization.memL2On_openCubeSet_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} {u : Vec d → ℝ} (hu : MemL2On (openCubeSet Q) u) : MeasureTheory.MemLp u 2 (normalizedCubeMeasure Q)

theorem Homogenization.HasWeakPartialDerivOn.restrict {d : ℕ} {U V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) {i : Fin d} {u gi : Vec d → ℝ} (h : HasWeakPartialDerivOn U i u gi) : HasWeakPartialDerivOn V i u gi

theorem Homogenization.HasWeakGradientOn.restrict {d : ℕ} {U V : Set (Vec d)} (hVopen : IsOpen V) (hVU : V ⊆ U) {u : Vec d → ℝ} {Du : Vec d → Vec d} (h : HasWeakGradientOn U u Du) : HasWeakGradientOn V u Du

theorem Homogenization.HasWeakPartialDerivOn.of_contDiff {d : ℕ} {U : Set (Vec d)} {i : Fin d} {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : HasWeakPartialDerivOn U i f fun (x : Vec d) => (fderiv ℝ f x) (basisVec i)

theorem Homogenization.HasWeakGradientOn.of_contDiff {d : ℕ} {U : Set (Vec d)} {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : HasWeakGradientOn U f fun (x : Vec d) (i : Fin d) => (fderiv ℝ f x) (basisVec i)

theorem Homogenization.H1Function.ext {d : ℕ} {U : Set (Vec d)} {u v : H1Function U} (htoFun : u.toFun = v.toFun) (hgrad : u.grad = v.grad) : u = v

theorem Homogenization.H1Function.ext_iff {d : ℕ} {U : Set (Vec d)} {u v : H1Function U} : u = v ↔ u.toFun = v.toFun ∧ u.grad = v.grad

theorem Homogenization.H1Function.hasWeakPartialDerivOn {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (i : Fin d) : HasWeakPartialDerivOn U i u.toFun fun (x : Vec d) => u.grad x i

theorem Homogenization.H1Function.grad_memL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) (i : Fin d) : MemL2On U fun (x : Vec d) => u.grad x i

theorem Homogenization.H1Function.grad_memVectorL2 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : MemVectorL2 U u.grad

theorem Homogenization.H1Function.memL2_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) : MeasureTheory.MemLp (fun (x : Vec d) => u.toFun x) 2 (normalizedCubeMeasure Q)

theorem Homogenization.H1Function.grad_memL2_normalizedCubeMeasure {d : ℕ} {Q : TriadicCube d} (u : H1Function (openCubeSet Q)) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => u.grad x i) 2 (normalizedCubeMeasure Q)

theorem Homogenization.H1Function.memH1 {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : MemH1 U u.toFun

noncomputable def Homogenization.H1Function.ofContDiff {d : ℕ} {U : Set (Vec d)} (_hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) (hf_supp : HasCompactSupport f) : H1Function U

Construct an H¹ function from a compactly supported C¹ function and its classical gradient.

Equations

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

noncomputable def Homogenization.H1Function.ofContDiffOnIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : H1Function U

Package a globally smooth function as an H¹(U) witness on a bounded measurable domain. Unlike ofContDiff, this constructor does not require compact support, because boundedness of U gives the needed L² control on the restriction.

Equations

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

noncomputable def Homogenization.H1Function.ofContDiffOnIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : H1Function U

Bounded open convex domains admit the bounded-domain smooth constructor for H¹.

Equations

• Homogenization.H1Function.ofContDiffOnIsOpenBoundedConvexDomain hU hf = Homogenization.H1Function.ofContDiffOnIsSobolevRegularDomain ⋯ hf

def Homogenization.H1Function.restrict {d : ℕ} {U V : Set (Vec d)} (u : H1Function U) (hVopen : IsOpen V) (hVU : V ⊆ U) : H1Function V

Restrict an H¹ function and its weak gradient to an open subdomain.

Equations

• u.restrict hVopen hVU = { toFun := u.toFun, grad := u.grad, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }

noncomputable def Homogenization.H1Function.restrictToOpenSubcube {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : H1Function (openCubeSet Q)) (hR : R ∈ descendantsAtDepth Q j) : H1Function (openCubeSet R)

Restrict an H¹ function to an open triadic descendant cube.

Equations

• u.restrictToOpenSubcube hR = u.restrict ⋯ ⋯

@[simp]

theorem Homogenization.H1Function.restrictToOpenSubcube_toFun {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : H1Function (openCubeSet Q)) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToOpenSubcube hR).toFun = u.toFun

@[simp]

theorem Homogenization.H1Function.restrictToOpenSubcube_grad {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : H1Function (openCubeSet Q)) (hR : R ∈ descendantsAtDepth Q j) : (u.restrictToOpenSubcube hR).grad = u.grad

theorem Homogenization.H1Function.grad_memL2_normalizedCubeMeasure_of_mem_descendantsAtDepth {d : ℕ} {Q R : TriadicCube d} {j : ℕ} (u : H1Function (openCubeSet Q)) (hR : R ∈ descendantsAtDepth Q j) (i : Fin d) : MeasureTheory.MemLp (fun (x : Vec d) => u.grad x i) 2 (normalizedCubeMeasure R)

theorem Homogenization.H10Function.memH1 {d : ℕ} {U : Set (Vec d)} (u : H10Function U) : MemH1 U u.toFun

noncomputable def Homogenization.H10Function.ofContDiff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (hf_sub : tsupport f ⊆ U) : H10Function U

Construct an H¹₀ function from a smooth function compactly supported inside the domain.

Equations

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

theorem Homogenization.memH1_of_memH10 {d : ℕ} {U : Set (Vec d)} {u : Vec d → ℝ} (hu : MemH10 U u) : MemH1 U u

theorem Homogenization.memH1_restrict {d : ℕ} {U V : Set (Vec d)} {u : Vec d → ℝ} (hVopen : IsOpen V) (hVU : V ⊆ U) (hu : MemH1 U u) : MemH1 V u

theorem Homogenization.H10Function.memH10 {d : ℕ} {U : Set (Vec d)} (u : H10Function U) : MemH10 U u.toFun

theorem Homogenization.memH10_of_contDiff {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {f : Vec d → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hf_supp : HasCompactSupport f) (hf_sub : tsupport f ⊆ U) : MemH10 U f

theorem Homogenization.memH1_of_contDiffOnIsSobolevRegularDomain {d : ℕ} {U : Set (Vec d)} (hU : IsSobolevRegularDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : MemH1 U f

theorem Homogenization.memH1_of_contDiffOnIsOpenBoundedConvexDomain {d : ℕ} {U : Set (Vec d)} (hU : IsOpenBoundedConvexDomain U) {f : Vec d → ℝ} (hf : ContDiff ℝ 1 f) : MemH1 U f