Joint regularity of the flux ingredients on the open half space

All statements are on (0,∞) × ℝ². Jointly C^∞ pieces: the diffusion matrix, ∇T, G_l, the shear field pulled back by the flows. The twisted corrector carries the time factor corrTime (only proved C²), so the divergence-form fluxes are treated at joint order 2; this suffices for continuity of their divergences.

The diffusion matrix

theorem AVenhance.Infra.Section5.Contracts.tf_contDiff_zetaMK {β : ℝ} (I : Ingredients β) (m : ℕ) (k : ℤ) : ContDiff ℝ (↑⊤) (I.zetaMK m k)

theorem AVenhance.Infra.Section5.Contracts.tf_psiTilde_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => psiTilde I hΦ m p.1 p.2

ψTilde_m is jointly C^∞.

theorem AVenhance.Infra.Section5.Contracts.tf_diffusion_contDiff {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (i j : Fin 2) : ContDiff ℝ ↑⊤ fun (p : ℝ × Homogenization.Vec 2) => diffusionMatrix I hΦ m κm p.1 p.2 i j

Each entry of the diffusion matrix is jointly C^∞.

Gradients of T, G_l

theorem AVenhance.Infra.Section5.Contracts.tf_gradT_contDiffOn {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (j : Fin 2) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => spaceGrad (T p.1) p.2 j) tfU

theorem AVenhance.Infra.Section5.Contracts.tf_G_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => G I hΦ m T l p.1 p.2 j) tfU

theorem AVenhance.Infra.Section5.Contracts.tf_gradG_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (l : ℤ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (i j : Fin 2) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => gradG I hΦ m T l p.1 p.2 i j) tfU

The generic flux form

noncomputable def AVenhance.Infra.Section5.Contracts.tfFlux (c : { k : ℤ // Odd k } → ℝ → ℝ) (D : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (W : { k : ℤ // Odd k } → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

∑_k c_k(t) D(t,x) W_k(t,x) over odd k.

Equations

• AVenhance.Infra.Section5.Contracts.tfFlux c D W t x = ∑' (k : { k : ℤ // Odd k }), c k t • (D t x).mulVec (W k t x)

theorem AVenhance.Infra.Section5.Contracts.tfFlux_contDiffOn {n : WithTop ℕ∞} (c : { k : ℤ // Odd k } → ℝ → ℝ) (D : ℝ → Homogenization.Vec 2 → Matrix (Fin 2) (Fin 2) ℝ) (W : { k : ℤ // Odd k } → ℝ → Homogenization.Vec 2 → Homogenization.Vec 2) (hc : ∀ (k : { k : ℤ // Odd k }), ContDiff ℝ n (c k)) (hD : ∀ (i j : Fin 2), ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => D p.1 p.2 i j) tfU) (hW : ∀ (k : { k : ℤ // Odd k }) (j : Fin 2), ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => W k p.1 p.2 j) tfU) (hact : ∀ (t₀ : ℝ), ∃ (S : Finset { k : ℤ // Odd k }), ∀ k ∉ S, ∀ (t : ℝ), |t - t₀| < 1 → c k t = 0) (i : Fin 2) : ContDiffOn ℝ n (fun (p : ℝ × Homogenization.Vec 2) => tfFlux c D W p.1 p.2 i) tfU

twistie3

theorem AVenhance.Infra.Section5.Contracts.tf_twistie3Flux_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => twistie3Flux I hΦ m κm T p.1 p.2 i) tfU

normie2

theorem AVenhance.Infra.Section5.Contracts.tf_normie2Flux_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hH : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => I.Hm hΦ m κm T p.1 p.2) tfU) (i : Fin 2) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => normie2Flux I hΦ m κm T p.1 p.2 i) tfU

normie1

noncomputable def AVenhance.Infra.Section5.Contracts.tfChiW {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The T-dependent factor of ΧTilde_{m,k} ∇G_{l_k}: the corrector without its time factor.

Equations

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

theorem AVenhance.Infra.Section5.Contracts.tf_chiGradG_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (k : ℤ) (t : ℝ) (x : Homogenization.Vec 2) : chiGradG I hΦ m κm T k t x = I.corrTime κm m k t • tfChiW I hΦ m T k t x

theorem AVenhance.Infra.Section5.Contracts.tf_normie1Flux_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : normie1Flux I hΦ m κm T t x = tfFlux (fun (k : { k : ℤ // Odd k }) (t : ℝ) => I.xiMK m (↑k) t * I.corrTime κm m (↑k) t) (fun (t : ℝ) (x : Homogenization.Vec 2) => diffusionMatrix I hΦ m κm t x) (fun (k : { k : ℤ // Odd k }) (t : ℝ) (x : Homogenization.Vec 2) => tfChiW I hΦ m T (↑k) t x) t x

theorem AVenhance.Infra.Section5.Contracts.tf_chiW_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (k : ℤ) (i : Fin 2) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => tfChiW I hΦ m T k p.1 p.2 i) tfU

theorem AVenhance.Infra.Section5.Contracts.tf_normie1Flux_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (i : Fin 2) : ContDiffOn ℝ 2 (fun (p : ℝ × Homogenization.Vec 2) => normie1Flux I hΦ m κm T p.1 p.2 i) tfU

R46

noncomputable def AVenhance.Infra.Section5.Contracts.tfR46Inner {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) : Homogenization.Vec 2

The vector inside the (time-only) flux matrix in R46.

Equations

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

theorem AVenhance.Infra.Section5.Contracts.tf_Gbar_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => Gbar I hΦ m T p.1 p.2) tfU

theorem AVenhance.Infra.Section5.Contracts.tf_R46Inner_contDiffOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) (j : Fin 2) : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => tfR46Inner I hΦ m T p.1 p.2 j) tfU

theorem AVenhance.Infra.Section5.Contracts.tf_spaceGrad_lin {f g : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (a b : ℝ) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => a * f y + b * g y) x i = a * spaceGrad f x i + b * spaceGrad g x i

theorem AVenhance.Infra.Section5.Contracts.tf_R46_eq {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) (m : ℕ) (κm : ℝ) (T : ℝ → Homogenization.Vec 2 → ℝ) (t : ℝ) (x : Homogenization.Vec 2) (hd : ∀ (j : Fin 2), DifferentiableAt ℝ (fun (y : Homogenization.Vec 2) => tfR46Inner I hΦ m T t y j) x) : R46 I hΦ m κm T t x = ∑ i : Fin 2, (I.flux κm m t i 0 * spaceGrad (fun (y : Homogenization.Vec 2) => tfR46Inner I hΦ m T t y 0) x i + I.flux κm m t i 1 * spaceGrad (fun (y : Homogenization.Vec 2) => tfR46Inner I hΦ m T t y 1) x i)

theorem AVenhance.Infra.Section5.Contracts.tf_R46_continuousOn {β : ℝ} (I : Ingredients β) {Φ : ℕ → ℝ → Homogenization.Vec 2 → ℝ} (hΦ : IsStreamSeq I Φ) {m : ℕ} (hm : 1 ≤ m) (κm : ℝ) {T : ℝ → Homogenization.Vec 2 → ℝ} (hT : ContDiffOn ℝ (↑⊤) (fun (p : ℝ × Homogenization.Vec 2) => T p.1 p.2) (Set.Ici 0 ×ˢ Set.univ)) : ContinuousOn (fun (p : ℝ × Homogenization.Vec 2) => R46 I hΦ m κm T p.1 p.2) tfU