MovingGiantSpectator.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Fixed spectator diagrams for the integral moving-giant coefficient

The support multiplier is allowed to include every original arithmetic and smooth restriction. Only a nonzero multiplier requires integrality. Thus the identification retains, rather than discards, the original support boundary.

theorem OAI.Ostmann.MovingGiantTree.exists_supported_diagram line 17

Source documentation

The diagram is chosen before the bulk variables and support multiplier.

theorem MovingGiantTree.exists_supported_diagram {q : ℕ} [Fact q.Prime]
    {n C : ℕ} (T : MovingGiantTree n C) (hT : T.UnitsAt q)
    (D : (ZMod q)ˣ) (XL XR : ℕ) (A B : (ZMod q)ˣ)
    (hA : (XL : ZMod q) = A) (hB : (XR : ZMod q) = B) :
    ∃ d : SpectatorDiagram q n,
      d.D = D ∧ d.XL = A ∧ d.XR = B ∧
      d.conjugations = transferConjugations n false ∧
      ∀ (g : ZMod q → ℂ) (x : TreeLeafTuple ℕ n)
        (y : TreeLeafTuple (ZMod q)ˣ n) (c : ℂ),
        TreeNaturalLift n x y → (c ≠ 0 → T.Integral XL XR x) →
        c * movingGiantAmplitude g D T XL XR x = c * d.value g y := by
…

Mentions: OAI.Ostmann.MovingGiantTree, OAI.Ostmann.SpectatorDiagram, OAI.Ostmann.transferConjugations, OAI.Ostmann.TreeLeafTuple, OAI.Ostmann.TreeNaturalLift, OAI.Ostmann.movingGiantAmplitude

theorem OAI.Ostmann.movingGiant_pair_diagrams line 39

Source documentation

Two original integral histories have the paired factor in (8.5), with fixed diagrams and a common support multiplier.

theorem movingGiant_pair_diagrams {q : ℕ} [Fact q.Prime]
    {n C₁ C₂ : ℕ} (T₁ : MovingGiantTree n C₁) (T₂ : MovingGiantTree n C₂)
    (hT₁ : T₁.UnitsAt q) (hT₂ : T₂.UnitsAt q)
    (D₁ D₂ : (ZMod q)ˣ) (XL₁ XR₁ XL₂ XR₂ : ℕ)
    (A₁ B₁ A₂ B₂ : (ZMod q)ˣ)
    (hA₁ : (XL₁ : ZMod q) = A₁) (hB₁ : (XR₁ : ZMod q) = B₁)
    (hA₂ : (XL₂ : ZMod q) = A₂) (hB₂ : (XR₂ : ZMod q) = B₂) :
    ∃ d₁ d₂ : SpectatorDiagram q n,
      d₁.conjugations = transferConjugations n false ∧
      d₂.conjugations = transferConjugations n false ∧
      ∀ (g : ZMod q → ℂ) (x₁ x₂ : TreeLeafTuple ℕ n)
        (y₁ y₂ : TreeLeafTuple (ZMod q)ˣ n) (c : ℂ),
…

Mentions: OAI.Ostmann.MovingGiantTree, OAI.Ostmann.SpectatorDiagram, OAI.Ostmann.transferConjugations, OAI.Ostmann.TreeLeafTuple