1. OAI
  2. NumberTheory
  3. DirichletL
  4. GaussSum
  5. CompletedExpansion
import OAI.NumberTheory.DirichletL.Arithmetic.IdealMobiusnamespace OAInoncomputable sectionopen scoped BigOperatorsopen MulChar AddCharopen scoped BigOperatorsopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen MeasureTheory Realopen scoped FourierTransform SchwartzMapopen Finset Complexopen scoped Classicalopen scoped Classicalopen Filter Real Asymptoticsopen ActualEisensteinCubicopen Filteropen ActualEisensteinCubic RationalPrimeExtraction ShortDraftLatticeCountopen ActualEisensteinCubic ShortDraftLatticeCountopen Filteropen scoped Topologyopen EisensteinEmbedding ConcreteTraceCRT ActualEisensteinCubicopen MulChar AddCharopen Filter Asymptoticsopen scoped LSeries.notation ArithmeticFunction.Moebiusopen Filteropen MulChar AddCharopen MulChar AddCharopen scoped LSeries.notation ArithmeticFunction.Moebiusopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptoticsopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Filter Asymptoticsopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptotics Ideal NumberFieldopen Filteropen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen MeasureTheory Realopen scoped ContDiff FourierTransform SchwartzMapopen scoped BigOperators Classicalopen scoped BigOperators Classicalopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen MeasureTheory Setopen scoped BigOperatorsopen scoped BigOperators Classicalopen scoped BigOperators Classicalopen ActualEisensteinCubic UniqueFactorizationMonoidopen scoped BigOperators Classicalnamespace CompletedGaussopen ActualEisensteinCubicdef expandedTerm (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) (I H J : Ideal O) : ℂ := (UniqueFactorizationMonoid.moebius H : ℂ) * cubeWeight Ψ (H * J) * (columnWeight Ψ I / (Real.sqrt (Ideal.absNorm I : ℝ) : ℂ) * Vstar W ((Ideal.absNorm I : ℝ) * (Ideal.absNorm H : ℝ) ^ 3 * (Ideal.absNorm J : ℝ) ^ 3 / X))theorem finite_support_expandedTerm (Ψ : O →* ℂ) (W : ℝ → ℂ) (hW : HasCompactSupport W) (X : ℝ) (hX : 0 < X) : (Function.support (fun p : Ideal O × Ideal O × Ideal O => expandedTerm Ψ W X p.1 p.2.1 p.2.2)).Finite := Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ (Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finite Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ ∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → expandedTerm Ψ W X (I, J, H).1 (I, J, H).2.1 (I, J, H).2.2 = 0Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ ∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → expandedTerm Ψ W X (I, J, H).1 (I, J, H).2.1 (I, J, H).2.2 = 0 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ ∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → expandedTerm Ψ W X (I, J, H).1 (I, J, H).2.1 (I, J, H).2.2 = 0 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal OH:Ideal OJ:Ideal Ohz:I = 0 ∨ H = 0 ∨ J = 0⊢ expandedTerm Ψ W X (I, H, J).1 (I, H, J).2.1 (I, H, J).2.2 = 0 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XH:Ideal OJ:Ideal O⊢ expandedTerm Ψ W X (0, H, J).1 (0, H, J).2.1 (0, H, J).2.2 = 0Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal OJ:Ideal O⊢ expandedTerm Ψ W X (I, 0, J).1 (I, 0, J).2.1 (I, 0, J).2.2 = 0Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal OH:Ideal O⊢ expandedTerm Ψ W X (I, H, 0).1 (I, H, 0).2.1 (I, H, 0).2.2 = 0 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XH:Ideal OJ:Ideal O⊢ expandedTerm Ψ W X (0, H, J).1 (0, H, J).2.1 (0, H, J).2.2 = 0Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal OJ:Ideal O⊢ expandedTerm Ψ W X (I, 0, J).1 (I, 0, J).2.1 (I, 0, J).2.2 = 0Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal OH:Ideal O⊢ expandedTerm Ψ W X (I, H, 0).1 (I, H, 0).2.1 (I, H, 0).2.2 = 0 All goals completed! 🐙 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ ∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → expandedTerm Ψ W X (I, J, H).1 (I, J, H).2.1 (I, J, H).2.2 = 0 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal OH:Ideal OJ:Ideal Ohw:W (↑(absNorm I) * ↑(absNorm H) ^ 3 * ↑(absNorm J) ^ 3 / X) = 0⊢ expandedTerm Ψ W X (I, H, J).1 (I, H, J).2.1 (I, H, J).2.2 = 0 All goals completed! 🐙theorem expandedTerm_scale (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) (I H J : Ideal O) : (UniqueFactorizationMonoid.moebius H : ℂ) * cubeWeight Ψ H * summand Ψ W (X / (Ideal.absNorm H : ℝ) ^ 3) I J = expandedTerm Ψ W X I H J := Ψ:O →* ℂW:ℝ → ℂX:ℝI:Ideal OH:Ideal OJ:Ideal O⊢ ↑(moebius H) * (cubeWeight Ψ) H * summand Ψ W (X / ↑(absNorm H) ^ 3) I J = expandedTerm Ψ W X I H J Ψ:O →* ℂW:ℝ → ℂX:ℝI:Ideal OH:Ideal OJ:Ideal Oharg:↑(absNorm I) * ↑(absNorm J) ^ 3 / (X / ↑(absNorm H) ^ 3) = ↑(absNorm I) * ↑(absNorm H) ^ 3 * ↑(absNorm J) ^ 3 / X⊢ ↑(moebius H) * (cubeWeight Ψ) H * summand Ψ W (X / ↑(absNorm H) ^ 3) I J = expandedTerm Ψ W X I H J Ψ:O →* ℂW:ℝ → ℂX:ℝI:Ideal OH:Ideal OJ:Ideal Oharg:↑(absNorm I) * ↑(absNorm J) ^ 3 / (X / ↑(absNorm H) ^ 3) = ↑(absNorm I) * ↑(absNorm H) ^ 3 * ↑(absNorm J) ^ 3 / X⊢ ↑(moebius H) * (cubeWeight Ψ) H * (columnWeight Ψ I / ↑√↑(absNorm I) * (cubeWeight Ψ) J * Vstar W (↑(absNorm I) * ↑(absNorm H) ^ 3 * ↑(absNorm J) ^ 3 / X)) = ↑(moebius H) * ((cubeWeight Ψ) H * (cubeWeight Ψ) J) * (columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) * ↑(absNorm H) ^ 3 * ↑(absNorm J) ^ 3 / X)) All goals completed! 🐙theorem expandedTerm_one (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) (I J : Ideal O) : expandedTerm Ψ W X I 1 J = summand Ψ W X I J := Ψ:O →* ℂW:ℝ → ℂX:ℝI:Ideal OJ:Ideal O⊢ expandedTerm Ψ W X I 1 J = summand Ψ W X I J Ψ:O →* ℂW:ℝ → ℂX:ℝI:Ideal OJ:Ideal O⊢ (cubeWeight Ψ) J * (columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) * ↑(absNorm J) ^ 3 / X)) = columnWeight Ψ I / ↑√↑(absNorm I) * (cubeWeight Ψ) J * Vstar W (↑(absNorm I) * ↑(absNorm J) ^ 3 / X) All goals completed! 🐙theorem completedT_finite_support (Ψ : O →* ℂ) (W : ℝ → ℂ) (hW : HasCompactSupport W) (X : ℝ) (hX : 0 < X) : (Function.support (fun p : Ideal O × Ideal O => summand Ψ W X p.1 p.2)).Finite := Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ (Function.support fun p => summand Ψ W X p.1 p.2).Finite Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finite⊢ (Function.support fun p => summand Ψ W X p.1 p.2).Finite Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finitehinj:Function.Injective fun p => (p.1, 1, p.2)⊢ (Function.support fun p => summand Ψ W X p.1 p.2).Finite Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finitehinj:Function.Injective fun p => (p.1, 1, p.2)hp:((fun p => (p.1, 1, p.2)) ⁻¹' Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finite⊢ (Function.support fun p => summand Ψ W X p.1 p.2).Finite Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finitehinj:Function.Injective fun p => (p.1, 1, p.2)hp:(Function.support fun p => expandedTerm Ψ W X p.1 1 p.2).Finite⊢ (Function.support fun p => summand Ψ W X p.1 p.2).Finite All goals completed! 🐙theorem completedT_summable (Ψ : O →* ℂ) (W : ℝ → ℂ) (hW : HasCompactSupport W) (X : ℝ) (hX : 0 < X) : Summable (fun p : Ideal O × Ideal O => summand Ψ W X p.1 p.2) := summable_of_hasFiniteSupport (completedT_finite_support Ψ W hW X hX)theorem weighted_completedT_reopen (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) (H : Ideal O) : (UniqueFactorizationMonoid.moebius H : ℂ) * cubeWeight Ψ H * completedT Ψ W (X / (Ideal.absNorm H : ℝ) ^ 3) = ∑' I : Ideal O, ∑' J : Ideal O, expandedTerm Ψ W X I H J := Ψ:O →* ℂW:ℝ → ℂX:ℝH:Ideal O⊢ ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3) = ∑' (I : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J All goals completed! 🐙theorem cube_inverse_finite_support (Ψ : O →* ℂ) (W : ℝ → ℂ) (hW : HasCompactSupport W) (X : ℝ) (hX : 0 < X) : (Function.support (fun H : Ideal O => (UniqueFactorizationMonoid.moebius H : ℂ) * cubeWeight Ψ H * completedT Ψ W (X / (Ideal.absNorm H : ℝ) ^ 3))).Finite := Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ (Function.support fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)).Finite Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finite⊢ (Function.support fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)).Finite Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finite⊢ (Function.support fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)) ⊆ (fun p => p.2.1) '' Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).FiniteH:Ideal OhH:H ∈ Function.support fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)⊢ H ∈ (fun p => p.2.1) '' Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).FiniteH:Ideal OhH:H ∈ Function.support fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)hn:H ∉ (fun p => p.2.1) '' Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2⊢ False Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).FiniteH:Ideal OhH:H ∈ Function.support fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)hn:H ∉ (fun p => p.2.1) '' Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hzero:∀ (I J : Ideal O), expandedTerm Ψ W X I H J = 0⊢ False Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).FiniteH:Ideal OhH:H ∈ Function.support fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)hn:H ∉ (fun p => p.2.1) '' Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hzero:∀ (I J : Ideal O), expandedTerm Ψ W X I H J = 0⊢ (fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)) H = 0 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).FiniteH:Ideal OhH:H ∈ Function.support fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)hn:H ∉ (fun p => p.2.1) '' Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hzero:∀ (I J : Ideal O), expandedTerm Ψ W X I H J = 0⊢ ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3) = 0 Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < Xhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).FiniteH:Ideal OhH:H ∈ Function.support fun H => ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3)hn:H ∉ (fun p => p.2.1) '' Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hzero:∀ (I J : Ideal O), expandedTerm Ψ W X I H J = 0⊢ ∑' (I : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = 0 All goals completed! 🐙theorem cube_inner_inverse (Ψ : O →* ℂ) (W : ℝ → ℂ) (hW : HasCompactSupport W) (X : ℝ) (hX : 0 < X) (I : Ideal O) : (∑' H : Ideal O, ∑' J : Ideal O, expandedTerm Ψ W X I H J) = columnWeight Ψ I / (Real.sqrt (Ideal.absNorm I : ℝ) : ℂ) * Vstar W ((Ideal.absNorm I : ℝ) / X) := Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal O⊢ ∑' (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal Of:Ideal O → ℂ := fun B => columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) * ↑(absNorm B) ^ 3 / X)⊢ ∑' (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal Of:Ideal O → ℂ := fun B => columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) * ↑(absNorm B) ^ 3 / X)heq:∀ (H J : Ideal O), ↑(moebius H) * (cubeWeight Ψ) (H * J) * f (H * J) = expandedTerm Ψ W X I H J⊢ ∑' (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal Of:Ideal O → ℂ := fun B => columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) * ↑(absNorm B) ^ 3 / X)heq:∀ (H J : Ideal O), ↑(moebius H) * (cubeWeight Ψ) (H * J) * f (H * J) = expandedTerm Ψ W X I H Jhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finite⊢ ∑' (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal Of:Ideal O → ℂ := fun B => columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) * ↑(absNorm B) ^ 3 / X)heq:∀ (H J : Ideal O), ↑(moebius H) * (cubeWeight Ψ) (H * J) * f (H * J) = expandedTerm Ψ W X I H Jhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finitehp:(Function.support fun p => expandedTerm Ψ W X I p.1 p.2).Finite⊢ ∑' (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal Of:Ideal O → ℂ := fun B => columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) * ↑(absNorm B) ^ 3 / X)heq:∀ (H J : Ideal O), ↑(moebius H) * (cubeWeight Ψ) (H * J) * f (H * J) = expandedTerm Ψ W X I H Jhf:(Function.support fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2).Finitehp:(Function.support fun p => expandedTerm Ψ W X I p.1 p.2).Finitehgeneric:∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * (cubeWeight Ψ) (H * J) * f (H * J) = f 1⊢ ∑' (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) All goals completed! 🐙theorem completed_cube_inverse_vstar (Ψ : O →* ℂ) (W : ℝ → ℂ) (hW : HasCompactSupport W) (X : ℝ) (hX : 0 < X) : (∑' H : Ideal O, (UniqueFactorizationMonoid.moebius H : ℂ) * cubeWeight Ψ H * completedT Ψ W (X / (Ideal.absNorm H : ℝ) ^ 3)) = ∑' I : Ideal O, columnWeight Ψ I / (Real.sqrt (Ideal.absNorm I : ℝ) : ℂ) * Vstar W ((Ideal.absNorm I : ℝ) / X) := Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ ∑' (H : Ideal O), ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3) = ∑' (I : Ideal O), columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2⊢ ∑' (H : Ideal O), ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3) = ∑' (I : Ideal O), columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable F⊢ ∑' (H : Ideal O), ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3) = ∑' (I : Ideal O), columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }⊢ ∑' (H : Ideal O), ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3) = ∑' (I : Ideal O), columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)⊢ ∑' (H : Ideal O), ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3) = ∑' (I : Ideal O), columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) calc _ = ∑' H : Ideal O, ∑' I : Ideal O, ∑' J : Ideal O, expandedTerm Ψ W X I H J := Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)⊢ ∑' (H : Ideal O), ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3) = ∑' (H : Ideal O) (I : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J All goals completed! 🐙 _ = ∑' p : Ideal O × Ideal O × Ideal O, F (e p) := Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)⊢ ∑' (H : Ideal O) (I : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = ∑' (p : Ideal O × Ideal O × Ideal O), F (e p) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)⊢ ∑' (H : Ideal O) (I : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = ∑' (b : Ideal O) (c : Ideal O × Ideal O), F (e (b, c)) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)⊢ ∀ (b : Ideal O), ∑' (I : Ideal O) (J : Ideal O), expandedTerm Ψ W X I b J = ∑' (c : Ideal O × Ideal O), F (e (b, c)) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)H:Ideal O⊢ ∑' (I : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J = ∑' (c : Ideal O × Ideal O), F (e (H, c)) All goals completed! 🐙 _ = ∑' p : Ideal O × Ideal O × Ideal O, F p := e.tsum_eq F _ = ∑' I : Ideal O, ∑' H : Ideal O, ∑' J : Ideal O, expandedTerm Ψ W X I H J := Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)⊢ ∑' (p : Ideal O × Ideal O × Ideal O), F p = ∑' (I : Ideal O) (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)⊢ ∑' (b : Ideal O) (c : Ideal O × Ideal O), F (b, c) = ∑' (I : Ideal O) (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)⊢ ∀ (b : Ideal O), ∑' (c : Ideal O × Ideal O), F (b, c) = ∑' (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X b H J Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂ := fun p => expandedTerm Ψ W X p.1 p.2.1 p.2.2hF:Summable Fe:Ideal O × Ideal O × Ideal O ≃ Ideal O × Ideal O × Ideal O := { toFun := fun p => (p.2.1, p.1, p.2.2), invFun := fun p => (p.2.1, p.1, p.2.2), left_inv := ⋯, right_inv := ⋯ }hswap:Summable fun p => F (e p)I:Ideal O⊢ ∑' (c : Ideal O × Ideal O), F (I, c) = ∑' (H : Ideal O) (J : Ideal O), expandedTerm Ψ W X I H J All goals completed! 🐙 _ = _ := tsum_congr (cube_inner_inverse Ψ W hW X hX)theorem vstar_source_normalization (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) (hX : 0 < X) (I : Ideal O) : columnWeight Ψ I / (Real.sqrt (Ideal.absNorm I : ℝ) : ℂ) * Vstar W ((Ideal.absNorm I : ℝ) / X) = (Real.sqrt X : ℂ)⁻¹ * columnWeight Ψ I * W ((Ideal.absNorm I : ℝ) / X) := Ψ:O →* ℂW:ℝ → ℂX:ℝhX:0 < XI:Ideal O⊢ columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) = (↑√X)⁻¹ * columnWeight Ψ I * W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂX:ℝhX:0 < XI:Ideal OhI:I = 0⊢ columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) = (↑√X)⁻¹ * columnWeight Ψ I * W (↑(absNorm I) / X)Ψ:O →* ℂW:ℝ → ℂX:ℝhX:0 < XI:Ideal OhI:¬I = 0⊢ columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) = (↑√X)⁻¹ * columnWeight Ψ I * W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂX:ℝhX:0 < XI:Ideal OhI:I = 0⊢ columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) = (↑√X)⁻¹ * columnWeight Ψ I * W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂX:ℝhX:0 < X⊢ columnWeight Ψ 0 / ↑√↑(absNorm 0) * Vstar W (↑(absNorm 0) / X) = (↑√X)⁻¹ * columnWeight Ψ 0 * W (↑(absNorm 0) / X); All goals completed! 🐙 Ψ:O →* ℂW:ℝ → ℂX:ℝhX:0 < XI:Ideal OhI:¬I = 0hN:0 < ↑(absNorm I)⊢ columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) = (↑√X)⁻¹ * columnWeight Ψ I * W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂX:ℝhX:0 < XI:Ideal OhI:¬I = 0hN:0 < ↑(absNorm I)hsN:↑√↑(absNorm I) ≠ 0⊢ columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) = (↑√X)⁻¹ * columnWeight Ψ I * W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂX:ℝhX:0 < XI:Ideal OhI:¬I = 0hN:0 < ↑(absNorm I)hsN:↑√↑(absNorm I) ≠ 0hsX:↑√X ≠ 0⊢ columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) = (↑√X)⁻¹ * columnWeight Ψ I * W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂX:ℝhX:0 < XI:Ideal OhI:¬I = 0hN:0 < ↑(absNorm I)hsN:↑√↑(absNorm I) ≠ 0hsX:↑√X ≠ 0⊢ columnWeight Ψ I / ↑√↑(absNorm I) * (↑√↑(absNorm I) / ↑√X * W (↑(absNorm I) / X)) = (↑√X)⁻¹ * columnWeight Ψ I * W (↑(absNorm I) / X) All goals completed! 🐙theorem completed_cube_inverse (Ψ : O →* ℂ) (W : ℝ → ℂ) (hW : HasCompactSupport W) (X : ℝ) (hX : 0 < X) : (Real.sqrt X : ℂ)⁻¹ * (∑' I : Ideal O, columnWeight Ψ I * W ((Ideal.absNorm I : ℝ) / X)) = ∑' H : Ideal O, (UniqueFactorizationMonoid.moebius H : ℂ) * cubeWeight Ψ H * completedT Ψ W (X / (Ideal.absNorm H : ℝ) ^ 3) := Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ (↑√X)⁻¹ * ∑' (I : Ideal O), columnWeight Ψ I * W (↑(absNorm I) / X) = ∑' (H : Ideal O), ↑(moebius H) * (cubeWeight Ψ) H * completedT Ψ W (X / ↑(absNorm H) ^ 3) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ ∑' (x : Ideal O), (↑√X)⁻¹ * (columnWeight Ψ x * W (↑(absNorm x) / X)) = ∑' (I : Ideal O), columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < X⊢ ∀ (b : Ideal O), (↑√X)⁻¹ * (columnWeight Ψ b * W (↑(absNorm b) / X)) = columnWeight Ψ b / ↑√↑(absNorm b) * Vstar W (↑(absNorm b) / X) Ψ:O →* ℂW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XI:Ideal O⊢ (↑√X)⁻¹ * (columnWeight Ψ I * W (↑(absNorm I) / X)) = columnWeight Ψ I / ↑√↑(absNorm I) * Vstar W (↑(absNorm I) / X) All goals completed! 🐙open ActualEisensteinCubic ConcreteTraceCRTtheorem normalizedFactors_product {ι : Type*} [Fintype ι] (p : ι → O) [∀ i, (Ideal.span {p i}).IsMaximal] : UniqueFactorizationMonoid.normalizedFactors (Ideal.span {∏ i, p i}) = Finset.univ.val.map (fun i => Ideal.span {p i}) := ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximal⊢ normalizedFactors (span {∏ i, p i}) = Multiset.map (fun i => span {p i}) Finset.univ.val ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhp:∀ (i : ι), Prime (span {p i})⊢ normalizedFactors (span {∏ i, p i}) = Multiset.map (fun i => span {p i}) Finset.univ.val ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhp:∀ (i : ι), Prime (span {p i})h:normalizedFactors (Multiset.map (fun i => span {p i}) Finset.univ.val).prod = Multiset.map (fun i => span {p i}) Finset.univ.val⊢ normalizedFactors (span {∏ i, p i}) = Multiset.map (fun i => span {p i}) Finset.univ.val ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhp:∀ (i : ι), Prime (span {p i})h:normalizedFactors (Multiset.map (fun i => span {p i}) Finset.univ.val).prod = Multiset.map (fun i => span {p i}) Finset.univ.val⊢ normalizedFactors (∏ i, span {p i}) = Multiset.map (fun i => span {p i}) Finset.univ.val All goals completed! 🐙theorem product_primary {ι : Type*} [Fintype ι] (p : ι → O) (hp : ∀ i, lambda ^ 2 ∣ p i - 1) : lambda ^ 2 ∣ (∏ i, p i) - 1 := ι:Type u_1inst✝:Fintype ιp:ι → Ohp:∀ (i : ι), lambda ^ 2 ∣ p i - 1⊢ lambda ^ 2 ∣ ∏ i, p i - 1 ι:Type u_1inst✝:Fintype ιp:ι → Ohp:∀ (i : ι), lambda ^ 2 ∣ p i - 1⊢ ∀ x ∈ Multiset.map p Finset.univ.val, lambda ^ 2 ∣ x - 1 ι:Type u_1inst✝:Fintype ιp:ι → Ohp:∀ (i : ι), lambda ^ 2 ∣ p i - 1r:ActualEisensteinCubic.Ohr:r ∈ Multiset.map p Finset.univ.val⊢ lambda ^ 2 ∣ r - 1 ι:Type u_1inst✝:Fintype ιp:ι → Ohp:∀ (i : ι), lambda ^ 2 ∣ p i - 1i:ιleft✝:i ∈ Finset.univ.valhr:p i ∈ Multiset.map p Finset.univ.val⊢ lambda ^ 2 ∣ p i - 1 All goals completed! 🐙def productPrimeIndexEquiv {ι : Type*} [Fintype ι] (p : ι → O) [∀ i, (Ideal.span {p i}).IsMaximal] (hcop : Pairwise (Function.onFun IsCoprime (fun i => Ideal.span {p i}))) : ι ≃ PrimeIndex (Ideal.span {∏ i, p i}) := ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})⊢ ι ≃ PrimeIndex (span {∏ i, p i}) ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}⊢ ι ≃ PrimeIndex (span {∏ i, p i}) ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})⊢ ι ≃ PrimeIndex (span {∏ i, p i}) ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩⊢ ι ≃ PrimeIndex (span {∏ i, p i}) ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩⊢ Function.Bijective f ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩⊢ Function.Injective fι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩⊢ Function.Surjective f ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩⊢ Function.Injective f ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩i:ιj:ιhij:f i = f j⊢ i = j All goals completed! 🐙 ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩⊢ Function.Surjective f ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩P:PrimeIndex (span {∏ i, p i})⊢ ∃ a, f a = P ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩P:PrimeIndex (span {∏ i, p i})hm:↑P ∈ normalizedFactors (span {∏ i, p i})⊢ ∃ a, f a = P ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩P:PrimeIndex (span {∏ i, p i})hm:↑P ∈ Multiset.map (fun i => span {p i}) Finset.univ.val⊢ ∃ a, f a = P ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hinj:Function.Injective fun i => span {p i}hmem:∀ (i : ι), span {p i} ∈ primeSupport (span {∏ i, p i})f:ι → PrimeIndex (span {∏ i, p i}) := fun i => ⟨span {p i}, ⋯⟩P:PrimeIndex (span {∏ i, p i})hm:↑P ∈ Multiset.map (fun i => span {p i}) Finset.univ.vali:ιleft✝:i ∈ Finset.univ.valhi:span {p i} = ↑P⊢ ∃ a, f a = P All goals completed! 🐙theorem cubicRow_product_mk {ι : Type*} [Fintype ι] (p : ι → O) [∀ i, (Ideal.span {p i}).IsMaximal] (hcop : Pairwise (Function.onFun IsCoprime (fun i => Ideal.span {p i}))) (hgood : ∀ i, lambda ∉ Ideal.span {p i}) (hI : primaryGenerator (Ideal.span {∏ i, p i}) ≠ 0) (a : O) : cubicRow (Ideal.span {∏ i, p i}) hI (Ideal.Quotient.mk (Ideal.span {∏ i, p i}) a) = ∏ i, (canonicalSextic (Ideal.span {p i}) (hgood i) ^ 2) (Ideal.Quotient.mk (Ideal.span {p i}) a) := ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hI:primaryGenerator (span {∏ i, p i}) ≠ 0a:O⊢ cubicRow (span {∏ i, p i}) hI ((Ideal.Quotient.mk (span {∏ i, p i})) a) = ∏ i, (canonicalSextic (span {p i}) ⋯ ^ 2) ((Ideal.Quotient.mk (span {p i})) a) ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hI:primaryGenerator (span {∏ i, p i}) ≠ 0a:O⊢ ∏ P, (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = ∏ i, (canonicalSextic (span {p i}) ⋯ ^ 2) ((Ideal.Quotient.mk (span {p i})) a) ι:Type u_1inst✝¹:Fintype ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hI:primaryGenerator (span {∏ i, p i}) ≠ 0a:O⊢ ∏ i, (canonicalSextic (span {p i}) ⋯ ^ 2) ((Ideal.Quotient.mk (span {p i})) a) = ∏ P, (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) All goals completed! 🐙theorem gaussTwo_eq_canonicalProductGauss {ι : Type*} [Fintype ι] (p : ι → O) (hp : ∀ i, p i ≠ 0) [∀ i, (Ideal.span {p i}).IsMaximal] (hcop : Pairwise (Function.onFun IsCoprime (fun i => Ideal.span {p i}))) (hgood : ∀ i, lambda ∉ Ideal.span {p i}) (hprimary : ∀ i, lambda ^ 2 ∣ p i - 1) (hI : primaryGenerator (Ideal.span {∏ i, p i}) ≠ 0) : gaussTwo (Ideal.span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood (fun _ => 2) := ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0⊢ gaussTwo (span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2 ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0hpall:∏ i, p i ≠ 0⊢ gaussTwo (span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2 ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p i⊢ gaussTwo (span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2 ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ithis:Finite (O ⧸ span {∏ i, p i}) := ···⊢ gaussTwo (span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2 ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ithis✝:Finite (O ⧸ span {∏ i, p i}) := ···this:Fintype (O ⧸ span {∏ i, p i}) := Fintype.ofFinite (O ⧸ span {∏ i, p i})⊢ gaussTwo (span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2 ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ithis✝¹:Finite (O ⧸ span {∏ i, p i}) := ···this✝:Fintype (O ⧸ span {∏ i, p i}) := Fintype.ofFinite (O ⧸ span {∏ i, p i})this:Finite (O ⧸ span {primaryGenerator (span {∏ i, p i})}) := ···⊢ gaussTwo (span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2 ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ithis✝²:Finite (O ⧸ span {∏ i, p i}) := ···this✝¹:Fintype (O ⧸ span {∏ i, p i}) := Fintype.ofFinite (O ⧸ span {∏ i, p i})this✝:Finite (O ⧸ span {primaryGenerator (span {∏ i, p i})}) := ···this:Fintype (O ⧸ span {primaryGenerator (span {∏ i, p i})}) := Fintype.ofFinite (O ⧸ span {primaryGenerator (span {∏ i, p i})})⊢ gaussTwo (span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2 ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ithis✝²:Finite (O ⧸ span {∏ i, p i}) := ···this✝¹:Fintype (O ⧸ span {∏ i, p i}) := Fintype.ofFinite (O ⧸ span {∏ i, p i})this✝:Finite (O ⧸ span {primaryGenerator (span {∏ i, p i})}) := ···this:Fintype (O ⧸ span {primaryGenerator (span {∏ i, p i})}) := Fintype.ofFinite (O ⧸ span {primaryGenerator (span {∏ i, p i})})e:O ⧸ span {primaryGenerator (span {∏ i, p i})} ≃+* O ⧸ span {∏ i, p i} := quotEquivOfEq ⋯⊢ gaussTwo (span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2 ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ithis✝²:Finite (O ⧸ span {∏ i, p i}) := ···this✝¹:Fintype (O ⧸ span {∏ i, p i}) := Fintype.ofFinite (O ⧸ span {∏ i, p i})this✝:Finite (O ⧸ span {primaryGenerator (span {∏ i, p i})}) := ···this:Fintype (O ⧸ span {primaryGenerator (span {∏ i, p i})}) := Fintype.ofFinite (O ⧸ span {primaryGenerator (span {∏ i, p i})})e:O ⧸ span {primaryGenerator (span {∏ i, p i})} ≃+* O ⧸ span {∏ i, p i} := quotEquivOfEq ⋯hsum:∑ x, cubicRow (span {∏ i, p i}) hI (e x) * (eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates (primaryGenerator (span {∏ i, p i})) hI) x = ∑ x, (∏ i, (canonicalSextic (span {p i}) ⋯ ^ 2) ((FiniteGaussPhase.productElementCRT p hcop) x i)) * (eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates (∏ i, p i) hpall) x⊢ gaussTwo (span {∏ i, p i}) hI = FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2 ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hI:primaryGenerator (span {∏ i, p i}) ≠ 0hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ithis✝²:Finite (O ⧸ span {∏ i, p i}) := ···this✝¹:Fintype (O ⧸ span {∏ i, p i}) := Fintype.ofFinite (O ⧸ span {∏ i, p i})this✝:Finite (O ⧸ span {primaryGenerator (span {∏ i, p i})}) := ···this:Fintype (O ⧸ span {primaryGenerator (span {∏ i, p i})}) := Fintype.ofFinite (O ⧸ span {primaryGenerator (span {∏ i, p i})})e:O ⧸ span {primaryGenerator (span {∏ i, p i})} ≃+* O ⧸ span {∏ i, p i} := quotEquivOfEq ⋯hsum:∑ x, cubicRow (span {∏ i, p i}) hI (e x) * (eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates (primaryGenerator (span {∏ i, p i})) hI) x = ∑ x, (∏ i, (canonicalSextic (span {p i}) ⋯ ^ 2) ((FiniteGaussPhase.productElementCRT p hcop) x i)) * (eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates (∏ i, p i) hpall) x⊢ (∑ x, cubicRow (span {∏ i, p i}) hI ((quotEquivOfEq ⋯) x) * (eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates (primaryGenerator (span {∏ i, p i})) hI) x) / ↑‖eisEmbedding (primaryGenerator (span {∏ i, p i}))‖ = (∑ x, (∏ i, ((fun i => canonicalSextic (span {p i}) ⋯ ^ (fun x => 2) i) i) ((FiniteGaussPhase.productElementCRT p hcop) x i)) * (eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates (∏ i, p i) ⋯) x) / ↑‖eisEmbedding (∏ i, p i)‖ All goals completed! 🐙theorem squarefreeGaussCoefficient_eq_canonicalProductCoefficient {ι : Type*} [Fintype ι] (p : ι → O) (hp : ∀ i, p i ≠ 0) [∀ i, (Ideal.span {p i}).IsMaximal] (hcop : Pairwise (Function.onFun IsCoprime (fun i => Ideal.span {p i}))) (hgood : ∀ i, lambda ∉ Ideal.span {p i}) (hprimary : ∀ i, lambda ^ 2 ∣ p i - 1) : squarefreeGaussCoefficient (Ideal.span {∏ i, p i}) = FiniteGaussPhase.canonicalProductCoefficient p hp hcop hgood := ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1⊢ squarefreeGaussCoefficient (span {∏ i, p i}) = FiniteGaussPhase.canonicalProductCoefficient p hp hcop hgood ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hpall:∏ i, p i ≠ 0⊢ squarefreeGaussCoefficient (span {∏ i, p i}) = FiniteGaussPhase.canonicalProductCoefficient p hp hcop hgood ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p i⊢ squarefreeGaussCoefficient (span {∏ i, p i}) = FiniteGaussPhase.canonicalProductCoefficient p hp hcop hgood ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ihI:primaryGenerator (span {∏ i, p i}) ≠ 0⊢ squarefreeGaussCoefficient (span {∏ i, p i}) = FiniteGaussPhase.canonicalProductCoefficient p hp hcop hgood ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ihI:primaryGenerator (span {∏ i, p i}) ≠ 0hsq:Squarefree (span {∏ i, p i})⊢ squarefreeGaussCoefficient (span {∏ i, p i}) = FiniteGaussPhase.canonicalProductCoefficient p hp hcop hgood ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1hpall:∏ i, p i ≠ 0hgen:primaryGenerator (span {∏ i, p i}) = ∏ i, p ihI:primaryGenerator (span {∏ i, p i}) ≠ 0hsq:Squarefree (span {∏ i, p i})⊢ (star (FiniteGaussPhase.angularFactor (∏ i, p i)) * FiniteGaussPhase.canonicalProductGauss p hp hcop hgood fun x => 2) = FiniteGaussPhase.canonicalProductCoefficient p hp hcop hgood All goals completed! 🐙end CompletedGaussnamespace FiniteRayExpansionvariable {R : Type*} [CommRing R] [Fintype R]noncomputable local instance : Fintype (MulChar R ℂ) := Fintype.ofFinite _def unitFourierCoeff (f : Rˣ → ℂ) (χ : MulChar R ℂ) : ℂ := (∑ u : Rˣ, f u * star (χ (u : R))) / (Fintype.card Rˣ : ℂ)theorem unit_fourier_inversion (f : Rˣ → ℂ) (v : Rˣ) : (∑ χ : MulChar R ℂ, unitFourierCoeff f χ * χ (v : R)) = f v := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:Rˣ⊢ ∑ χ, unitFourierCoeff f χ * χ ↑v = f v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ ∑ χ, unitFourierCoeff f χ * χ ↑v = f v simp_rw R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ ∑ χ, unitFourierCoeff f χ * χ ↑v = f vR:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ ∑ χ, (∑ u, f u * star (χ ↑u)) / ↑(Fintype.card Rˣ) * χ ↑v = f v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ ∑ x, (∑ u, f u * star (x ↑u)) * x ↑v / ↑(Fintype.card Rˣ) = f v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ ∑ x, (∑ i, f i * star (x ↑i) * x ↑v) / ↑(Fintype.card Rˣ) = f v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ ∑ x, (∑ x_1, f x_1 * (star (x ↑x_1) * x ↑v)) / ↑(Fintype.card Rˣ) = f v] R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ (∑ y, ∑ x, f y * (star (x ↑y) * x ↑v)) / ↑(Fintype.card Rˣ) = f v simp_rw R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ (∑ y, ∑ x, f y * (star (x ↑y) * x ↑v)) / ↑(Fintype.card Rˣ) = f vR:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ (∑ x, f x * ∑ i, star (i ↑x) * i ↑v) / ↑(Fintype.card Rˣ) = f v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ (∑ x, f x * if x = v then ↑(Fintype.card Rˣ) else 0) / ↑(Fintype.card Rˣ) = f v] R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂv:RˣhN:↑(Fintype.card Rˣ) ≠ 0⊢ f v * ↑(Fintype.card Rˣ) / ↑(Fintype.card Rˣ) = f v All goals completed! 🐙theorem norm_char_unit (χ : MulChar R ℂ) (u : Rˣ) : ‖χ (u : R)‖ = 1 := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rχ:MulChar R ℂu:Rˣ⊢ ‖χ ↑u‖ = 1 All goals completed! 🐙theorem norm_char_le_one (χ : MulChar R ℂ) (r : R) : ‖χ r‖ ≤ 1 := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rχ:MulChar R ℂr:R⊢ ‖χ r‖ ≤ 1 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rχ:MulChar R ℂr:Rhr:IsUnit r⊢ ‖χ r‖ ≤ 1R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rχ:MulChar R ℂr:Rhr:¬IsUnit r⊢ ‖χ r‖ ≤ 1 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rχ:MulChar R ℂr:Rhr:IsUnit r⊢ ‖χ r‖ ≤ 1 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rχ:MulChar R ℂu:Rˣ⊢ ‖χ ↑u‖ ≤ 1 All goals completed! 🐙 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rχ:MulChar R ℂr:Rhr:¬IsUnit r⊢ ‖χ r‖ ≤ 1 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rχ:MulChar R ℂr:Rhr:¬IsUnit r⊢ 0 ≤ 1 All goals completed! 🐙theorem unitFourierCoeff_norm_le_average (f : Rˣ → ℂ) (χ : MulChar R ℂ) : ‖unitFourierCoeff f χ‖ ≤ (∑ u : Rˣ, ‖f u‖) / (Fintype.card Rˣ : ℝ) := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂχ:MulChar R ℂ⊢ ‖unitFourierCoeff f χ‖ ≤ (∑ u, ‖f u‖) / ↑(Fintype.card Rˣ) R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂχ:MulChar R ℂ⊢ ‖∑ u, f u * star (χ ↑u)‖ / ↑(Fintype.card Rˣ) ≤ (∑ u, ‖f u‖) / ↑(Fintype.card Rˣ) apply div_le_div_of_nonneg_right _ (R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂχ:MulChar R ℂ⊢ 0 ≤ ↑(Fintype.card Rˣ) All goals completed! 🐙) calc _ ≤ ∑ u : Rˣ, ‖f u * star (χ (u : R))‖ := norm_sum_le _ _ _ = _ := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂχ:MulChar R ℂ⊢ ∑ u, ‖f u * star (χ ↑u)‖ = ∑ u, ‖f u‖ All goals completed! 🐙theorem unitFourierCoeff_norm_le (f : Rˣ → ℂ) (B : ℝ) (hf : ∀ u, ‖f u‖ ≤ B) (χ : MulChar R ℂ) : ‖unitFourierCoeff f χ‖ ≤ B := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂB:ℝhf:∀ (u : Rˣ), ‖f u‖ ≤ Bχ:MulChar R ℂ⊢ ‖unitFourierCoeff f χ‖ ≤ B R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂB:ℝhf:∀ (u : Rˣ), ‖f u‖ ≤ Bχ:MulChar R ℂhN:↑(Fintype.card Rˣ) ≠ 0⊢ ‖unitFourierCoeff f χ‖ ≤ B calc _ ≤ (∑ u : Rˣ, ‖f u‖) / (Fintype.card Rˣ : ℝ) := unitFourierCoeff_norm_le_average f χ _ ≤ (∑ _u : Rˣ, B) / (Fintype.card Rˣ : ℝ) := div_le_div_of_nonneg_right (Finset.sum_le_sum (fun u _ => hf u)) (R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂB:ℝhf:∀ (u : Rˣ), ‖f u‖ ≤ Bχ:MulChar R ℂhN:↑(Fintype.card Rˣ) ≠ 0⊢ 0 ≤ ↑(Fintype.card Rˣ) All goals completed! 🐙) _ = B := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂB:ℝhf:∀ (u : Rˣ), ‖f u‖ ≤ Bχ:MulChar R ℂhN:↑(Fintype.card Rˣ) ≠ 0⊢ (∑ _u, B) / ↑(Fintype.card Rˣ) = B R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂB:ℝhf:∀ (u : Rˣ), ‖f u‖ ≤ Bχ:MulChar R ℂhN:↑(Fintype.card Rˣ) ≠ 0⊢ ↑(Fintype.card Rˣ) * B / ↑(Fintype.card Rˣ) = B; All goals completed! 🐙theorem character_card_eq_units : Fintype.card (MulChar R ℂ) = Fintype.card Rˣ := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype R⊢ Fintype.card (MulChar R ℂ) = Fintype.card Rˣ All goals completed! 🐙theorem unitFourierCoeff_sum_norm_le (f : Rˣ → ℂ) (B : ℝ) (hf : ∀ u, ‖f u‖ ≤ B) : (∑ χ : MulChar R ℂ, ‖unitFourierCoeff f χ‖) ≤ (Fintype.card Rˣ : ℝ) * B := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂB:ℝhf:∀ (u : Rˣ), ‖f u‖ ≤ B⊢ ∑ χ, ‖unitFourierCoeff f χ‖ ≤ ↑(Fintype.card Rˣ) * B calc _ ≤ ∑ _χ : MulChar R ℂ, B := Finset.sum_le_sum (fun χ _ => unitFourierCoeff_norm_le f B hf χ) _ = _ := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂB:ℝhf:∀ (u : Rˣ), ‖f u‖ ≤ B⊢ ∑ _χ, B = ↑(Fintype.card Rˣ) * B All goals completed! 🐙theorem unitFourierCoeff_sum_norm_le_sum (f : Rˣ → ℂ) : (∑ χ : MulChar R ℂ, ‖unitFourierCoeff f χ‖) ≤ ∑ u : Rˣ, ‖f u‖ := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂ⊢ ∑ χ, ‖unitFourierCoeff f χ‖ ≤ ∑ u, ‖f u‖ R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂhN:↑(Fintype.card Rˣ) ≠ 0⊢ ∑ χ, ‖unitFourierCoeff f χ‖ ≤ ∑ u, ‖f u‖ calc _ ≤ ∑ _χ : MulChar R ℂ, (∑ u : Rˣ, ‖f u‖) / (Fintype.card Rˣ : ℝ) := Finset.sum_le_sum (fun χ _ => unitFourierCoeff_norm_le_average f χ) _ = _ := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂhN:↑(Fintype.card Rˣ) ≠ 0⊢ ∑ _χ, (∑ u, ‖f u‖) / ↑(Fintype.card Rˣ) = ∑ u, ‖f u‖ R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂhN:↑(Fintype.card Rˣ) ≠ 0⊢ ↑(Fintype.card Rˣ) * ((∑ u, ‖f u‖) / ↑(Fintype.card Rˣ)) = ∑ u, ‖f u‖ All goals completed! 🐙def zeroExtendUnits (f : Rˣ → ℂ) (r : R) : ℂ := if hr : IsUnit r then f hr.unit else 0@[simp] theorem zeroExtendUnits_unit (f : Rˣ → ℂ) (u : Rˣ) : zeroExtendUnits f (u : R) = f u := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂu:Rˣ⊢ zeroExtendUnits f ↑u = f u R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂu:Rˣ⊢ f ⋯.unit = f u R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂu:Rˣ⊢ ⋯.unit = u All goals completed! 🐙@[simp] theorem zeroExtendUnits_nonunit (f : Rˣ → ℂ) (r : R) (hr : ¬ IsUnit r) : zeroExtendUnits f r = 0 := dite_eq_right hrtheorem zeroExtendUnits_fourier (f : Rˣ → ℂ) (r : R) : zeroExtendUnits f r = ∑ χ : MulChar R ℂ, unitFourierCoeff f χ * χ r := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂr:R⊢ zeroExtendUnits f r = ∑ χ, unitFourierCoeff f χ * χ r R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂr:Rhr:IsUnit r⊢ zeroExtendUnits f r = ∑ χ, unitFourierCoeff f χ * χ rR:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂr:Rhr:¬IsUnit r⊢ zeroExtendUnits f r = ∑ χ, unitFourierCoeff f χ * χ r R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂr:Rhr:IsUnit r⊢ zeroExtendUnits f r = ∑ χ, unitFourierCoeff f χ * χ r R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂu:Rˣ⊢ zeroExtendUnits f ↑u = ∑ χ, unitFourierCoeff f χ * χ ↑u R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂu:Rˣ⊢ f u = ∑ χ, unitFourierCoeff f χ * χ ↑u All goals completed! 🐙 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂr:Rhr:¬IsUnit r⊢ zeroExtendUnits f r = ∑ χ, unitFourierCoeff f χ * χ r R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → ℂr:Rhr:¬IsUnit r⊢ 0 = ∑ χ, unitFourierCoeff f χ * χ r All goals completed! 🐙theorem zeroExtendUnits_restrict (f : R → ℂ) (r : R) : zeroExtendUnits (fun u : Rˣ => f (u : R)) r = (if IsUnit r then 1 else 0) * f r := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → ℂr:R⊢ zeroExtendUnits (fun u => f ↑u) r = (if IsUnit r then 1 else 0) * f r R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → ℂr:Rhr:IsUnit r⊢ zeroExtendUnits (fun u => f ↑u) r = (if IsUnit r then 1 else 0) * f rR:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → ℂr:Rhr:¬IsUnit r⊢ zeroExtendUnits (fun u => f ↑u) r = (if IsUnit r then 1 else 0) * f r R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → ℂr:Rhr:IsUnit r⊢ zeroExtendUnits (fun u => f ↑u) r = (if IsUnit r then 1 else 0) * f r R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → ℂu:Rˣ⊢ zeroExtendUnits (fun u => f ↑u) ↑u = (if IsUnit ↑u then 1 else 0) * f ↑u All goals completed! 🐙 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → ℂr:Rhr:¬IsUnit r⊢ zeroExtendUnits (fun u => f ↑u) r = (if IsUnit r then 1 else 0) * f r All goals completed! 🐙def unitTensorCoeff (f : Rˣ → Rˣ → ℂ) (χ η : MulChar R ℂ) : ℂ := unitFourierCoeff (fun u => unitFourierCoeff (f u) η) χtheorem unit_tensor_fourier_inversion (f : Rˣ → Rˣ → ℂ) (u v : Rˣ) : (∑ χ : MulChar R ℂ, ∑ η : MulChar R ℂ, unitTensorCoeff f χ η * χ (u : R) * η (v : R)) = f u v := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂu:Rˣv:Rˣ⊢ ∑ χ, ∑ η, unitTensorCoeff f χ η * χ ↑u * η ↑v = f u v calc _ = ∑ η : MulChar R ℂ, (∑ χ : MulChar R ℂ, unitTensorCoeff f χ η * χ (u : R)) * η (v : R) := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂu:Rˣv:Rˣ⊢ ∑ χ, ∑ η, unitTensorCoeff f χ η * χ ↑u * η ↑v = ∑ η, (∑ χ, unitTensorCoeff f χ η * χ ↑u) * η ↑v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂu:Rˣv:Rˣ⊢ ∑ y, ∑ x, unitTensorCoeff f x y * x ↑u * y ↑v = ∑ η, (∑ χ, unitTensorCoeff f χ η * χ ↑u) * η ↑v All goals completed! 🐙 _ = ∑ η : MulChar R ℂ, unitFourierCoeff (f u) η * η (v : R) := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂu:Rˣv:Rˣ⊢ ∑ η, (∑ χ, unitTensorCoeff f χ η * χ ↑u) * η ↑v = ∑ η, unitFourierCoeff (f u) η * η ↑v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂu:Rˣv:Rˣ⊢ ∀ x ∈ Finset.univ, (∑ χ, unitTensorCoeff f χ x * χ ↑u) * x ↑v = unitFourierCoeff (f u) x * x ↑v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂu:Rˣv:Rˣη:MulChar R ℂa✝:η ∈ Finset.univ⊢ (∑ χ, unitTensorCoeff f χ η * χ ↑u) * η ↑v = unitFourierCoeff (f u) η * η ↑v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂu:Rˣv:Rˣη:MulChar R ℂa✝:η ∈ Finset.univ⊢ (∑ χ, unitFourierCoeff (fun a => unitFourierCoeff (f a) η) χ * χ ↑u) * η ↑v = unitFourierCoeff (f u) η * η ↑v All goals completed! 🐙 _ = _ := unit_fourier_inversion (f u) vtheorem unitTensorCoeff_norm_le (f : Rˣ → Rˣ → ℂ) (B : ℝ) (hf : ∀ u v, ‖f u v‖ ≤ B) (χ η : MulChar R ℂ) : ‖unitTensorCoeff f χ η‖ ≤ B := unitFourierCoeff_norm_le _ B (fun u => unitFourierCoeff_norm_le (f u) B (hf u) η) χtheorem unitTensorCoeff_sum_norm_le (f : Rˣ → Rˣ → ℂ) (B : ℝ) (hf : ∀ u v, ‖f u v‖ ≤ B) : (∑ χ : MulChar R ℂ, ∑ η : MulChar R ℂ, ‖unitTensorCoeff f χ η‖) ≤ (Fintype.card Rˣ : ℝ) ^ 2 * B := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂB:ℝhf:∀ (u v : Rˣ), ‖f u v‖ ≤ B⊢ ∑ χ, ∑ η, ‖unitTensorCoeff f χ η‖ ≤ ↑(Fintype.card Rˣ) ^ 2 * B calc _ ≤ ∑ _χ : MulChar R ℂ, ∑ _η : MulChar R ℂ, B := Finset.sum_le_sum (fun χ _ => Finset.sum_le_sum (fun η _ => unitTensorCoeff_norm_le f B hf χ η)) _ = _ := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂB:ℝhf:∀ (u v : Rˣ), ‖f u v‖ ≤ B⊢ ∑ _χ, ∑ _η, B = ↑(Fintype.card Rˣ) ^ 2 * B R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂB:ℝhf:∀ (u v : Rˣ), ‖f u v‖ ≤ B⊢ ↑(Fintype.card Rˣ) * (↑(Fintype.card Rˣ) * B) = ↑(Fintype.card Rˣ) ^ 2 * B All goals completed! 🐙theorem unitTensorCoeff_sum_norm_le_sum (f : Rˣ → Rˣ → ℂ) : (∑ χ : MulChar R ℂ, ∑ η : MulChar R ℂ, ‖unitTensorCoeff f χ η‖) ≤ ∑ u : Rˣ, ∑ v : Rˣ, ‖f u v‖ := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂ⊢ ∑ χ, ∑ η, ‖unitTensorCoeff f χ η‖ ≤ ∑ u, ∑ v, ‖f u v‖ R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂ⊢ ∑ y, ∑ x, ‖unitTensorCoeff f x y‖ ≤ ∑ u, ∑ v, ‖f u v‖ calc _ ≤ ∑ η : MulChar R ℂ, ∑ u : Rˣ, ‖unitFourierCoeff (f u) η‖ := Finset.sum_le_sum (fun η _ => unitFourierCoeff_sum_norm_le_sum (fun u => unitFourierCoeff (f u) η)) _ = ∑ u : Rˣ, ∑ η : MulChar R ℂ, ‖unitFourierCoeff (f u) η‖ := Finset.sum_comm _ ≤ _ := Finset.sum_le_sum (fun u _ => unitFourierCoeff_sum_norm_le_sum (f u))def zeroExtendUnitPair (f : Rˣ → Rˣ → ℂ) (r s : R) : ℂ := zeroExtendUnits (fun u => zeroExtendUnits (f u) s) rtheorem zeroExtendUnitPair_fourier (f : Rˣ → Rˣ → ℂ) (r s : R) : zeroExtendUnitPair f r s = ∑ χ : MulChar R ℂ, ∑ η : MulChar R ℂ, unitTensorCoeff f χ η * χ r * η s := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂr:Rs:R⊢ zeroExtendUnitPair f r s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ r * η s R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂr:Rs:Rhr:IsUnit r⊢ zeroExtendUnitPair f r s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ r * η sR:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂr:Rs:Rhr:¬IsUnit r⊢ zeroExtendUnitPair f r s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ r * η s R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂr:Rs:Rhr:IsUnit r⊢ zeroExtendUnitPair f r s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ r * η s R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂs:Ru:Rˣ⊢ zeroExtendUnitPair f (↑u) s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ ↑u * η s R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂs:Ru:Rˣhs:IsUnit s⊢ zeroExtendUnitPair f (↑u) s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ ↑u * η sR:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂs:Ru:Rˣhs:¬IsUnit s⊢ zeroExtendUnitPair f (↑u) s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ ↑u * η s R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂs:Ru:Rˣhs:IsUnit s⊢ zeroExtendUnitPair f (↑u) s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ ↑u * η s R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂu:Rˣv:Rˣ⊢ zeroExtendUnitPair f ↑u ↑v = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ ↑u * η ↑v R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂu:Rˣv:Rˣ⊢ f u v = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ ↑u * η ↑v All goals completed! 🐙 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂs:Ru:Rˣhs:¬IsUnit s⊢ zeroExtendUnitPair f (↑u) s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ ↑u * η s All goals completed! 🐙 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:Rˣ → Rˣ → ℂr:Rs:Rhr:¬IsUnit r⊢ zeroExtendUnitPair f r s = ∑ χ, ∑ η, unitTensorCoeff f χ η * χ r * η s All goals completed! 🐙theorem zeroExtendUnitPair_restrict (f : R → R → ℂ) (r s : R) : zeroExtendUnitPair (fun u v : Rˣ => f (u : R) (v : R)) r s = (if IsUnit r then 1 else 0) * (if IsUnit s then 1 else 0) * f r s := R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → R → ℂr:Rs:R⊢ zeroExtendUnitPair (fun u v => f ↑u ↑v) r s = ((if IsUnit r then 1 else 0) * if IsUnit s then 1 else 0) * f r s R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → R → ℂr:Rs:Rhr:IsUnit r⊢ zeroExtendUnitPair (fun u v => f ↑u ↑v) r s = ((if IsUnit r then 1 else 0) * if IsUnit s then 1 else 0) * f r sR:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → R → ℂr:Rs:Rhr:¬IsUnit r⊢ zeroExtendUnitPair (fun u v => f ↑u ↑v) r s = ((if IsUnit r then 1 else 0) * if IsUnit s then 1 else 0) * f r s R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → R → ℂr:Rs:Rhr:IsUnit r⊢ zeroExtendUnitPair (fun u v => f ↑u ↑v) r s = ((if IsUnit r then 1 else 0) * if IsUnit s then 1 else 0) * f r s R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → R → ℂs:Ru:Rˣ⊢ zeroExtendUnitPair (fun u v => f ↑u ↑v) (↑u) s = ((if IsUnit ↑u then 1 else 0) * if IsUnit s then 1 else 0) * f (↑u) s All goals completed! 🐙 R:Type u_1inst✝¹:CommRing Rinst✝:Fintype Rf:R → R → ℂr:Rs:Rhr:¬IsUnit r⊢ zeroExtendUnitPair (fun u v => f ↑u ↑v) r s = ((if IsUnit r then 1 else 0) * if IsUnit s then 1 else 0) * f r s All goals completed! 🐙end FiniteRayExpansionopen scoped BigOperators Classicalnamespace RayFourExpansionabbrev O := ActualEisensteinCubic.Oopen ActualEisensteinCubic ConcreteTraceCRT ActualEisensteinCoordinates QuadraticGaussRayopen FiniteRayExpansionabbrev RayRing := O ⧸ Ideal.span {(4 : O)}noncomputable instance rayRingFintype : Fintype RayRing := ⊢ Fintype RayRing letI : Finite RayRing := finite_quotient_span (⊢ 4 ≠ 0 All goals completed! 🐙 : (4 : O) ≠ 0) All goals completed! 🐙abbrev RayCharacter := MulChar RayRing ℂnoncomputable instance rayCharacterFintype : Fintype RayCharacter := Fintype.ofFinite _def rayCharacter (χ : RayCharacter) (a : O) : ℂ := χ (Ideal.Quotient.mk (Ideal.span {(4 : O)}) a)theorem rayCharacter_mul (χ : RayCharacter) (a b : O) : rayCharacter χ (a * b) = rayCharacter χ a * rayCharacter χ b := χ:RayCharactera:Ob:O⊢ rayCharacter χ (a * b) = rayCharacter χ a * rayCharacter χ b All goals completed! 🐙theorem rayCharacter_eq_of_mod_four (χ : RayCharacter) (a b : O) (h : (4 : O) ∣ a - b) : rayCharacter χ a = rayCharacter χ b := χ:RayCharactera:Ob:Oh:4 ∣ a - b⊢ rayCharacter χ a = rayCharacter χ b χ:RayCharactera:Ob:Oh:4 ∣ a - b⊢ χ ((Ideal.Quotient.mk (span {4})) a) = χ ((Ideal.Quotient.mk (span {4})) b) χ:RayCharactera:Ob:Oh:4 ∣ a - b⊢ (Ideal.Quotient.mk (span {4})) a = (Ideal.Quotient.mk (span {4})) b All goals completed! 🐙def rayMask (a : O) : ℂ := if IsUnit (Ideal.Quotient.mk (Ideal.span {(4 : O)}) a) then 1 else 0theorem rayRing_card : Fintype.card RayRing = 16 := ⊢ Fintype.card RayRing = 16 h:Nat.card (ActualEisensteinCubic.O ⧸ span {↑4}) = 4 ^ 2⊢ Fintype.card RayRing = 16 simpa only [Nat.card_eq_fintype_card, Nat.cast_ofNat, show (4 : ℕ) ^ 2 = 16 ⊢ Fintype.card RayRing = 16 All goals completed! 🐙] using htheorem rayUnit_card_le : Fintype.card RayRingˣ ≤ 16 := ⊢ Fintype.card RayRingˣ ≤ 16 calc _ ≤ Fintype.card RayRing := Fintype.card_le_of_injective _ Units.val_injective _ = 16 := rayRing_cardtheorem rayCharacter_card_le : Fintype.card RayCharacter ≤ 16 := ⊢ Fintype.card RayCharacter ≤ 16 ⊢ Fintype.card RayRingˣ ≤ 16 All goals completed! 🐙def phaseCoeff (f : RayRing → ℂ) (χ : RayCharacter) : ℂ := unitFourierCoeff (fun u : RayRingˣ => f (u : RayRing)) χtheorem phase_expansion (f : RayRing → ℂ) (a : O) : rayMask a * f (Ideal.Quotient.mk (Ideal.span {(4 : O)}) a) = ∑ χ : RayCharacter, phaseCoeff f χ * rayCharacter χ a := f:RayRing → ℂa:O⊢ rayMask a * f ((Ideal.Quotient.mk (span {4})) a) = ∑ χ, phaseCoeff f χ * rayCharacter χ a f:RayRing → ℂa:O⊢ zeroExtendUnits (fun u => f ↑u) ((Ideal.Quotient.mk (span {4})) a) = ∑ χ, phaseCoeff f χ * rayCharacter χ a All goals completed! 🐙theorem phaseCoeff_norm_le (f : RayRing → ℂ) (B : ℝ) (hf : ∀ u : RayRingˣ, ‖f (u : RayRing)‖ ≤ B) (χ : RayCharacter) : ‖phaseCoeff f χ‖ ≤ B := unitFourierCoeff_norm_le _ B hf χtheorem phaseCoeff_sum_norm_le (f : RayRing → ℂ) (B : ℝ) (hf : ∀ u : RayRingˣ, ‖f (u : RayRing)‖ ≤ B) : (∑ χ : RayCharacter, ‖phaseCoeff f χ‖) ≤ 16 * B := f:RayRing → ℂB:ℝhf:∀ (u : RayRingˣ), ‖f ↑u‖ ≤ B⊢ ∑ χ, ‖phaseCoeff f χ‖ ≤ 16 * B f:RayRing → ℂB:ℝhf:∀ (u : RayRingˣ), ‖f ↑u‖ ≤ BhB:0 ≤ B⊢ ∑ χ, ‖phaseCoeff f χ‖ ≤ 16 * B exact (unitFourierCoeff_sum_norm_le _ B hf).trans (mul_le_mul_of_nonneg_right (f:RayRing → ℂB:ℝhf:∀ (u : RayRingˣ), ‖f ↑u‖ ≤ BhB:0 ≤ B⊢ ↑(Fintype.card RayRingˣ) ≤ 16 All goals completed! 🐙) hB)def pairCoeff (f : RayRing → RayRing → ℂ) (χ η : RayCharacter) : ℂ := unitTensorCoeff (fun u v : RayRingˣ => f (u : RayRing) (v : RayRing)) χ ηtheorem pair_phase_expansion (f : RayRing → RayRing → ℂ) (a b : O) : rayMask a * rayMask b * f (Ideal.Quotient.mk (Ideal.span {(4 : O)}) a) (Ideal.Quotient.mk (Ideal.span {(4 : O)}) b) = ∑ χ : RayCharacter, ∑ η : RayCharacter, pairCoeff f χ η * rayCharacter χ a * rayCharacter η b := f:RayRing → RayRing → ℂa:Ob:O⊢ rayMask a * rayMask b * f ((Ideal.Quotient.mk (span {4})) a) ((Ideal.Quotient.mk (span {4})) b) = ∑ χ, ∑ η, pairCoeff f χ η * rayCharacter χ a * rayCharacter η b f:RayRing → RayRing → ℂa:Ob:O⊢ zeroExtendUnitPair (fun u v => f ↑u ↑v) ((Ideal.Quotient.mk (span {4})) a) ((Ideal.Quotient.mk (span {4})) b) = ∑ χ, ∑ η, pairCoeff f χ η * rayCharacter χ a * rayCharacter η b All goals completed! 🐙theorem pairCoeff_norm_le (f : RayRing → RayRing → ℂ) (B : ℝ) (hf : ∀ u v : RayRingˣ, ‖f (u : RayRing) (v : RayRing)‖ ≤ B) (χ η : RayCharacter) : ‖pairCoeff f χ η‖ ≤ B := unitTensorCoeff_norm_le _ B hf χ ηtheorem pairCoeff_sum_norm_le (f : RayRing → RayRing → ℂ) (B : ℝ) (hf : ∀ u v : RayRingˣ, ‖f (u : RayRing) (v : RayRing)‖ ≤ B) : (∑ χ : RayCharacter, ∑ η : RayCharacter, ‖pairCoeff f χ η‖) ≤ 256 * B := f:RayRing → RayRing → ℂB:ℝhf:∀ (u v : RayRingˣ), ‖f ↑u ↑v‖ ≤ B⊢ ∑ χ, ∑ η, ‖pairCoeff f χ η‖ ≤ 256 * B f:RayRing → RayRing → ℂB:ℝhf:∀ (u v : RayRingˣ), ‖f ↑u ↑v‖ ≤ BhB:0 ≤ B⊢ ∑ χ, ∑ η, ‖pairCoeff f χ η‖ ≤ 256 * B f:RayRing → RayRing → ℂB:ℝhf:∀ (u v : RayRingˣ), ‖f ↑u ↑v‖ ≤ BhB:0 ≤ Bhcard:↑(Fintype.card RayRingˣ) ^ 2 ≤ 256⊢ ∑ χ, ∑ η, ‖pairCoeff f χ η‖ ≤ 256 * B All goals completed! 🐙theorem quadraticRayValue_bounds (r : EisensteinEPrimaryPhase.Coord) : ‖quadraticRayValue r‖ ≤ 2 ∧ ‖(quadraticRayValue r)⁻¹‖ ≤ 1 := r:EisensteinEPrimaryPhase.Coord⊢ ‖quadraticRayValue r‖ ≤ 2 ∧ ‖(quadraticRayValue r)⁻¹‖ ≤ 1 a:ZMod 4b:ZMod 4⊢ ‖quadraticRayValue (a, b)‖ ≤ 2 ∧ ‖(quadraticRayValue (a, b))⁻¹‖ ≤ 1 b:ZMod 4⊢ ‖quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, b)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, b))⁻¹‖ ≤ 1b:ZMod 4⊢ ‖quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, b)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, b))⁻¹‖ ≤ 1b:ZMod 4⊢ ‖quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, b)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, b))⁻¹‖ ≤ 1b:ZMod 4⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, b)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, b))⁻¹‖ ≤ 1 b:ZMod 4⊢ ‖quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, b)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, b))⁻¹‖ ≤ 1b:ZMod 4⊢ ‖quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, b)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, b))⁻¹‖ ≤ 1b:ZMod 4⊢ ‖quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, b)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, b))⁻¹‖ ≤ 1b:ZMod 4⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, b)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, b))⁻¹‖ ≤ 1 ⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨0, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨0, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨1, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨1, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨2, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨2, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨3, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨3, ⋯⟩))⁻¹‖ ≤ 1 ⊢ ‖quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨0, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨0, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨1, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨1, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨2, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨2, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨3, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨0, ⋯⟩, (fun i => i) ⟨3, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨0, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨1, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨2, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨3, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨1, ⋯⟩, (fun i => i) ⟨3, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨0, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨1, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨2, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨3, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨2, ⋯⟩, (fun i => i) ⟨3, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨0, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨0, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨1, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨1, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨2, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨2, ⋯⟩))⁻¹‖ ≤ 1⊢ ‖quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨3, ⋯⟩)‖ ≤ 2 ∧ ‖(quadraticRayValue ((fun i => i) ⟨3, ⋯⟩, (fun i => i) ⟨3, ⋯⟩))⁻¹‖ ≤ 1 All goals completed! 🐙 ⊢ ‖1 + -I + 1 + I‖ / 2 ≤ 2 ∧ 2 / ‖1 + -I + 1 + I‖ ≤ 1⊢ ‖1 + I + 1 + -I‖ / 2 ≤ 2 ∧ 2 / ‖1 + I + 1 + -I‖ ≤ 1⊢ ‖1 + I + I + -1‖ / 2 ≤ 2 ∧ 2 / ‖1 + I + I + -1‖ ≤ 1⊢ ‖1 + -I + -I + -1‖ / 2 ≤ 2 ∧ 2 / ‖1 + -I + -I + -1‖ ≤ 1 ⊢ ‖-(I * 2)‖ * (1 / 2) ≤ 2 ∧ ‖-(I * 2)‖⁻¹ * 2 ≤ 1 ⊢ ‖2‖ * (1 / 2) ≤ 2 ∧ ‖2‖⁻¹ * 2 ≤ 1⊢ ‖2‖ * (1 / 2) ≤ 2 ∧ ‖2‖⁻¹ * 2 ≤ 1⊢ ‖I * 2‖ * (1 / 2) ≤ 2 ∧ ‖I * 2‖⁻¹ * 2 ≤ 1⊢ ‖-(I * 2)‖ * (1 / 2) ≤ 2 ∧ ‖-(I * 2)‖⁻¹ * 2 ≤ 1 All goals completed! 🐙theorem fixedGQuotientValue_norm_le_two (r : RayRing) : ‖fixedGQuotientValue r‖ ≤ 2 := r:RayRing⊢ ‖fixedGQuotientValue r‖ ≤ 2 r:RayRingthis:Fintype (O ⧸ cubicTwoIdeal) := Fintype.ofFinite (O ⧸ cubicTwoIdeal)⊢ ‖fixedGQuotientValue r‖ ≤ 2 r:RayRingthis:Fintype (O ⧸ cubicTwoIdeal) := Fintype.ofFinite (O ⧸ cubicTwoIdeal)χ:MulChar (O ⧸ cubicTwoIdeal) ℂ := (cubicChar cubicTwoIdeal cubicTwoIdeal_good).ringHomComp eisEmbedding⊢ ‖fixedGQuotientValue r‖ ≤ 2 r:RayRingthis:Fintype (O ⧸ cubicTwoIdeal) := Fintype.ofFinite (O ⧸ cubicTwoIdeal)χ:MulChar (O ⧸ cubicTwoIdeal) ℂ := (cubicChar cubicTwoIdeal cubicTwoIdeal_good).ringHomComp eisEmbeddingx:ActualEisensteinCubic.O ⧸ cubicTwoIdeal := (Ideal.Quotient.mk cubicTwoIdeal) (ActualEisensteinCoordinates.lift (residueQuotientFour r))⊢ ‖fixedGQuotientValue r‖ ≤ 2 r:RayRingthis:Fintype (O ⧸ cubicTwoIdeal) := Fintype.ofFinite (O ⧸ cubicTwoIdeal)χ:MulChar (O ⧸ cubicTwoIdeal) ℂ := (cubicChar cubicTwoIdeal cubicTwoIdeal_good).ringHomComp eisEmbeddingx:ActualEisensteinCubic.O ⧸ cubicTwoIdeal := (Ideal.Quotient.mk cubicTwoIdeal) (ActualEisensteinCoordinates.lift (residueQuotientFour r))hc:‖(χ x)⁻¹‖ ≤ 1⊢ ‖fixedGQuotientValue r‖ ≤ 2 r:RayRingthis:Fintype (O ⧸ cubicTwoIdeal) := Fintype.ofFinite (O ⧸ cubicTwoIdeal)χ:MulChar (O ⧸ cubicTwoIdeal) ℂ := (cubicChar cubicTwoIdeal cubicTwoIdeal_good).ringHomComp eisEmbeddingx:ActualEisensteinCubic.O ⧸ cubicTwoIdeal := (Ideal.Quotient.mk cubicTwoIdeal) (ActualEisensteinCoordinates.lift (residueQuotientFour r))hc:‖(χ x)⁻¹‖ ≤ 1⊢ ‖(χ x)⁻¹ * quadraticRayValue (residueQuotientFour r)‖ ≤ 2 r:RayRingthis:Fintype (O ⧸ cubicTwoIdeal) := Fintype.ofFinite (O ⧸ cubicTwoIdeal)χ:MulChar (O ⧸ cubicTwoIdeal) ℂ := (cubicChar cubicTwoIdeal cubicTwoIdeal_good).ringHomComp eisEmbeddingx:ActualEisensteinCubic.O ⧸ cubicTwoIdeal := (Ideal.Quotient.mk cubicTwoIdeal) (ActualEisensteinCoordinates.lift (residueQuotientFour r))hc:‖(χ x)⁻¹‖ ≤ 1⊢ ‖(χ x)⁻¹‖ * ‖quadraticRayValue (residueQuotientFour r)‖ ≤ 2 calc _ ≤ 1 * 2 := mul_le_mul hc (quadraticRayValue_bounds _).1 (norm_nonneg _) (r:RayRingthis:Fintype (O ⧸ cubicTwoIdeal) := Fintype.ofFinite (O ⧸ cubicTwoIdeal)χ:MulChar (O ⧸ cubicTwoIdeal) ℂ := (cubicChar cubicTwoIdeal cubicTwoIdeal_good).ringHomComp eisEmbeddingx:ActualEisensteinCubic.O ⧸ cubicTwoIdeal := (Ideal.Quotient.mk cubicTwoIdeal) (ActualEisensteinCoordinates.lift (residueQuotientFour r))hc:‖(χ x)⁻¹‖ ≤ 1⊢ 0 ≤ 1 All goals completed! 🐙) _ = 2 := r:RayRingthis:Fintype (O ⧸ cubicTwoIdeal) := Fintype.ofFinite (O ⧸ cubicTwoIdeal)χ:MulChar (O ⧸ cubicTwoIdeal) ℂ := (cubicChar cubicTwoIdeal cubicTwoIdeal_good).ringHomComp eisEmbeddingx:ActualEisensteinCubic.O ⧸ cubicTwoIdeal := (Ideal.Quotient.mk cubicTwoIdeal) (ActualEisensteinCoordinates.lift (residueQuotientFour r))hc:‖(χ x)⁻¹‖ ≤ 1⊢ 1 * 2 = 2 All goals completed! 🐙def gCoeff : RayCharacter → ℂ := phaseCoeff fixedGQuotientValuetheorem gCoeff_norm_le_two (χ : RayCharacter) : ‖gCoeff χ‖ ≤ 2 := phaseCoeff_norm_le _ 2 (fun u => fixedGQuotientValue_norm_le_two u) χtheorem gCoeff_sum_norm_le : (∑ χ : RayCharacter, ‖gCoeff χ‖) ≤ 32 := ⊢ ∑ χ, ‖gCoeff χ‖ ≤ 32 exact (phaseCoeff_sum_norm_le _ 2 (fun u => fixedGQuotientValue_norm_le_two u)).trans_eq (⊢ 16 * 2 = 32 All goals completed! 🐙)theorem fixedG_character_expansion (a : O) : rayMask a * fixedGQuotientValue (Ideal.Quotient.mk (Ideal.span {(4 : O)}) a) = ∑ χ : RayCharacter, gCoeff χ * rayCharacter χ a := phase_expansion _ adef crossQuotientPhase (r s : RayRing) : ℂ := MixedCrossSeparation.quadraticRayPair (residueQuotientFour r) (residueQuotientFour s)theorem crossQuotientPhase_norm_le_two (r s : RayRing) : ‖crossQuotientPhase r s‖ ≤ 2 := r:RayRings:RayRing⊢ ‖crossQuotientPhase r s‖ ≤ 2 r:RayRings:RayRing⊢ ‖quadraticRayValue (EisensteinEPrimaryPhase.mul (residueQuotientFour r) (residueQuotientFour s)) / (quadraticRayValue (residueQuotientFour r) * quadraticRayValue (residueQuotientFour s))‖ ≤ 2 r:RayRings:RayRing⊢ ‖quadraticRayValue (EisensteinEPrimaryPhase.mul (residueQuotientFour r) (residueQuotientFour s))‖ * (‖(quadraticRayValue (residueQuotientFour s))⁻¹‖ * ‖(quadraticRayValue (residueQuotientFour r))⁻¹‖) ≤ 2 calc _ ≤ 2 * (1 * 1) := mul_le_mul (quadraticRayValue_bounds _).1 (mul_le_mul (quadraticRayValue_bounds _).2 (quadraticRayValue_bounds _).2 (norm_nonneg _) (r:RayRings:RayRing⊢ 0 ≤ 1 All goals completed! 🐙)) (mul_nonneg (norm_nonneg _) (norm_nonneg _)) (r:RayRings:RayRing⊢ 0 ≤ 2 All goals completed! 🐙) _ = 2 := r:RayRings:RayRing⊢ 2 * (1 * 1) = 2 All goals completed! 🐙def crossCoeff : RayCharacter → RayCharacter → ℂ := pairCoeff crossQuotientPhasetheorem crossCoeff_norm_le_two (χ η : RayCharacter) : ‖crossCoeff χ η‖ ≤ 2 := pairCoeff_norm_le _ 2 (fun u v => crossQuotientPhase_norm_le_two u v) χ ηtheorem crossCoeff_sum_norm_le : (∑ χ : RayCharacter, ∑ η : RayCharacter, ‖crossCoeff χ η‖) ≤ 512 := ⊢ ∑ χ, ∑ η, ‖crossCoeff χ η‖ ≤ 512 exact (pairCoeff_sum_norm_le _ 2 (fun u v => crossQuotientPhase_norm_le_two u v)).trans_eq (⊢ 256 * 2 = 512 All goals completed! 🐙)theorem quadraticRayPair_character_expansion (a b : O) : rayMask a * rayMask b * MixedCrossSeparation.quadraticRayPair (residue a) (residue b) = ∑ χ : RayCharacter, ∑ η : RayCharacter, crossCoeff χ η * rayCharacter χ a * rayCharacter η b := a:Ob:O⊢ rayMask a * rayMask b * MixedCrossSeparation.quadraticRayPair (residue a) (residue b) = ∑ χ, ∑ η, crossCoeff χ η * rayCharacter χ a * rayCharacter η b All goals completed! 🐙end RayFourExpansionendend OAI