Coordinate expansions for averaged Faà di Bruno estimates. Positions are labelled even when coordinate directions repeat.

noncomputable def AVenhance.Infra.Ergodic.spatialJet {d : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (n : ℕ) (f : Homogenization.Vec d → F) (w : Fin n → Fin d) (x : Homogenization.Vec d) : F

An ordered spatial derivative evaluated on coordinate directions.

Equations

• AVenhance.Infra.Ergodic.spatialJet n f w x = (iteratedFDeriv ℝ n f x) fun (i : Fin n) => Homogenization.basisVec (w i)

theorem AVenhance.Infra.Ergodic.spatialJet_continuous {d n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {f : Homogenization.Vec d → F} (hf : ContDiff ℝ (↑⊤) f) (w : Fin n → Fin d) : Continuous (spatialJet n f w)

theorem AVenhance.Infra.Ergodic.spatialJet_periodic {d n : ℕ} {f : Homogenization.Vec d → ℂ} (hper : Torus.IsZdPeriodic f) (w : Fin n → Fin d) : Torus.IsZdPeriodic (spatialJet n f w)

theorem AVenhance.Infra.Ergodic.spatialJet_const_eq_coordDerivIter {d : ℕ} {f : Homogenization.Vec d → ℂ} (hf : ContDiff ℝ (↑⊤) f) (i : Fin d) (n : ℕ) : (spatialJet n f fun (x : Fin n) => i) = coordDerivIter i n f

theorem AVenhance.Infra.Ergodic.multilinear_coordinate_expansion {d k : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (T : Homogenization.Vec d [×k]→L[ℝ] F) (v : Fin k → Homogenization.Vec d) : T v = ∑ j : Fin k → Fin d, (∏ b : Fin k, v b (j b)) • T fun (b : Fin k) => Homogenization.basisVec (j b)

Coordinate expansion of a multilinear evaluation.

theorem AVenhance.Infra.Ergodic.composition_block_size_sum {n : ℕ} (c : OrderedFinpartition n) : ∑ b : Fin c.length, c.partSize b = n

Total size of all blocks in a partition of the derivative positions.

noncomputable def AVenhance.Infra.Ergodic.compositionJetTerm {d n : ℕ} (f : Homogenization.Vec d → ℂ) (X : Homogenization.Vec d → Homogenization.Vec d) (w : Fin n → Fin d) (c : OrderedFinpartition n) (j : Fin c.length → Fin d) (x : Homogenization.Vec d) : ℂ

The scalar summand of the coordinate Faà di Bruno expansion.

Equations

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

theorem AVenhance.Infra.Ergodic.spatialJet_comp_expansion {d n : ℕ} {f : Homogenization.Vec d → ℂ} {X : Homogenization.Vec d → Homogenization.Vec d} (hf : ContDiff ℝ (↑⊤) f) (hX : ContDiff ℝ (↑⊤) X) (w : Fin n → Fin d) (x : Homogenization.Vec d) : spatialJet n (f ∘ X) w x = ∑ c : OrderedFinpartition n, ∑ j : Fin c.length → Fin d, compositionJetTerm f X w c j x

Exact finite chain-rule sum, with every coordinate assignment retained.