Coarse-graining support: Support.Sobolev.H1.Algebra.H1Function

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

@[instance_reducible]

instance HCPolySupport.H1Function.instZero {d : ℕ} {U : Set (Vec d)} : Zero (H1Function U)

Equations

• HCPolySupport.H1Function.instZero = { zero := { toFun := 0, grad := 0, memL2 := ⋯, gradMemL2 := ⋯, hasWeakGradient := ⋯ } }

@[instance_reducible]

instance HCPolySupport.H1Function.instSMulReal {d : ℕ} {U : Set (Vec d)} : SMul ℝ (H1Function U)

Equations

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

@[instance_reducible]

instance HCPolySupport.H1Function.instNeg {d : ℕ} {U : Set (Vec d)} : Neg (H1Function U)

Equations

• HCPolySupport.H1Function.instNeg = { neg := fun (u : HCPolySupport.H1Function U) => -1 • u }

@[instance_reducible]

instance HCPolySupport.H1Function.instAdd {d : ℕ} {U : Set (Vec d)} : Add (H1Function U)

Equations

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

@[instance_reducible]

instance HCPolySupport.H1Function.instSub {d : ℕ} {U : Set (Vec d)} : Sub (H1Function U)

Equations

• HCPolySupport.H1Function.instSub = { sub := fun (u v : HCPolySupport.H1Function U) => u + -v }

@[simp]

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

@[simp]

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

@[simp]

