MovingRegularTransfer.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The surviving regular Fourier transform in the giant-only transfer

theorem OAI.Ostmann.transfer_quotient line 12

theorem OAI.Ostmann.moving_regular_left_transfer line 22

Source documentation

The local left transform keeps its function; only the denominator changes.

theorem moving_regular_left_transfer {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (L R M D : ℕ) (v w s : ℤ)
    (hpL : p ∣ L) (hM : M.Coprime p) (hR : R.Coprime p) (hD : D.Coprime p)
    (hrel : v * R - w * L = s * M) :
    g ((v : ZMod p) / ((M * D : ℕ) : ZMod p)) =
      g ((s : ZMod p) / ((R * D : ℕ) : ZMod p)) := by
…

theorem OAI.Ostmann.moving_regular_right_transfer line 38

Source documentation

The conjugated right transform has the same new argument, because the underlying physical residue function is real.

theorem moving_regular_right_transfer {p : ℕ} [Fact p.Prime]
    (g : ZMod p → ℂ) (hg : ∀ x, g (-x) = conj (g x))
    (L R M D : ℕ) (v w s : ℤ)
    (hpR : p ∣ R) (hM : M.Coprime p) (hL : L.Coprime p) (hD : D.Coprime p)
    (hrel : v * R - w * L = s * M) :
    conj (g ((w : ZMod p) / ((M * D : ℕ) : ZMod p))) =
      g ((s : ZMod p) / ((L * D : ℕ) : ZMod p)) := by
…

def OAI.Ostmann.movingRegularTransform line 55

Source documentation

Product of the actual local transforms, with their CRT cofactors.

noncomputable def movingRegularTransform {I : Type*} [Fintype I]
    (p : I → ℕ) [∀ i, NeZero (p i)]
    (g : ∀ i, ZMod (p i) → ℂ) (D : ℕ) (s : ℤ) : ℂ :=
…

theorem OAI.Ostmann.moving_regular_transform_split line 67

Source documentation

Splitting the actual prime list extracts exactly the pivot row and retains the old regular transform at the composite pivot denominator.

theorem moving_regular_transform_split {H K : Type*} [Fintype H] [Fintype K]
    (L : H → ℕ) (R : K → ℕ) [∀ i, NeZero (L i)] [∀ i, NeZero (R i)]
    (gL : ∀ i, ZMod (L i) → ℂ) (gR : ∀ i, ZMod (R i) → ℂ)
    (D : ℕ) (s : ℤ) :
    movingRegularTransform (Sum.elim L R)
      (fun i => match i with | .inl j => gL j | .inr j => gR j) D s =
    movingRegularTransform L gL (D * ∏ i, R i) s *
      movingRegularTransform R gR (D * ∏ i, L i) s := by
…

Mentions: OAI.Ostmann.movingRegularTransform

theorem OAI.Ostmann.moving_regular_transform_grouped_key line 91

Source documentation

The extracted row depends only on the grouped key v/H mod P, with the original outside denominator and every local cofactor unchanged.

theorem moving_regular_transform_grouped_key {J : Type*} [Fintype J]
    (p : J → ℕ) [∀ j, Fact (p j).Prime]
    (g : ∀ j, ZMod (p j) → ℂ) (H D : ℕ) (v : ℤ)
    (hH : H.Coprime (∏ j, p j)) :
    movingRegularTransform p g D
      ((positiveIntegerPivotKey (∏ j, p j)
        (Finset.prod_pos (fun j _ => (Fact.out : (p j).Prime).pos)) H v).val : ℤ) =
      movingRegularTransform p g (D * H) v := by
…

Mentions: OAI.Ostmann.movingRegularTransform, OAI.Ostmann.positiveIntegerPivotKey

theorem OAI.Ostmann.moving_full_transform_grouped line 113

Source documentation

The full current transform factors through the precise grouped row used by the Cauchy step, before the giant is extended to integers.

theorem moving_full_transform_grouped {J K : Type*} [Fintype J] [Fintype K]
    (p : J → ℕ) (q : K → ℕ)
    [∀ j, Fact (p j).Prime] [∀ k, Fact (q k).Prime]
    (g : ∀ j, ZMod (p j) → ℂ) (h : ∀ k, ZMod (q k) → ℂ)
    (D : ℕ) (v : ℤ) (hqp : (∏ k, q k).Coprime (∏ j, p j)) :
    movingRegularTransform (Sum.elim p q)
      (fun i => match i with | .inl j => g j | .inr k => h k) D v =
    movingRegularTransform p g D
      ((positiveIntegerPivotKey (∏ j, p j)
        (Finset.prod_pos (fun j _ => (Fact.out : (p j).Prime).pos)) (∏ k, q k) v).val : ℤ) *
      movingRegularTransform q h (D * ∏ j, p j) v := by
…

Mentions: OAI.Ostmann.movingRegularTransform, OAI.Ostmann.positiveIntegerPivotKey

theorem OAI.Ostmann.moving_regular_transform_transfer line 129

Source documentation

No averaging or approximation occurs when the two surviving transforms combine. The extracted pivot and compensation product disappear together.

theorem moving_regular_transform_transfer {H K : Type*} [Fintype H] [Fintype K]
    (L : H → ℕ) (R : K → ℕ)
    [∀ i, Fact (L i).Prime] [∀ i, Fact (R i).Prime]
    (gL : ∀ i, ZMod (L i) → ℂ) (gR : ∀ i, ZMod (R i) → ℂ)
    (hgR : ∀ i x, gR i (-x) = conj (gR i x))
    (M D : ℕ) (v w s : ℤ)
    (hc : Pairwise (fun i j => (Sum.elim L R i).Coprime (Sum.elim L R j)))
    (hM : ∀ i, M.Coprime (Sum.elim L R i))
    (hD : ∀ i, D.Coprime (Sum.elim L R i))
    (hrel : v * (∏ i, R i) - w * (∏ i, L i) = s * M) :
    movingRegularTransform L gL (M * D) v *
      conj (movingRegularTransform R gR (M * D) w) =
…

Mentions: OAI.Ostmann.movingRegularTransform