ClosedWalkNormalization.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization of a closed numerical word, counting repeated visits.

def OAI.TwoPointCorrelations.scalarWalkProduct line 12

Source documentation

Multiply departure-indexed edge coefficients along the actual integer walk.

noncomputable def scalarWalkProduct (h : ℕ) (weight : SignedStep → ℤ → ℝ)
    (n : ℤ) : List SignedStep → ℝ
  | [] => 1
  | a :: w => weight a n * scalarWalkProduct h weight (n + a.displacement h) w

Mentions: OAI.TwoPointCorrelations.SignedStep

lemma OAI.TwoPointCorrelations.scalarWalkProduct_mul line 17
lemma OAI.TwoPointCorrelations.scalarWalkProduct_congr line 25

theorem OAI.TwoPointCorrelations.scalarWalkProduct_normalize line 33

Source documentation

Each visit contributes its denominator once at departure and once at arrival; the only uncancelled factors lie at the two endpoints.

theorem scalarWalkProduct_normalize (h : ℕ) (a : SignedStep → ℤ → ℝ)
    (g : ℤ → ℝ) (hg : ∀ n, g n ≠ 0) (n : ℤ) (w : List SignedStep) :
    scalarWalkProduct h (fun t x => a t x / (g x * g (x + t.displacement h))) n w =
      scalarWalkProduct h (fun t x => a t x / (g x) ^ 2) n w *
        g n / g (n + wordDisplacement h w) := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.scalarWalkProduct, OAI.TwoPointCorrelations.wordDisplacement

theorem OAI.TwoPointCorrelations.scalarWalkProduct_closed_normalize line 48

Source documentation

On a closed word, the exact original edge denominators become the product of departure weights. Repeated sites remain repeated factors.

theorem scalarWalkProduct_closed_normalize (h : ℕ) (a : SignedStep → ℤ → ℝ)
    (g : ℤ → ℝ) (hg : ∀ n, g n ≠ 0) (n : ℤ) (w : List SignedStep)
    (hclosed : wordDisplacement h w = 0) :
    scalarWalkProduct h (fun t x => a t x / (g x * g (x + t.displacement h))) n w =
      scalarWalkProduct h (fun t x => a t x / (g x) ^ 2) n w := by
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordDisplacement, OAI.TwoPointCorrelations.scalarWalkProduct

theorem OAI.TwoPointCorrelations.signedIntegerWeight_closed_normalize line 57

Source documentation

Keep every arithmetic, vertex, and orientation condition while moving the exact matrix denominator to the departure site.

theorem signedIntegerWeight_closed_normalize (Q : Finset ℕ) (u : ℕ → ℝ)
    (eligible : SignedStep → ℕ → Prop) (g : ℤ → ℝ) (center : SignedStep → ℤ → ℝ) (L K : ℝ)
    (extra : SignedStep → ℤ → Prop) (h : ℕ) (n : ℤ) (w : List SignedStep)
    (hg : ∀ n, g n ≠ 0)
    (hperiod : ∀ t, ∀ q ∈ Q, ∀ z, center t (z + (h * q * t.tuple : ℕ)) = center t z)
    (hclosed : wordDisplacement h w = 0) :
    scalarWalkProduct h (fun t x =>
      signedIntegerWeight Q u (eligible t) g (center t) L K (extra t) h t x) n w =
      scalarWalkProduct h (fun t x =>
        if t.padding ∈ Q ∧ eligible t t.padding ∧ (t.padding : ℤ) ∣ x ∧
          integerEdgeKeep Q u (eligible t) g L K (extra t) x ∧
          integerEdgeKeep Q u (eligible t) g L K (extra t) (x + t.displacement h)
…

Mentions: OAI.TwoPointCorrelations.SignedStep, OAI.TwoPointCorrelations.wordDisplacement, OAI.TwoPointCorrelations.scalarWalkProduct, OAI.TwoPointCorrelations.signedIntegerWeight, OAI.TwoPointCorrelations.integerEdgeKeep