Time averaging the fixed-time flux symmetry, under explicit time regularity.

noncomputable def AVenhance.Infra.Section3.KhomSymmetry.fluxDiagDiff {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) : ℝ → ℝ

Difference of the two diagonal entries of the time-dependent flux matrix.

Equations

• AVenhance.Infra.Section3.KhomSymmetry.fluxDiagDiff I κ m t = I.flux κ m t 1 1 - I.flux κ m t 0 0

theorem AVenhance.Infra.Section3.fluxDiagDiff_add_twoCellCount {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ t : ℝ) : KhomSymmetry.fluxDiagDiff I κ m (t + 2 * tauPP β I.Λ m) = -KhomSymmetry.fluxDiagDiff I κ m t

The diagonal difference changes sign after a half-period shift.

theorem AVenhance.Infra.Section3.khom_diag_entries_eq_of_flux_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hcont : ∀ (i j : Fin 2), Continuous fun (t : ℝ) => I.flux κ m t i j) : I.Khom κ m 0 0 = I.Khom κ m 1 1

The difference of the two time-averaged diagonal entries is zero whenever the fixed-time flux entries are continuous in time.

theorem AVenhance.Infra.Section3.khom_eq_scalar_of_flux_continuous {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (κ : ℝ) (hκ : 0 < κ) (hcont : ∀ (i j : Fin 2), Continuous fun (t : ℝ) => I.flux κ m t i j) : I.Khom κ m = I.KhomScalar κ m • 1 ∧ 0 < I.KhomScalar κ m

Conditional completion of the scalar-flux argument: once the fixed-time flux entries are shown continuous in time, its time average is scalar and its scalar is at least κ.