Time primitives of the actual large-cell diffusivity coefficient.

theorem AVenhance.Infra.Section4.iterate_periodic_primitive_bound {f : ℝ → ℝ} {P B : ℝ} (hP : 0 < P) (hB : 0 ≤ B) (hf : Continuous f) (hp : Function.Periodic f P) (hz : ∫ (t : ℝ) in 0..P, f t = 0) (hb : ∀ (t : ℝ), |f t| ≤ B) (t : ℝ) : |∫ (s : ℝ) in 0..t, f s| ≤ P * B

Primitive control uses the period length, rather than the time interval length.

theorem AVenhance.Infra.Section4.iterate_Kmat_periodic {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) : Function.Periodic (I.Kmat κ m) (tauPP β I.Λ m)

Periodicity follows from the explicit finite sum defining Kmat.

theorem AVenhance.Infra.Section4.iterate_centered_primitive {f : ℝ → ℝ} {P B : ℝ} {N : ℕ} (hP : 0 < P) (hB : 0 ≤ B) (hf : Continuous f) (hp : Function.Periodic f P) (hunit : ↑N * P = 1) (hb : ∀ (t : ℝ), |f t| ≤ B) : have avg := ∫ (s : ℝ) in 0..1, f s; have Q := fun (t : ℝ) => ∫ (s : ℝ) in 0..t, f s - avg; Q 0 = 0 ∧ Q 1 = 0 ∧ (∀ (t : ℝ), HasDerivAt Q (f t - avg) t) ∧ ∀ (t : ℝ), |Q t| ≤ 2 * P * B

The uncentered primitive is zero at both endpoints and differentiates back to the centered periodic coefficient.

noncomputable def AVenhance.Infra.Section4.iterateKmatPrimitive {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (t : ℝ) : Matrix (Fin 2) (Fin 2) ℝ

The material integration by parts uses this explicit primitive of Kmat.

Equations

• AVenhance.Infra.Section4.iterateKmatPrimitive I κ m t i j = ∫ (s : ℝ) in 0..t, I.Kmat κ m s i j - AVenhance.timeAvgMat (I.Kmat κ m) i j

theorem AVenhance.Infra.Section4.iterateKmatPrimitive_properties {β : ℝ} (I : Ingredients β) {κ : ℝ} (hκ : 0 < κ) {m : ℕ} (hm : 1 ≤ m) {B : ℝ} (hB : 0 ≤ B) (hb : ∀ (t : ℝ) (i j : Fin 2), |I.Kmat κ m t i j| ≤ B) : iterateKmatPrimitive I κ m 0 = 0 ∧ iterateKmatPrimitive I κ m 1 = 0 ∧ (∀ (t : ℝ) (i j : Fin 2), HasDerivAt (fun (s : ℝ) => iterateKmatPrimitive I κ m s i j) (I.Kmat κ m t i j - timeAvgMat (I.Kmat κ m) i j) t) ∧ ∀ (t : ℝ) (i j : Fin 2), |iterateKmatPrimitive I κ m t i j| ≤ 2 * tauPP β I.Λ m * B

Quantitative endpoint and derivative facts for the actual matrix primitive.