3D Torus Sobolev Spaces

This file defines the H¹ Sobolev space on the 3D Torus using spectral properties.

@[reducible, inline]

abbrev Index3 : Type

Equations

• Index3 = (Fin 3 → ℤ)

instance instDecidableEqIndex3 : DecidableEq Index3

Equations

• instDecidableEqIndex3 = inferInstanceAs (DecidableEq (Fin 3 → ℤ))

instance instZeroIndex3 : Zero Index3

Equations

• instZeroIndex3 = Pi.instZero

instance instAddIndex3 : Add Index3

Equations

• instAddIndex3 = Pi.instAdd

instance instNegIndex3 : Neg Index3

Equations

• instNegIndex3 = Pi.instNeg

instance instAddCommGroupIndex3 : AddCommGroup Index3

Equations

• instAddCommGroupIndex3 = Pi.addCommGroup

def h1Weight (k : Index3) : ℝ

Equations

• h1Weight k = 1 + ‖fun (i : Fin 3) => ↑(k i)‖ ^ 2

theorem h1Weight_pos (k : Index3) : 0 < h1Weight k

def h1_carrier : Submodule ℂ (Index3 → ℂ)

Equations

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

def SobolevH1 : Type

Equations

• SobolevH1 = ↥h1_carrier

instance SobolevH1.instAddCommGroup : AddCommGroup SobolevH1

Equations

• SobolevH1.instAddCommGroup = h1_carrier.addCommGroup

instance SobolevH1.instModuleComplex : Module ℂ SobolevH1

Equations

• SobolevH1.instModuleComplex = h1_carrier.module

def SobolevH1.inner_sum (f g : SobolevH1) (k : Index3) : ℂ

The weighted inner product term.

Equations

• f.inner_sum g k = ↑(h1Weight k) * ((starRingEnd ℂ) (↑f k) * ↑g k)

theorem SobolevH1.inner_norm_summable (f g : SobolevH1) : Summable fun (k : Index3) => ‖f.inner_sum g k‖

The h1-weighted inner product terms are norm-summable.

theorem SobolevH1.inner_summable' (f g : SobolevH1) : Summable (f.inner_sum g)

The h1-weighted inner product terms are summable.

def SobolevH1.H1Inner (f g : SobolevH1) : ℂ

The H¹ inner product.

Equations

• f.H1Inner g = ∑' (k : Index3), f.inner_sum g k

theorem SobolevH1.re_inner_sum_self (f : SobolevH1) (k : Index3) : RCLike.re (f.inner_sum f k) = h1Weight k * ‖↑f k‖ ^ 2

Each term re(inner_sum f f k) = h1Weight k * ‖f.val k‖²

def SobolevH1.h1InnerCore : InnerProductSpace.Core ℂ SobolevH1

Core inner product structure for SobolevH1.

Equations

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

instance SobolevH1.instInnerComplex : Inner ℂ SobolevH1

Equations

• SobolevH1.instInnerComplex = InnerProductSpace.Core.toInner'

instance SobolevH1.instSeminormedAddCommGroup : SeminormedAddCommGroup SobolevH1

Equations

• SobolevH1.instSeminormedAddCommGroup = InnerProductSpace.Core.toSeminormedAddCommGroup

instance SobolevH1.instInnerProductSpaceComplex : InnerProductSpace ℂ SobolevH1

Equations

• SobolevH1.instInnerProductSpaceComplex = InnerProductSpace.ofCore SobolevH1.h1InnerCore.toCore