Unit-cube tools for the time integration by parts

Source: enhance.tex 8700–8830. Differentiation under the integral sign over the unit cube, periodic integration by parts on the unit cube (real-valued, C¹ hypotheses), the periodicity of the gradient of a periodic function, and the Cauchy–Schwarz inequality on a measure space (via the discriminant of λ ↦ ∫ (λ f - g)²).

def AVenhance.Infra.Section5.LeftToShow.cubeCl : Set (Homogenization.Vec 2)

The closed unit square.

Equations

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

theorem AVenhance.Infra.Section5.LeftToShow.isCompact_cubeCl : IsCompact cubeCl

theorem AVenhance.Infra.Section5.LeftToShow.unitCube_subset_cubeCl : unitCube ⊆ cubeCl

theorem AVenhance.Infra.Section5.LeftToShow.measurableSet_unitCube' : MeasurableSet unitCube

Differentiation under the integral over the unit cube

theorem AVenhance.Infra.Section5.LeftToShow.hasDerivAt_integral_unitCube {h h' : ℝ → Homogenization.Vec 2 → ℝ} (hc : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => h p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) (hd : ∀ (s : ℝ), 0 < s → ∀ (x : Homogenization.Vec 2), HasDerivAt (fun (r : ℝ) => h r x) (h' s x) s) (hc' : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => h' p.1 p.2) (Set.Ioi 0 ×ˢ Set.univ)) {t : ℝ} (ht : 0 < t) : HasDerivAt (fun (s : ℝ) => ∫ (x : Homogenization.Vec 2) in unitCube, h s x) (∫ (x : Homogenization.Vec 2) in unitCube, h' t x) t

Differentiation under the integral sign over the unit cube: a parameter function that is jointly continuous with jointly continuous pointwise time derivative on (0,∞) × ℝ².

Periodic integration by parts on the unit cube

theorem AVenhance.Infra.Section5.LeftToShow.Cube.integrableOn_unitCell_of_continuous {f : Homogenization.Vec 2 → ℝ} (hf : Continuous f) : MeasureTheory.IntegrableOn f (Torus.unitCell 2) MeasureTheory.volume

theorem AVenhance.Infra.Section5.LeftToShow.integral_unitCube_mul_spaceGrad {f g : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hg : ContDiff ℝ 1 g) (hpf : IsZ2Periodic f) (hpg : IsZ2Periodic g) (i : Fin 2) : ∫ (x : Homogenization.Vec 2) in unitCube, f x * spaceGrad g x i = -∫ (x : Homogenization.Vec 2) in unitCube, spaceGrad f x i * g x

Real periodic integration by parts on the unit cube.

theorem AVenhance.Infra.Section5.LeftToShow.isZ2Periodic_spaceGrad {f : Homogenization.Vec 2 → ℝ} (hf : ContDiff ℝ 1 f) (hper : IsZ2Periodic f) : IsZ2Periodic (spaceGrad f)

The gradient of a C¹ periodic function is periodic.

Cauchy–Schwarz

theorem AVenhance.Infra.Section5.LeftToShow.integral_mul_le_sqrt_mul_sqrt {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {f g : α → ℝ} (hf : MeasureTheory.Integrable (fun (x : α) => f x ^ 2) μ) (hg : MeasureTheory.Integrable (fun (x : α) => g x ^ 2) μ) (hfg : MeasureTheory.Integrable (fun (x : α) => f x * g x) μ) : ∫ (x : α), f x * g x ∂μ ≤ √(∫ (x : α), f x ^ 2 ∂μ) * √(∫ (x : α), g x ^ 2 ∂μ)

Cauchy–Schwarz for integrable f², g², f g (by the discriminant of λ ↦ ∫ (λ f - g)²).