Linear operations on periodic weak gradients

Cell L² control and periodicity imply global integrability against compact tests. This lets the whole-space weak derivative identities be subtracted without relying on junk integral values.

def AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakTimeClosedCell : Set (ℝ × Homogenization.Vec 2)

Closed time-space unit cell for the weak equation algebra.

Equations

• AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakTimeClosedCell = Set.Icc 0 1 ×ˢ Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakTimeClosedCell_compact : IsCompact weakTimeClosedCell

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakTimeCube_subset_closedCell : timeCube ⊆ weakTimeClosedCell

def AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakSpatialClosedCell : Set (Homogenization.Vec 2)

Closed spatial unit cell used for compactness and periodic integration.

Equations

• AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakSpatialClosedCell = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakSpatialClosedCell_compact : IsCompact weakSpatialClosedCell

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakUnitCube_subset_closedCell : unitCube ⊆ weakSpatialClosedCell

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weak_unitCube_volume_lt_top : MeasureTheory.volume unitCube < ⊤

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_finite_unitCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakTimeCube_measure_eq_product : MeasureTheory.volume.restrict timeCube = (MeasureTheory.volume.restrict (Set.Ioo 0 1)).prod (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_finite_timeCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_continuous_memLp_two_timeCube {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : Continuous F) : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_continuous_memL2On {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : Homogenization.MemL2On unitCube f

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_continuous_timeCube_bound {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : Continuous F) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ p ∈ timeCube, ‖F p‖ ≤ C

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_product_integrable_timeCube {f g : ℝ × Homogenization.Vec 2 → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict timeCube)) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict timeCube)) : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => f p * g p) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weak_product_integrable_cell {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : MeasureTheory.Integrable (fun (x : Homogenization.Vec 2) => f x * g x) (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weak_l2_sub_sq_le {f g : Homogenization.Vec 2 → ℝ} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) : (l2NormSq fun (x : Homogenization.Vec 2) => f x - g x) ≤ 2 * l2NormSq f + 2 * l2NormSq g

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakSpacetimeSpatialGradient_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) : Continuous fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (φ p.1) p.2

noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.weakEquationIntegrand (b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (κ : ℝ) (θ : ℝ → Homogenization.Vec 2 → ℝ) (Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (φ : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) : ℝ

Time, drift, and diffusion terms of the tested weak parabolic equation.

Equations

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

theorem AVenhance.Infra.Parabolic.WeakUniqueness.weakEquationIntegrand_integrable {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} {Dθ : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {φ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => θ p.1 p.2) 2 (MeasureTheory.volume.restrict timeCube)) (hDθ : ∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Dθ p.1 p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) (hDrift : MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (b p.1 p.2) (Dθ p.1 p.2)) (MeasureTheory.volume.restrict timeCube)) (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) : MeasureTheory.Integrable (weakEquationIntegrand b κ θ Dθ φ) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakPartialDerivOn_sub_univ {u v Du Dv : Homogenization.Vec 2 → ℝ} {i : Fin 2} (hu : Homogenization.MemL2On unitCube u) (hv : Homogenization.MemL2On unitCube v) (hDu : Homogenization.MemL2On unitCube Du) (hDv : Homogenization.MemL2On unitCube Dv) (hperU : IsZ2Periodic u) (hperV : IsZ2Periodic v) (hperDu : IsZ2Periodic Du) (hperDv : IsZ2Periodic Dv) (hweakU : Homogenization.HasWeakPartialDerivOn Set.univ i u Du) (hweakV : Homogenization.HasWeakPartialDerivOn Set.univ i v Dv) : Homogenization.HasWeakPartialDerivOn Set.univ i (fun (x : Homogenization.Vec 2) => u x - v x) fun (x : Homogenization.Vec 2) => Du x - Dv x

theorem AVenhance.Infra.Parabolic.WeakUniqueness.isPeriodicH1With_sub {u v : Homogenization.Vec 2 → ℝ} {Du Dv : Homogenization.Vec 2 → Homogenization.Vec 2} (hu : IsPeriodicH1With u Du) (hv : IsPeriodicH1With v Dv) : IsPeriodicH1With (fun (x : Homogenization.Vec 2) => u x - v x) fun (x : Homogenization.Vec 2) => Du x - Dv x

The periodic H¹ witnesses are closed under subtraction, with the expected weak gradient.

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weak_vecDot_sub_right (v u w : Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) : Homogenization.vecDot (v x) (u x - w x) = Homogenization.vecDot (v x) (u x) - Homogenization.vecDot (v x) (w x)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weak_vecDot_sub_left (u w v : Homogenization.Vec 2 → Homogenization.Vec 2) (x : Homogenization.Vec 2) : Homogenization.vecDot (u x - w x) (v x) = Homogenization.vecDot (u x) (v x) - Homogenization.vecDot (w x) (v x)

theorem AVenhance.Infra.Parabolic.WeakUniqueness.WeakAlgebra.weakEquationIntegrand_sub {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {θ η : ℝ → Homogenization.Vec 2 → ℝ} {D E : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (φ : ℝ → Homogenization.Vec 2 → ℝ) (p : ℝ × Homogenization.Vec 2) : weakEquationIntegrand b κ (fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - η t x) (fun (t : ℝ) (x : Homogenization.Vec 2) => D t x - E t x) φ p = weakEquationIntegrand b κ θ D φ p - weakEquationIntegrand b κ η E φ p

theorem AVenhance.Infra.Parabolic.WeakUniqueness.isWeakSolutionGrad_sub {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {f g : Homogenization.Vec 2 → ℝ} {θ η : ℝ → Homogenization.Vec 2 → ℝ} {D E : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} (hf : Homogenization.MemL2On unitCube f) (hg : Homogenization.MemL2On unitCube g) (hθ : IsWeakSolutionGrad b κ f θ D) (hη : IsWeakSolutionGrad b κ g η E) : IsWeakSolutionGrad b κ (fun (x : Homogenization.Vec 2) => f x - g x) (fun (t : ℝ) (x : Homogenization.Vec 2) => θ t x - η t x) fun (t : ℝ) (x : Homogenization.Vec 2) => D t x - E t x

Difference of two solutions of the same equation is a weak solution with the corresponding difference datum and difference gradient.