Space-time pairing of the finite Fourier projection with forcing

The scalar identity for each Fourier mode is summed and rewritten as one space-time integral against the finite Fourier projection.

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

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

def AVenhance.Infra.Section5.RelativeError.forcedClamp (t : ℝ) : ℝ

Clamp of a real time into [0,1].

Equations

• AVenhance.Infra.Section5.RelativeError.forcedClamp t = max 0 (min t 1)

theorem AVenhance.Infra.Section5.RelativeError.forcedClamp_mem (t : ℝ) : forcedClamp t ∈ Set.Icc 0 1

theorem AVenhance.Infra.Section5.RelativeError.forcedClamp_eq {t : ℝ} (ht : t ∈ Set.Icc 0 1) : forcedClamp t = t

theorem AVenhance.Infra.Section5.RelativeError.forcedClamp_continuous : Continuous forcedClamp

theorem AVenhance.Infra.Section5.RelativeError.forced_projection_expansion (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Parabolic.WeakUniqueness.weakFourierModeProjection N u t x = ∑ i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N), Parabolic.WeakUniqueness.weakModePairing u (forcedMode N i) t * forcedMode N i x

The projection of a path is the Fourier polynomial with the coefficient path.

theorem AVenhance.Infra.Section5.RelativeError.forced_projection_eq_sum (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) : Parabolic.WeakUniqueness.weakFourierModeProjection N u t = fun (x : Homogenization.Vec 2) => ∑ i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N), Parabolic.WeakUniqueness.weakModePairing u (forcedMode N i) t * forcedMode N i x

The projection of a path as a function of space is a finite sum.

theorem AVenhance.Infra.Section5.RelativeError.forcedMode_differentiable (N : ℕ) (i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) : Differentiable ℝ (forcedMode N i)

theorem AVenhance.Infra.Section5.RelativeError.forced_projection_grad_expansion (N : ℕ) (u : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (j : Fin 2) : spaceGrad (Parabolic.WeakUniqueness.weakFourierModeProjection N u t) x j = ∑ i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N), Parabolic.WeakUniqueness.weakModePairing u (forcedMode N i) t * spaceGrad (forcedMode N i) x j

Spatial gradient of the projection.

theorem AVenhance.Infra.Section5.RelativeError.forced_spaceGrad_component_continuous {ψ : Homogenization.Vec 2 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (j : Fin 2) : Continuous fun (x : Homogenization.Vec 2) => spaceGrad ψ x j

Continuity of x ↦ ∂_j ψ for a smooth ψ.

theorem AVenhance.Infra.Section5.RelativeError.forced_coeff_clamp_continuous {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {G : ℝ × Homogenization.Vec 2 → ℝ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (h : ForcedModePath κ f u Du G F) (N : ℕ) (i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N)) : Continuous fun (s : ℝ) => Parabolic.WeakUniqueness.weakModePairing u (forcedMode N i) (forcedClamp s)

Time-clamped coefficient of a mode is continuous.

theorem AVenhance.Infra.Section5.RelativeError.forced_projection_memLp {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {G : ℝ × Homogenization.Vec 2 → ℝ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (h : ForcedModePath κ f u Du G F) (N : ℕ) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => Parabolic.WeakUniqueness.weakFourierModeProjection N u p.1 p.2) 2 (MeasureTheory.volume.restrict timeCube)

The Fourier projection of a forced path is in spacetime L².

theorem AVenhance.Infra.Section5.RelativeError.forced_projection_grad_memLp {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {G : ℝ × Homogenization.Vec 2 → ℝ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (h : ForcedModePath κ f u Du G F) (N : ℕ) (j : Fin 2) : MeasureTheory.MemLp (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (Parabolic.WeakUniqueness.weakFourierModeProjection N u p.1) p.2 j) 2 (MeasureTheory.volume.restrict timeCube)

The projected gradient components of a forced path are in spacetime L².

theorem AVenhance.Infra.Section5.RelativeError.forced_modeSum_eq (κ : ℝ) (Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (G : ℝ × Homogenization.Vec 2 → ℝ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (u : ℝ → Homogenization.Vec 2 → ℝ) (N : ℕ) (t : ℝ) (x : Homogenization.Vec 2) : ∑ i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N), Parabolic.WeakUniqueness.weakModePairing u (forcedMode N i) t * forcedModeIntegrand κ Du G F (forcedMode N i) (t, x) = G (t, x) * Parabolic.WeakUniqueness.weakFourierModeProjection N u t x + κ * Homogenization.vecDot (Du t x) (spaceGrad (Parabolic.WeakUniqueness.weakFourierModeProjection N u t) x) + Homogenization.vecDot (F (t, x)) (spaceGrad (Parabolic.WeakUniqueness.weakFourierModeProjection N u t) x)

Pointwise mode-sum identity.

noncomputable def AVenhance.Infra.Section5.RelativeError.forcedProjectionPairing (κ : ℝ) (Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (G : ℝ × Homogenization.Vec 2 → ℝ) (F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2) (u : ℝ → Homogenization.Vec 2 → ℝ) (N : ℕ) (p : ℝ × Homogenization.Vec 2) : ℝ

The integrand of the space-time pairing against the projection.

Equations

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

theorem AVenhance.Infra.Section5.RelativeError.forcedProjectionPairing_integrable {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {G : ℝ × Homogenization.Vec 2 → ℝ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (h : ForcedModePath κ f u Du G F) (N : ℕ) : MeasureTheory.Integrable (forcedProjectionPairing κ Du G F u N) (MeasureTheory.volume.restrict timeCube)

theorem AVenhance.Infra.Section5.RelativeError.forced_pairing {κ : ℝ} {f : Homogenization.Vec 2 → ℝ} {u : ℝ → Homogenization.Vec 2 → ℝ} {Du : ℝ → Homogenization.Vec 2 → Homogenization.Vec 2} {G : ℝ × Homogenization.Vec 2 → ℝ} {F : ℝ × Homogenization.Vec 2 → Homogenization.Vec 2} (h : ForcedModePath κ f u Du G F) (N : ℕ) {t : ℝ} (ht : t ∈ Set.Icc 0 1) : ∫ (s : ℝ) in 0..t, 2 * ∑ i : Fin (Parabolic.FourierGalerkin.RealFourierDimension N), Parabolic.WeakUniqueness.weakModePairing u (forcedMode N i) s * forcedModeForcing κ Du G F (forcedMode N i) s = ∫ (p : ℝ × Homogenization.Vec 2) in Parabolic.WeakUniqueness.weakEnergyRegion t, 2 * forcedProjectionPairing κ Du G F u N p

Summing the mode energy integrals gives the space-time pairing with the projection.