A classical solution is a weak solution

The regularity clauses of IsWeakSolutionGrad follow from joint continuity up to t = 0; the weak identity follows from integration by parts in time and in space against the periodic smooth test functions.

theorem AVenhance.Infra.Section5.RelativeError.classicalFiniteUnitCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict unitCube)

theorem AVenhance.Infra.Section5.RelativeError.classicalFiniteTimeCube : MeasureTheory.IsFiniteMeasure (MeasureTheory.volume.restrict timeCube)

def AVenhance.Infra.Section5.RelativeError.forcedClosedCell : Set (Homogenization.Vec 2)

The closed unit cell.

Equations

• AVenhance.Infra.Section5.RelativeError.forcedClosedCell = Set.univ.pi fun (x : Fin 2) => Set.Icc 0 1

theorem AVenhance.Infra.Section5.RelativeError.forcedClosedCell_compact : IsCompact forcedClosedCell

theorem AVenhance.Infra.Section5.RelativeError.unitCube_ae_eq_closedCell : unitCube =ᵐ[MeasureTheory.volume] forcedClosedCell

theorem AVenhance.Infra.Section5.RelativeError.unitCube_subset_closedCell : unitCube ⊆ forcedClosedCell

theorem AVenhance.Infra.Section5.RelativeError.classical_contDiffOn {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) : ContDiffOn ℝ (↑⊤) (Function.uncurry θ) classicalHalfSpace

theorem AVenhance.Infra.Section5.RelativeError.classical_weak_regularity {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hb : Continuous fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (hθ : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) : (∀ t ∈ Set.Icc 0 1, IsZ2Periodic (θ t) ∧ Homogenization.MemL2On unitCube (θ t)) ∧ (∃ (C : ℝ), ∀ t ∈ Set.Icc 0 1, l2NormSq (θ t) ≤ C) ∧ MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => θ p.1 p.2) 2 (MeasureTheory.volume.restrict timeCube) ∧ (∀ (i : Fin 2), MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (θ p.1) p.2 i) 2 (MeasureTheory.volume.restrict timeCube)) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 1), IsPeriodicH1With (θ t) fun (x : Homogenization.Vec 2) => spaceGrad (θ t) x) ∧ MeasureTheory.Integrable (fun (p : ℝ × Homogenization.Vec 2) => Homogenization.vecDot (b p.1 p.2) (spaceGrad (θ p.1) p.2)) (MeasureTheory.volume.restrict timeCube) ∧ ∀ (ψ : Homogenization.Vec 2 → ℝ), ContDiff ℝ (↑⊤) ψ → IsZ2Periodic ψ → ContinuousOn (fun (t : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, θ t x * ψ x) (Set.Icc 0 1)

Regularity clauses (1)-(7) of the weak-solution predicate for a classical solution.

theorem AVenhance.Infra.Section5.RelativeError.continuous_integrable_timeCube {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : Continuous F) : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)

A continuous function is integrable on the time cell.

theorem AVenhance.Infra.Section5.RelativeError.continuous_integrableOn_unitCube' {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.Integrable f (MeasureTheory.volume.restrict unitCube)

A continuous function is integrable on the unit cube.

theorem AVenhance.Infra.Section5.RelativeError.timeCube_integral_eq_time_space {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, F p = ∫ (t : ℝ) in Set.Ioo 0 1, ∫ (x : Homogenization.Vec 2) in unitCube, F (t, x)

Fubini on the time cell, time outermost.

theorem AVenhance.Infra.Section5.RelativeError.timeCube_integral_eq_space_time {F : ℝ × Homogenization.Vec 2 → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict timeCube)) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, F p = ∫ (x : Homogenization.Vec 2) in unitCube, ∫ (t : ℝ) in Set.Ioo 0 1, F (t, x)

Fubini on the time cell, space outermost.

theorem AVenhance.Infra.Section5.RelativeError.test_timeDeriv_continuous {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => φ p.1 p.2) : Continuous fun (p : ℝ × Homogenization.Vec 2) => deriv (fun (s : ℝ) => φ s p.2) p.1

Time derivative of a test function is continuous.

theorem AVenhance.Infra.Section5.RelativeError.classical_time_ibp {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) (x : Homogenization.Vec 2) : ∫ (t : ℝ) in 0..1, -clExt θ (t, x) * deriv (fun (s : ℝ) => φ s x) t = g x * φ 0 x + ∫ (t : ℝ) in 0..1, clTimeExt θ (t, x) * φ t x

Integration by parts in time for one spatial point.

theorem AVenhance.Infra.Section5.RelativeError.vecDot_comm' (a c : Homogenization.Vec 2) : Homogenization.vecDot a c = Homogenization.vecDot c a

theorem AVenhance.Infra.Section5.RelativeError.classical_space_ibp {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hθ : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) {t : ℝ} (ht : 0 < t) : ∫ (x : Homogenization.Vec 2) in unitCube, κ * Homogenization.vecDot (fun (i : Fin 2) => clGradExt θ i (t, x)) (spaceGrad (φ t) x) = -∫ (x : Homogenization.Vec 2) in unitCube, (clTimeExt θ (t, x) + Homogenization.vecDot (b t x) fun (i : Fin 2) => clGradExt θ i (t, x)) * φ t x

Integration by parts in space at one positive time.

theorem AVenhance.Infra.Section5.RelativeError.classical_weak_identity {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hb : Continuous fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (hθ : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) {φ : ℝ → Homogenization.Vec 2 → ℝ} (hφ : IsTestFunction φ) : ∫ (p : ℝ × Homogenization.Vec 2) in timeCube, -θ p.1 p.2 * deriv (fun (s : ℝ) => φ s p.2) p.1 + Homogenization.vecDot (b p.1 p.2) (spaceGrad (θ p.1) p.2) * φ p.1 p.2 + κ * Homogenization.vecDot (spaceGrad (θ p.1) p.2) (spaceGrad (φ p.1) p.2) = ∫ (x : Homogenization.Vec 2) in unitCube, g x * φ 0 x

The weak identity (clause 8) of the weak-solution predicate.

theorem AVenhance.Infra.Section5.RelativeError.classical_isWeakSolutionGrad {b : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {κ : ℝ} {g : Homogenization.Vec 2 → ℝ} {θ : ℝ → Homogenization.Vec 2 → ℝ} (hb : Continuous fun (p : ℝ × Homogenization.Vec 2) => b p.1 p.2) (hθ : IsClassicalSol b κ (fun (x : ℝ) (x_1 : Homogenization.Vec 2) => 0) g θ) : IsWeakSolutionGrad b κ g θ fun (t : ℝ) (x : Homogenization.Vec 2) => spaceGrad (θ t) x

A classical solution with a continuous drift is a weak solution, with its classical gradient as weak gradient.