Proof of the §3 characterization of the qMNR family.

theorem AVenhance.Proofs.Ingredients.qMNR_char {β : ℝ} (I : Ingredients β) (κ : ℝ) (_hκ : 0 < κ) (m : ℕ) (hm : 1 ≤ m) (n : ℕ) : (∀ (t : ℝ), I.qMNR κ m n 0 t = I.jMN κ m n t - timeAvgMat (I.jMN κ m n)) ∧ (∀ (r : ℕ), Function.Periodic (I.qMNR κ m n r) (4 * tau β I.Λ m)) ∧ (∀ (r : ℕ), 1 ≤ r → timeAvgMat (I.qMNR κ m n r) = 0) ∧ (∀ (r : ℕ) (t : ℝ) (i j : Fin 2), HasDerivAt (fun (s : ℝ) => I.qMNR κ m n (r + 1) s i j) (-I.qMNR κ m n r t i j) t) ∧ ∀ (q' : ℕ → ℝ → Matrix (Fin 2) (Fin 2) ℝ), (∀ (t : ℝ), q' 0 t = I.jMN κ m n t - timeAvgMat (I.jMN κ m n)) → (∀ (r : ℕ), Function.Periodic (q' r) (4 * tau β I.Λ m)) → (∀ (r : ℕ), 1 ≤ r → timeAvgMat (q' r) = 0) → (∀ (r : ℕ) (t : ℝ) (i j : Fin 2), HasDerivAt (fun (s : ℝ) => q' (r + 1) s i j) (-q' r t i j) t) → ∀ (r : ℕ), q' r = I.qMNR κ m n r