Energy estimates for a finite family of coupled derivative paths.

@[reducible, inline]

abbrev AVenhance.Infra.Classical.EnergyFamily (ι : Type u_4) (E : Type u_5) : Type (max u_4 u_5)

The ℓ² carrier for a family of copies of a real Hilbert space.

Equations

• AVenhance.Infra.Classical.EnergyFamily ι E = PiLp 2 fun (x : ι) => E

theorem AVenhance.Infra.Classical.intervalIntegrable_energyFamily_of_components {ι : Type u_1} {E : Type u_2} [Fintype ι] [NormedAddCommGroup E] (f : ℝ → ι → E) (hf : ∀ (i : ι), IntervalIntegrable (fun (t : ℝ) => f t i) MeasureTheory.volume 0 1) : IntervalIntegrable (fun (t : ℝ) => WithLp.toLp 2 (f t)) MeasureTheory.volume 0 1

Componentwise interval integrability assembles into integrability of a finite Hilbert product forcing path.

def AVenhance.Infra.Classical.energyFamilyMap {ι : Type u_1} {E : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (L : E →L[ℝ] G) : EnergyFamily ι E →L[ℝ] EnergyFamily ι G

Apply one continuous linear map in every coordinate of a finite Hilbert product.

Equations

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

@[simp]

theorem AVenhance.Infra.Classical.energyFamilyMap_apply {ι : Type u_1} {E : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (L : E →L[ℝ] G) (u : EnergyFamily ι E) (i : ι) : ((energyFamilyMap L) u).ofLp i = L (u.ofLp i)

theorem AVenhance.Infra.Classical.energyFamilyMap_norm_le {ι : Type u_1} {E : Type u_2} {G : Type u_3} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (L : E →L[ℝ] G) : ‖energyFamilyMap L‖ ≤ ‖L‖

The diagonal family map does not increase the operator norm.

def AVenhance.Infra.Classical.FamilyEnergy.energyFamilyMapLinear {ι : Type u_1} {E : Type u_2} {G : Type u_3} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] : (E →L[ℝ] G) →ₗ[ℝ] EnergyFamily ι E →L[ℝ] EnergyFamily ι G

Lift a continuous linear map to finite energy families, linearly in the map.

Equations

• AVenhance.Infra.Classical.FamilyEnergy.energyFamilyMapLinear = { toFun := fun (L : E →L[ℝ] G) => AVenhance.Infra.Classical.energyFamilyMap L, map_add' := ⋯, map_smul' := ⋯ }

theorem AVenhance.Infra.Classical.FamilyEnergy.energyFamilyMapLinear_apply {ι : Type u_1} {E : Type u_2} {G : Type u_3} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (L : E →L[ℝ] G) : energyFamilyMapLinear L = energyFamilyMap L

noncomputable def AVenhance.Infra.Classical.energyFamilyMapCLM {ι : Type u_1} {E : Type u_2} {G : Type u_3} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] : (E →L[ℝ] G) →L[ℝ] EnergyFamily ι E →L[ℝ] EnergyFamily ι G

The diagonal product construction depends continuously on the original linear map.

Equations

• AVenhance.Infra.Classical.energyFamilyMapCLM = AVenhance.Infra.Classical.FamilyEnergy.energyFamilyMapLinear.mkContinuous 1 ⋯

@[simp]

theorem AVenhance.Infra.Classical.energyFamilyMapCLM_apply {ι : Type u_1} {E : Type u_2} {G : Type u_3} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (L : E →L[ℝ] G) : energyFamilyMapCLM L = energyFamilyMap L

noncomputable def AVenhance.Infra.Classical.EnergyWeakFormData.family {ι : Type u_1} {E : Type u_2} {G : Type u_3} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (W : EnergyWeakFormData E G) : EnergyWeakFormData (EnergyFamily ι E) (EnergyFamily ι G)

Sum the component energy identities and drift forms on a finite Hilbert product.

Equations

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