theorem HCPolySupport.H1Function.add_toFun {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : (u + v).toFun = fun (x : Vec d) => u.toFun x + v.toFun x

@[simp]

theorem HCPolySupport.H1Function.add_grad {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : (u + v).grad = fun (x : Vec d) => u.grad x + v.grad x

@[simp]

theorem HCPolySupport.H1Function.smul_toFun {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1Function U) : (c • u).toFun = fun (x : Vec d) => c * u.toFun x

@[simp]

theorem HCPolySupport.H1Function.smul_grad {d : ℕ} {U : Set (Vec d)} (c : ℝ) (u : H1Function U) : (c • u).grad = fun (x : Vec d) => c • u.grad x

@[simp]

theorem HCPolySupport.H1Function.neg_toFun {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : (-u).toFun = fun (x : Vec d) => -u.toFun x

@[simp]

theorem HCPolySupport.H1Function.neg_grad {d : ℕ} {U : Set (Vec d)} (u : H1Function U) : (-u).grad = fun (x : Vec d) => -u.grad x

@[simp]

theorem HCPolySupport.H1Function.sub_toFun {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : (u - v).toFun = fun (x : Vec d) => u.toFun x - v.toFun x

@[simp]

theorem HCPolySupport.H1Function.sub_grad {d : ℕ} {U : Set (Vec d)} (u v : H1Function U) : (u - v).grad = fun (x : Vec d) => u.grad x - v.grad x

@[instance_reducible]

instance HCPolySupport.H1Function.instSMulNat {d : ℕ} {U : Set (Vec d)} : SMul ℕ (H1Function U)

Equations

• HCPolySupport.H1Function.instSMulNat = { smul := fun (n : ℕ) (u : HCPolySupport.H1Function U) => ↑n • u }

@[instance_reducible]

instance HCPolySupport.H1Function.instSMulInt {d : ℕ} {U : Set (Vec d)} : SMul ℤ (H1Function U)

Equations

• HCPolySupport.H1Function.instSMulInt = { smul := fun (n : ℤ) (u : HCPolySupport.H1Function U) => ↑n • u }

theorem HCPolySupport.H1Function.toFunGrad_injective {d : ℕ} {U : Set (Vec d)} : Function.Injective fun (u : H1Function U) => (u.toFun, u.grad)

@[instance_reducible]

instance HCPolySupport.H1Function.instAddCommGroup {d : ℕ} {U : Set (Vec d)} : AddCommGroup (H1Function U)

Equations

• HCPolySupport.H1Function.instAddCommGroup = Function.Injective.addCommGroup (fun (u : HCPolySupport.H1Function U) => (u.toFun, u.grad)) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

noncomputable def HCPolySupport.H1Function.toFunGradAddMonoidHom {d : ℕ} {U : Set (Vec d)} : H1Function U →+ (Vec d → ℝ) × (Vec d → Vec d)

The additive homomorphism sending an H¹ function to its pair of value and weak-gradient representatives.

Equations

• HCPolySupport.H1Function.toFunGradAddMonoidHom = { toFun := fun (u : HCPolySupport.H1Function U) => (u.toFun, u.grad), map_zero' := ⋯, map_add' := ⋯ }

@[instance_reducible]

noncomputable instance HCPolySupport.H1Function.instModuleReal {d : ℕ} {U : Set (Vec d)} : Module ℝ (H1Function U)

Equations

• HCPolySupport.H1Function.instModuleReal = Function.Injective.module ℝ HCPolySupport.H1Function.toFunGradAddMonoidHom ⋯ ⋯

theorem HCPolySupport.H1Function.hasWeakGradient_mulContDiff {d : ℕ} {U : Set (Vec d)} (u : H1Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) : HasWeakGradientOn U (fun (x : Vec d) => φ x * u.toFun x) fun (x : Vec d) (i : Fin d) => φ x * u.grad x i + u.toFun x * (fderiv ℝ φ x) (basisVec i)

The weak product rule for a smooth scalar multiplier on an H¹ function.

noncomputable def HCPolySupport.H1Function.mulContDiffMemLpTop {d : ℕ} {U : Set (Vec d)} (u : H1Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_memTop : MeasureTheory.MemLp φ ⊤ (MeasureTheory.volume.restrict U)) (hdφ_memTop : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => (fderiv ℝ φ x) (basisVec i)) ⊤ (MeasureTheory.volume.restrict U)) : H1Function U

Multiplication of an H¹ function by a smooth scalar multiplier which is bounded, together with its first derivatives, on the underlying domain. This is the non-compact-support variant of mulContDiffHasCompactSupport; the test function still provides the compact support in the weak-gradient identity.

Equations

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

@[simp]

theorem HCPolySupport.H1Function.mulContDiffMemLpTop_toFun {d : ℕ} {U : Set (Vec d)} (u : H1Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_memTop : MeasureTheory.MemLp φ ⊤ (MeasureTheory.volume.restrict U)) (hdφ_memTop : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => (fderiv ℝ φ x) (basisVec i)) ⊤ (MeasureTheory.volume.restrict U)) : (u.mulContDiffMemLpTop hφ hφ_memTop hdφ_memTop).toFun = fun (x : Vec d) => φ x * u.toFun x

@[simp]

theorem HCPolySupport.H1Function.mulContDiffMemLpTop_grad {d : ℕ} {U : Set (Vec d)} (u : H1Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_memTop : MeasureTheory.MemLp φ ⊤ (MeasureTheory.volume.restrict U)) (hdφ_memTop : ∀ (i : Fin d), MeasureTheory.MemLp (fun (x : Vec d) => (fderiv ℝ φ x) (basisVec i)) ⊤ (MeasureTheory.volume.restrict U)) : (u.mulContDiffMemLpTop hφ hφ_memTop hdφ_memTop).grad = fun (x : Vec d) (i : Fin d) => φ x * u.grad x i + u.toFun x * (fderiv ℝ φ x) (basisVec i)

noncomputable def HCPolySupport.H1Function.mulContDiffHasCompactSupport {d : ℕ} {U : Set (Vec d)} (u : H1Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : H1Function U

The H¹ product φ u for a smooth compactly supported multiplier, with gradient φ∇u + u∇φ.

Equations

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

@[simp]

theorem HCPolySupport.H1Function.mulContDiffHasCompactSupport_toFun {d : ℕ} {U : Set (Vec d)} (u : H1Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : (u.mulContDiffHasCompactSupport hφ hφ_compact).toFun = fun (x : Vec d) => φ x * u.toFun x

@[simp]

theorem HCPolySupport.H1Function.mulContDiffHasCompactSupport_grad {d : ℕ} {U : Set (Vec d)} (u : H1Function U) {φ : Vec d → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφ_compact : HasCompactSupport φ) : (u.mulContDiffHasCompactSupport hφ hφ_compact).grad = fun (x : Vec d) (i : Fin d) => φ x * u.grad x i + u.toFun x * (fderiv ℝ φ x) (basisVec i)