The unpulled corrector flux divergence identity and its conditional cofactor push-forward along the inverse flow.

noncomputable def AVenhance.Infra.Section5.frozenCorrectorFlux {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (j : Fin 2) (t : ℝ) (y : Homogenization.Vec 2) : Homogenization.Vec 2

Flux in the jth corrector equation before the inverse-flow push-forward.

Equations

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

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

theorem AVenhance.Infra.Section5.CorrectorFlux.spaceGrad_const_mul_left {f : Homogenization.Vec 2 → ℝ} {x : Homogenization.Vec 2} (c : ℝ) (hf : DifferentiableAt ℝ f x) (i : Fin 2) : spaceGrad (fun (y : Homogenization.Vec 2) => c * f y) x i = c * spaceGrad f x i

theorem AVenhance.Infra.Section5.frozenCorrectorFlux_vecDiv {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) (k : ℤ) (j : Fin 2) (t : ℝ) (x : Homogenization.Vec 2) : vecDiv (frozenCorrectorFlux I κ m k j t) x = deriv (fun (s : ℝ) => I.chiMK κ m k s x j) t

The corrector equation is exactly the divergence identity for its base flux. No inverse-flow regularity or Piola premise enters this local step.