def AVenhance.Infra.Classical.ForcedGalerkinData.ofWeak {E : Type u_2} {G : Type u_3} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (W : EnergyWeakFormData E G) (initial : E) (forcing : ℝ → E) (hforcing : IntervalIntegrable forcing MeasureTheory.volume 0 1) : ForcedGalerkinData E G

A forced Galerkin equation with a specified weak energy structure.

Equations

• AVenhance.Infra.Classical.ForcedGalerkinData.ofWeak W initial forcing hforcing = { weak := W, initial := initial, forcing := forcing, forcing_integrable := hforcing }

def AVenhance.Infra.Classical.energyFamilyPath {ι : Type u_1} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u : ι → C(↑(Set.Icc 0 1), E)) : C(↑(Set.Icc 0 1), EnergyFamily ι E)

The continuous path whose value is the finite Hilbert product of the component paths.

Equations

• AVenhance.Infra.Classical.energyFamilyPath u = { toFun := fun (t : ↑(Set.Icc 0 1)) => WithLp.toLp 2 fun (i : ι) => (u i) t, continuous_toFun := ⋯ }

noncomputable def AVenhance.Infra.Classical.ForcedGalerkinData.family {ι : Type u_1} {E : Type u_2} {G : Type u_3} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (W : EnergyWeakFormData E G) (initial : ι → E) (forcing : ℝ → ι → E) (hforcing : IntervalIntegrable (fun (t : ℝ) => WithLp.toLp 2 (forcing t)) MeasureTheory.volume 0 1) : ForcedGalerkinData (EnergyFamily ι E) (EnergyFamily ι G)

Combine finitely many forced paths with a common weak energy structure.

Equations

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

theorem AVenhance.Infra.Classical.ForcedGalerkinData.familyPath_isSolution {ι : Type u_1} {E : Type u_2} {G : Type u_3} [Fintype ι] [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] [NormedAddCommGroup G] [InnerProductSpace ℝ G] (W : EnergyWeakFormData E G) (initial : ι → E) (forcing : ℝ → ι → E) (hforcing : IntervalIntegrable (fun (t : ℝ) => WithLp.toLp 2 (forcing t)) MeasureTheory.volume 0 1) (hforcing_i : ∀ (i : ι), IntervalIntegrable (fun (t : ℝ) => forcing t i) MeasureTheory.volume 0 1) (u : ι → C(↑(Set.Icc 0 1), E)) (hu : ∀ (i : ι), (ofWeak W (initial i) (fun (t : ℝ) => forcing t i) ⋯).ode.IsSolution (u i)) : (family W initial forcing hforcing).ode.IsSolution (energyFamilyPath u)

If every coordinate path solves its forced equation, their finite Hilbert product solves the diagonal product equation.

noncomputable def AVenhance.Infra.Classical.ForcedGalerkinData.wordDerivativeFamilyData {ι : Type u_1} {G : Type u_3} [Fintype ι] [NormedAddCommGroup G] [InnerProductSpace ℝ G] {N : ℕ} (D : ForcedGalerkinData (Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) G) (u : C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) (word : ι → List (Fin 2)) : ForcedGalerkinData (EnergyFamily ι (Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) (EnergyFamily ι G)

The diagonal finite-family ODE for the ordered derivatives of one Fourier Galerkin path. Each component uses the original weak operator, with its derivative commutator included in the component forcing.

Equations

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

theorem AVenhance.Infra.Classical.ForcedGalerkinData.wordDerivativeFamilyPath_isSolution {ι : Type u_1} {G : Type u_3} [Fintype ι] [NormedAddCommGroup G] [InnerProductSpace ℝ G] {N : ℕ} (D : ForcedGalerkinData (Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N)) G) (u : C(↑(Set.Icc 0 1), Parabolic.FourierGalerkin.Coefficients (Parabolic.FourierGalerkin.RealFourierDimension N))) (hu : D.ode.IsSolution u) (word : ι → List (Fin 2)) : (D.wordDerivativeFamilyData u word).ode.IsSolution (energyFamilyPath fun (i : ι) => mapPath (realFourierWordDerivativeMap N (word i)) u)

Differentiated Galerkin paths form a solution of the diagonal finite-family ODE.