Coarse-graining support: Support.Sobolev.H1.OriginCubeBridge

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

def HCPolySupport.diagonalShift {d : ℕ} (ε : ℝ) : Vec d

The vector whose every coordinate equals ε.

Equations

• HCPolySupport.diagonalShift ε x✝ = ε

theorem HCPolySupport.volume_cubeSet_originCube_lt_top {d : ℕ} (n : ℤ) : MeasureTheory.volume (cubeSet (originCube d n)) < ⊤

theorem HCPolySupport.volume_openCubeSet_originCube_lt_top_originCubeBridge {d : ℕ} (n : ℤ) : MeasureTheory.volume (openCubeSet (originCube d n)) < ⊤

theorem HCPolySupport.tendsto_setIntegral_mul_precomp_subRight_of_memL2On {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict U)] {f ψ : Vec d → ℝ} (hfL2 : MemL2On U f) (hψ_cont : Continuous ψ) (hψ_compact : HasCompactSupport ψ) (ε₀ : ℝ) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : Vec d) in U, f x * ψ (x - diagonalShift (ε₀ / (↑n + 2)))) Filter.atTop (nhds (∫ (x : Vec d) in U, f x * ψ x))

noncomputable def HCPolySupport.H1Function.toCubeSetOriginCube {d : ℕ} [NeZero d] {n : ℤ} (u : H1Function (openCubeSet (originCube d n))) : H1Function (cubeSet (originCube d n))

Promote an H¹ witness on the open centered cube to an H¹ witness on the corresponding half-open centered cube by shifting smooth compactly supported tests inward and passing to the limit.

Equations

• u.toCubeSetOriginCube = { toFun := u.toFun, grad := u.grad, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ }

theorem HCPolySupport.H1Function.exists_toCubeSetOriginCube {d : ℕ} [NeZero d] {n : ℤ} (u : H1Function (openCubeSet (originCube d n))) : ∃ (v : H1Function (cubeSet (originCube d n))), v.toFun = u.toFun ∧ v.grad = u.grad

noncomputable def HCPolySupport.H1Function.coordOnOpenCubeSetOriginCube {d : ℕ} {n : ℤ} (i : Fin d) : H1Function (openCubeSet (originCube d n))

The coordinate projection x ↦ x i as an H¹ function on the open centered cube, with constant gradient basisVec i.

Equations

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

noncomputable def HCPolySupport.H10Function.toCubeSetOriginCube {d : ℕ} [NeZero d] {n : ℤ} (u : H10Function (openCubeSet (originCube d n))) : H10Function (cubeSet (originCube d n))

Promote an H¹₀ witness on the open centered cube to an H¹₀ witness on the corresponding half-open centered cube.

Equations

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

@[simp]

theorem HCPolySupport.H10Function.toCubeSetOriginCube_toH1Function_toFun {d : ℕ} [NeZero d] {n : ℤ} (u : H10Function (openCubeSet (originCube d n))) : u.toCubeSetOriginCube.toFun = u.toFun

@[simp]

theorem HCPolySupport.H10Function.toCubeSetOriginCube_toH1Function_grad {d : ℕ} [NeZero d] {n : ℤ} (u : H10Function (openCubeSet (originCube d n))) : u.toCubeSetOriginCube.grad = u.grad

theorem HCPolySupport.H10Function.exists_originCubeInwardShiftData {d : ℕ} [NeZero d] {n : ℤ} (u : H10Function (cubeSet (originCube d n))) (m : ℕ) : ∃ (ε : ℝ), 0 < ε ∧ (tsupport fun (x : Vec d) => u.approx m (x - diagonalShift ε)) ⊆ openCubeSet (originCube d n) ∧ (∀ (x : Vec d), dist (u.approx m (x - diagonalShift ε)) (u.approx m x) ≤ 1 / (↑m + 1)) ∧ ∀ (i : Fin d) (x : Vec d), dist ((fderiv ℝ (u.approx m) (x - diagonalShift ε)) (basisVec i)) ((fderiv ℝ (u.approx m) x) (basisVec i)) ≤ 1 / (↑m + 1)

theorem HCPolySupport.H10Function.tendsto_shifted_originCube_approx {d : ℕ} {n : ℤ} (u : H10Function (cubeSet (originCube d n))) (εShift : ℕ → ℝ) (approx' : ℕ → Vec d → ℝ) (hvalueShiftBound : ∀ (m : ℕ) (x : Vec d), dist (approx' m x) (u.approx m x) ≤ 1 / (↑m + 1)) (hgradShiftBound : ∀ (m : ℕ) (i : Fin d) (x : Vec d), dist ((fderiv ℝ (u.approx m) (x - diagonalShift (εShift m))) (basisVec i)) ((fderiv ℝ (u.approx m) x) (basisVec i)) ≤ 1 / (↑m + 1)) (happrox'_smooth : ∀ (m : ℕ), ContDiff ℝ (↑⊤) (approx' m)) : Filter.Tendsto (fun (m : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => approx' m x - u.approx m x) 2 (MeasureTheory.volume.restrict (openCubeSet (originCube d n)))) Filter.atTop (nhds 0) ∧ ∀ (i : Fin d), Filter.Tendsto (fun (m : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (u.approx m) (x - diagonalShift (εShift m))) (basisVec i) - (fderiv ℝ (u.approx m) x) (basisVec i)) 2 (MeasureTheory.volume.restrict (openCubeSet (originCube d n)))) Filter.atTop (nhds 0)

theorem HCPolySupport.H10Function.tendsto_approx_restrict_originCube {d : ℕ} {n : ℤ} (u : H10Function (cubeSet (originCube d n))) : Filter.Tendsto (fun (m : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => u.approx m x - (u.restrict ⋯ ⋯).toFun x) 2 (MeasureTheory.volume.restrict (openCubeSet (originCube d n)))) Filter.atTop (nhds 0) ∧ ∀ (i : Fin d), Filter.Tendsto (fun (m : ℕ) => MeasureTheory.eLpNorm (fun (x : Vec d) => (fderiv ℝ (u.approx m) x) (basisVec i) - (u.restrict ⋯ ⋯).grad x i) 2 (MeasureTheory.volume.restrict (openCubeSet (originCube d n)))) Filter.atTop (nhds 0)

noncomputable def HCPolySupport.H10Function.toOpenCubeSetOriginCube {d : ℕ} [NeZero d] {n : ℤ} (u : H10Function (cubeSet (originCube d n))) : H10Function (openCubeSet (originCube d n))

Restrict an H¹₀ witness on the half-open centered cube to the corresponding open centered cube by pushing each smooth approximant slightly inward while keeping the shift small enough that the L² error still vanishes.

Equations

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

@[simp]

theorem HCPolySupport.H10Function.toOpenCubeSetOriginCube_toH1Function_toFun {d : ℕ} [NeZero d] {n : ℤ} (u : H10Function (cubeSet (originCube d n))) : u.toOpenCubeSetOriginCube.toFun = u.toFun

@[simp]

theorem HCPolySupport.H10Function.toOpenCubeSetOriginCube_toH1Function_grad {d : ℕ} [NeZero d] {n : ℤ} (u : H10Function (cubeSet (originCube d n))) : u.toOpenCubeSetOriginCube.grad = u.grad