Invariant Transport

Invariant concrete transport coefficients

This module supplies the child-swap symmetries needed to cancel the off-diagonal terms in the complete-tree Haar expansion.

theorem FD1D.completeHaarNode_intervalsSeparated_of_depth_eq {L : ℕ} (i j : CompleteHaarNode L) (hdepth : i.fst = j.fst) (hij : i ≠ j) : IntervalsSeparated haarNodeLeft haarNodeWidth i j

Distinct complete-tree nodes at the same depth have disjoint tent interiors.

theorem FD1D.FiniteLaw.oddSymmetry_mul_of_invariant_neg_fixed {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (e : Equiv.Perm Ω) (hμ : FiniteKernel.LawInvariant μ e) (f g : Ω → ℝ) (hf : ∀ (ω : Ω), f (e ω) = -f ω) (hg : ∀ (ω : Ω), g (e ω) = g ω) : μ.OddSymmetry fun (ω : Ω) => f ω * g ω

An invariant equivalence which negates one factor and fixes the other makes their product an odd observable.

theorem FD1D.FiniteLaw.oddSymmetry_mul_of_invariant_fixed_neg {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (e : Equiv.Perm Ω) (hμ : FiniteKernel.LawInvariant μ e) (f g : Ω → ℝ) (hf : ∀ (ω : Ω), f (e ω) = f ω) (hg : ∀ (ω : Ω), g (e ω) = -g ω) : μ.OddSymmetry fun (ω : Ω) => f ω * g ω

Symmetric version of oddSymmetry_mul_of_invariant_neg_fixed.

theorem FD1D.TreeSymmetry.inventoryPerm_eq_inventoryStatePerm {ι : Type u_1} [Fintype ι] {m : ℕ} (e : Equiv.Perm ι) : inventoryPerm e = inventoryStatePerm e

The inventory lift used by the symmetry module agrees with the canonical lift used by refreshed initialization.

theorem FD1D.completeHaar_crossTerm_symmetry_of_invariant_swaps {L : ℕ} {Ω : Type u_1} [Fintype Ω] (μ : FiniteLaw Ω) (b : Ω → CompleteHaarNode L → ℝ) (swap : (d : Fin L) → DyadicNode ↑d → Equiv.Perm Ω) (hinv : ∀ (d : Fin L) (v : DyadicNode ↑d), FiniteKernel.LawInvariant μ (swap d v)) (hflip : ∀ (d : Fin L) (v : DyadicNode ↑d) (ω : Ω), b ((swap d v) ω) ⟨d, v⟩ = -b ω ⟨d, v⟩) (hshallower : ∀ (d : Fin L) (v : DyadicNode ↑d) (k : Fin L) (w : Fin (2 ^ ↑k)), ↑k < ↑d → ∀ (ω : Ω), b ((swap d v) ω) ⟨k, w⟩ = b ω ⟨k, w⟩) (i j : CompleteHaarNode L) : i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ μ.OddSymmetry fun (ω : Ω) => b ω i * b ω j

Abstract complete-tree cancellation criterion. A swap at a node negates that node's coefficient and fixes every strictly shallower coefficient.

theorem FD1D.HierarchicalDynamics.concrete_haarCoefficient_swapNode {L m : ℕ} (a : ℝ) (ha : 0 < a) (i : CompleteHaarNode L) (x : InventoryState (DyadicNode L) m) : (stateDyadicMass a ((TreeSymmetry.inventorySwap ⋯ i.snd) x)).nodeCoefficient i = -(stateDyadicMass a x).nodeCoefficient i

Swapping the children of i negates its concrete Haar coefficient.

theorem FD1D.HierarchicalDynamics.concrete_haarCoefficient_strictAncestor {L m : ℕ} (a : ℝ) (ha : 0 < a) (i j : CompleteHaarNode L) (hji : ↑j.fst < ↑i.fst) (x : InventoryState (DyadicNode L) m) : (stateDyadicMass a ((TreeSymmetry.inventorySwap ⋯ i.snd) x)).nodeCoefficient j = (stateDyadicMass a x).nodeCoefficient j

A child swap at i fixes every concrete Haar coefficient at a strictly shallower depth.

theorem FD1D.HierarchicalDynamics.concrete_nodeCoefficient_crossTerm_symmetry_of_swapInvariant {L m : ℕ} (a : ℝ) (ha : 0 < a) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hinv : ∀ (d : Fin L) (v : DyadicNode ↑d), FiniteKernel.LawInvariant μ (TreeSymmetry.inventorySwap ⋯ v)) (i j : CompleteHaarNode L) : i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ μ.OddSymmetry fun (x : InventoryState (DyadicNode L) m) => (stateDyadicMass a x).nodeCoefficient i * (stateDyadicMass a x).nodeCoefficient j

Cross-term symmetry for the canonical node coefficients of the concrete dyadic mass.

theorem FD1D.HierarchicalDynamics.concrete_haar_crossTerm_symmetry_of_swapInvariant {L m : ℕ} (a : ℝ) (ha : 0 < a) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hinv : ∀ (d : Fin L) (v : DyadicNode ↑d), FiniteKernel.LawInvariant μ (TreeSymmetry.inventorySwap ⋯ v)) (i j : CompleteHaarNode L) : i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ μ.OddSymmetry fun (x : InventoryState (DyadicNode L) m) => stateHaarCoefficient a x i * stateHaarCoefficient a x j

The exact stateHaarCoefficient symmetry premise used by transport_cost_equation_three, for any law invariant under every child swap.

theorem FD1D.HierarchicalDynamics.concrete_stationary_haar_crossTerm_symmetry {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (μ : FiniteLaw (InventoryState (DyadicNode L) m)) (hirr : (kernel a ha hm).Irreducible) (hstationary : (kernel a ha hm).IsStationary μ) (i j : CompleteHaarNode L) : i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ μ.OddSymmetry fun (x : InventoryState (DyadicNode L) m) => stateHaarCoefficient a x i * stateHaarCoefficient a x j

The concrete stationary law satisfies the complete Haar cross-term symmetry premise in transport_cost_equation_three.

theorem FD1D.HierarchicalDynamics.concrete_iterate_refreshedLaw_lawInvariant {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (n : ℕ) (d : Fin L) (v : DyadicNode ↑d) : FiniteKernel.LawInvariant ((kernel a ha hm).iterate n (refreshedLaw L m)) (TreeSymmetry.inventorySwap ⋯ v)

Every iterate of the concrete kernel from the refreshed law is invariant under a specified child swap.

theorem FD1D.HierarchicalDynamics.concrete_refreshed_iterate_haar_crossTerm_symmetry {L m : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (n : ℕ) (i j : CompleteHaarNode L) : i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ ((kernel a ha hm).iterate n (refreshedLaw L m)).OddSymmetry fun (x : InventoryState (DyadicNode L) m) => stateHaarCoefficient a x i * stateHaarCoefficient a x j

Every refreshed iterate satisfies the complete Haar cross-term symmetry premise in transport_cost_equation_three.

theorem FD1D.HierarchicalDynamics.concrete_refreshed_timeAverage_haar_crossTerm_symmetry {L m T : ℕ} (a : ℝ) (ha : 0 < a) (hm : 0 < m) (hT : 0 < T) (i j : CompleteHaarNode L) : i ≠ j → IntervalsSeparated haarNodeLeft haarNodeWidth i j ∨ (FiniteLaw.timeAverage hT fun (t : Fin T) => (kernel a ha hm).iterate (↑t) (refreshedLaw L m)).OddSymmetry fun (z : Fin T × InventoryState (DyadicNode L) m) => stateHaarCoefficient a z.2 i * stateHaarCoefficient a z.2 j

The uniform mixture of the first T refreshed iterates has one time-preserving odd symmetry for every nonseparated coefficient pair.