import OAI.NumberTheory.DirichletL.QuadraticSieve.CrossSeparationnamespace 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 UniqueFactorizationMonoidnamespace IdealMobiusDivisorSumabbrev O := ActualEisensteinCubic.Odef idealDivisors (I : Ideal O) : Finset (Ideal O) := (Ideal.finite_setOfPred_absNorm_le (S := O) (Ideal.absNorm I)).toFinset.filter (fun J => J ∣ I)theorem mem_idealDivisors {I J : Ideal O} (hI : I ≠ ⊥) : J ∈ idealDivisors I ↔ J ∣ I := byI:Ideal OJ:Ideal OhI:I ≠ ⊥⊢ J ∈ idealDivisors I ↔ J ∣ I simp only [idealDivisors, Finset.mem_filter, Set.Finite.mem_toFinset, Set.mem_ofPred_eq]I:Ideal OJ:Ideal OhI:I ≠ ⊥⊢ absNorm J ≤ absNorm I ∧ J ∣ I ↔ J ∣ I constructormpI:Ideal OJ:Ideal OhI:I ≠ ⊥⊢ absNorm J ≤ absNorm I ∧ J ∣ I → J ∣ ImprI:Ideal OJ:Ideal OhI:I ≠ ⊥⊢ J ∣ I → absNorm J ≤ absNorm I ∧ J ∣ I ·mpI:Ideal OJ:Ideal OhI:I ≠ ⊥⊢ absNorm J ≤ absNorm I ∧ J ∣ I → J ∣ I exact And.rightAll goals completed! 🐙 ·mprI:Ideal OJ:Ideal OhI:I ≠ ⊥⊢ J ∣ I → absNorm J ≤ absNorm I ∧ J ∣ I intro hJImprI:Ideal OJ:Ideal OhI:I ≠ ⊥hJI:J ∣ I⊢ absNorm J ≤ absNorm I ∧ J ∣ I have hn : 0 < Ideal.absNorm I := Nat.pos_iff_ne_zero.mpr (fun hz => hI (Ideal.absNorm_eq_zero_iff.mp hz))mprI:Ideal OJ:Ideal OhI:I ≠ ⊥hJI:J ∣ Ihn:0 < absNorm I⊢ absNorm J ≤ absNorm I ∧ J ∣ I exact ⟨Nat.le_of_dvd hn (map_dvd Ideal.absNorm hJI), hJI⟩All goals completed! 🐙def primeSupport (I : Ideal O) : Finset (Ideal O) := (normalizedFactors I).toFinsettheorem support_prime {I : Ideal O} {P : Ideal O} (hP : P ∈ primeSupport I) : Prime P := prime_of_normalized_factor P (Multiset.mem_toFinset.mp hP)theorem support_product_ne_zero {I : Ideal O} {S : Finset (Ideal O)} (hS : S ⊆ primeSupport I) : (∏ P ∈ S, P) ≠ 0 := Finset.prod_ne_zero_iff.mpr (fun _P hP => (support_prime (hS hP)).ne_zero)theorem factors_support_product {I : Ideal O} {S : Finset (Ideal O)} (hS : S ⊆ primeSupport I) : normalizedFactors (∏ P ∈ S, P) = S.val := byI:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ normalizedFactors (∏ P ∈ S, P) = S.val have hp : ∀ P ∈ S.val, Prime P := fun P hP => support_prime (hS hP)I:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport Ihp:∀ P ∈ S.val, Prime P⊢ normalizedFactors (∏ P ∈ S, P) = S.val simpa using normalizedFactors_prod_of_prime hpAll goals completed! 🐙theorem squarefree_support_product {I : Ideal O} {S : Finset (Ideal O)} (hS : S ⊆ primeSupport I) : Squarefree (∏ P ∈ S, P) := byI:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ Squarefree (∏ P ∈ S, P) apply (squarefree_iff_nodup_normalizedFactors (support_product_ne_zero hS)).mprI:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ (normalizedFactors (∏ P ∈ S, P)).Nodup rw [factors_support_product hSI:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ S.val.Nodup]I:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ S.val.Nodup exact S.nodupAll goals completed! 🐙theorem support_product_dvd {I : Ideal O} (hI : I ≠ ⊥) {S : Finset (Ideal O)} (hS : S ⊆ primeSupport I) : (∏ P ∈ S, P) ∣ I := byI:Ideal OhI:I ≠ ⊥S:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ ∏ P ∈ S, P ∣ I apply (dvd_iff_normalizedFactors_le_normalizedFactors (support_product_ne_zero hS) hI).mprI:Ideal OhI:I ≠ ⊥S:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ normalizedFactors (∏ P ∈ S, P) ≤ normalizedFactors I rw [factors_support_product hSI:Ideal OhI:I ≠ ⊥S:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ S.val ≤ normalizedFactors I]I:Ideal OhI:I ≠ ⊥S:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ S.val ≤ normalizedFactors I apply (Multiset.le_iff_subset S.nodup).mprI:Ideal OhI:I ≠ ⊥S:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ S.val ⊆ normalizedFactors I intro P hPI:Ideal OhI:I ≠ ⊥S:Finset (Ideal O)hS:S ⊆ primeSupport IP:Ideal OhP:P ∈ S.val⊢ P ∈ normalizedFactors I exact Multiset.mem_toFinset.mp (hS hP)All goals completed! 🐙theorem moebius_support_product {I : Ideal O} {S : Finset (Ideal O)} (hS : S ⊆ primeSupport I) : (moebius (∏ P ∈ S, P) : ℂ) = (-1 : ℂ) ^ S.card := byI:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ ↑(moebius (∏ P ∈ S, P)) = (-1) ^ #S rw [(squarefree_support_product hS).moebius_eq,I:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ ↑((-1) ^ (factors (∏ P ∈ S, P)).card) = (-1) ^ #S factors_eq_normalizedFactors,I:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ ↑((-1) ^ (normalizedFactors (∏ P ∈ S, P)).card) = (-1) ^ #S factors_support_product hSI:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ ↑((-1) ^ S.val.card) = (-1) ^ #S]I:Ideal OS:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ ↑((-1) ^ S.val.card) = (-1) ^ #S simpAll goals completed! 🐙theorem support_product_injective {I : Ideal O} {S T : Finset (Ideal O)} (hS : S ⊆ primeSupport I) (hT : T ⊆ primeSupport I) (h : (∏ P ∈ S, P) = ∏ P ∈ T, P) : S = T := byI:Ideal OS:Finset (Ideal O)T:Finset (Ideal O)hS:S ⊆ primeSupport IhT:T ⊆ primeSupport Ih:∏ P ∈ S, P = ∏ P ∈ T, P⊢ S = T have hf := congrArg normalizedFactors hI:Ideal OS:Finset (Ideal O)T:Finset (Ideal O)hS:S ⊆ primeSupport IhT:T ⊆ primeSupport Ih:∏ P ∈ S, P = ∏ P ∈ T, Phf:normalizedFactors (∏ P ∈ S, P) = normalizedFactors (∏ P ∈ T, P)⊢ S = T rw [factors_support_product hS,I:Ideal OS:Finset (Ideal O)T:Finset (Ideal O)hS:S ⊆ primeSupport IhT:T ⊆ primeSupport Ih:∏ P ∈ S, P = ∏ P ∈ T, Phf:S.val = normalizedFactors (∏ P ∈ T, P)⊢ S = T factors_support_product hTI:Ideal OS:Finset (Ideal O)T:Finset (Ideal O)hS:S ⊆ primeSupport IhT:T ⊆ primeSupport Ih:∏ P ∈ S, P = ∏ P ∈ T, Phf:S.val = T.val⊢ S = T] at hfI:Ideal OS:Finset (Ideal O)T:Finset (Ideal O)hS:S ⊆ primeSupport IhT:T ⊆ primeSupport Ih:∏ P ∈ S, P = ∏ P ∈ T, Phf:S.val = T.val⊢ S = T exact Finset.val_inj.mp hfAll goals completed! 🐙theorem squarefree_divisor_support {I J : Ideal O} (hI : I ≠ ⊥) (hJ : Squarefree J) (hJI : J ∣ I) : primeSupport J ⊆ primeSupport I := byI:Ideal OJ:Ideal OhI:I ≠ ⊥hJ:Squarefree JhJI:J ∣ I⊢ primeSupport J ⊆ primeSupport I have hf := (dvd_iff_normalizedFactors_le_normalizedFactors hJ.ne_zero hI).mp hJII:Ideal OJ:Ideal OhI:I ≠ ⊥hJ:Squarefree JhJI:J ∣ Ihf:normalizedFactors J ≤ normalizedFactors I⊢ primeSupport J ⊆ primeSupport I intro P hPI:Ideal OJ:Ideal OhI:I ≠ ⊥hJ:Squarefree JhJI:J ∣ Ihf:normalizedFactors J ≤ normalizedFactors IP:Ideal OhP:P ∈ primeSupport J⊢ P ∈ primeSupport I exact Multiset.mem_toFinset.mpr (Multiset.mem_of_le hf (Multiset.mem_toFinset.mp hP))All goals completed! 🐙theorem squarefree_support_product_self {J : Ideal O} (hJ : Squarefree J) : (∏ P ∈ primeSupport J, P) = J := byJ:Ideal OhJ:Squarefree J⊢ ∏ P ∈ primeSupport J, P = J have hn : (normalizedFactors J).Nodup := (squarefree_iff_nodup_normalizedFactors hJ.ne_zero).mp hJJ:Ideal OhJ:Squarefree Jhn:(normalizedFactors J).Nodup⊢ ∏ P ∈ primeSupport J, P = J have hv : (primeSupport J).val = normalizedFactors J := by simpa only [primeSupport, Multiset.toFinset_val] using hn.dedupJ:Ideal OhJ:Squarefree Jhn:(normalizedFactors J).Noduphv:(primeSupport J).val = normalizedFactors J⊢ ∏ P ∈ primeSupport J, P = J calc _ = (primeSupport J).val.prod := (Finset.prod_val _).symm _ = (normalizedFactors J).prod := byJ:Ideal OhJ:Squarefree Jhn:(normalizedFactors J).Noduphv:(primeSupport J).val = normalizedFactors J⊢ (primeSupport J).val.prod = (normalizedFactors J).prod rw [hvJ:Ideal OhJ:Squarefree Jhn:(normalizedFactors J).Noduphv:(primeSupport J).val = normalizedFactors J⊢ (normalizedFactors J).prod = (normalizedFactors J).prod]All goals completed! 🐙 _ = J := Ideal.prod_normalizedFactors_eq_self hJ.ne_zerotheorem squarefree_divisors_eq_image (I : Ideal O) (hI : I ≠ ⊥) : (idealDivisors I).filter Squarefree = (primeSupport I).powerset.image (fun S => ∏ P ∈ S, P) := byI:Ideal OhI:I ≠ ⊥⊢ filter Squarefree (idealDivisors I) = Finset.image (fun S => ∏ P ∈ S, P) (primeSupport I).powerset ext JI:Ideal OhI:I ≠ ⊥J:Ideal O⊢ J ∈ filter Squarefree (idealDivisors I) ↔ J ∈ Finset.image (fun S => ∏ P ∈ S, P) (primeSupport I).powerset simp only [Finset.mem_filter, mem_idealDivisors hI, Finset.mem_image, Finset.mem_powerset]I:Ideal OhI:I ≠ ⊥J:Ideal O⊢ J ∣ I ∧ Squarefree J ↔ ∃ a ⊆ primeSupport I, ∏ P ∈ a, P = J constructormpI:Ideal OhI:I ≠ ⊥J:Ideal O⊢ J ∣ I ∧ Squarefree J → ∃ a ⊆ primeSupport I, ∏ P ∈ a, P = JmprI:Ideal OhI:I ≠ ⊥J:Ideal O⊢ (∃ a ⊆ primeSupport I, ∏ P ∈ a, P = J) → J ∣ I ∧ Squarefree J ·mpI:Ideal OhI:I ≠ ⊥J:Ideal O⊢ J ∣ I ∧ Squarefree J → ∃ a ⊆ primeSupport I, ∏ P ∈ a, P = J rintro ⟨hJI, hJ⟩mpI:Ideal OhI:I ≠ ⊥J:Ideal OhJI:J ∣ IhJ:Squarefree J⊢ ∃ a ⊆ primeSupport I, ∏ P ∈ a, P = J exact ⟨primeSupport J, squarefree_divisor_support hI hJ hJI, squarefree_support_product_self hJ⟩All goals completed! 🐙 ·mprI:Ideal OhI:I ≠ ⊥J:Ideal O⊢ (∃ a ⊆ primeSupport I, ∏ P ∈ a, P = J) → J ∣ I ∧ Squarefree J rintro ⟨S, hS, rfl⟩mprI:Ideal OhI:I ≠ ⊥S:Finset (Ideal O)hS:S ⊆ primeSupport I⊢ ∏ P ∈ S, P ∣ I ∧ Squarefree (∏ P ∈ S, P) exact ⟨support_product_dvd hI hS, squarefree_support_product hS⟩All goals completed! 🐙theorem primeSupport_empty_iff (I : Ideal O) (hI : I ≠ ⊥) : primeSupport I = ∅ ↔ I = ⊤ := byI:Ideal OhI:I ≠ ⊥⊢ primeSupport I = ∅ ↔ I = ⊤ constructormpI:Ideal OhI:I ≠ ⊥⊢ primeSupport I = ∅ → I = ⊤mprI:Ideal OhI:I ≠ ⊥⊢ I = ⊤ → primeSupport I = ∅ ·mpI:Ideal OhI:I ≠ ⊥⊢ primeSupport I = ∅ → I = ⊤ intro hmpI:Ideal OhI:I ≠ ⊥h:primeSupport I = ∅⊢ I = ⊤ have hz : normalizedFactors I = 0 := byI:Ideal OhI:I ≠ ⊥⊢ primeSupport I = ∅ ↔ I = ⊤ apply Multiset.toFinset_eq_empty.mpI:Ideal OhI:I ≠ ⊥h:primeSupport I = ∅⊢ (normalizedFactors I).toFinset = ∅ exact hmpI:Ideal OhI:I ≠ ⊥h:primeSupport I = ∅hz:normalizedFactors I = 0⊢ I = ⊤ have hp := Ideal.prod_normalizedFactors_eq_self hImpI:Ideal OhI:I ≠ ⊥h:primeSupport I = ∅hz:normalizedFactors I = 0hp:(normalizedFactors I).prod = I⊢ I = ⊤ rw [hz,mpI:Ideal OhI:I ≠ ⊥h:primeSupport I = ∅hz:normalizedFactors I = 0hp:Multiset.prod 0 = I⊢ I = ⊤ Multiset.prod_zerompI:Ideal OhI:I ≠ ⊥h:primeSupport I = ∅hz:normalizedFactors I = 0hp:1 = I⊢ I = ⊤] at hpmpI:Ideal OhI:I ≠ ⊥h:primeSupport I = ∅hz:normalizedFactors I = 0hp:1 = I⊢ I = ⊤ simpa only [Ideal.one_eq_top] using hp.symmAll goals completed! 🐙 ·mprI:Ideal OhI:I ≠ ⊥⊢ I = ⊤ → primeSupport I = ∅ intro hmprI:Ideal OhI:I ≠ ⊥h:I = ⊤⊢ primeSupport I = ∅ subst ImprhI:⊤ ≠ ⊥⊢ primeSupport ⊤ = ∅ simp [primeSupport, ← Ideal.one_eq_top]All goals completed! 🐙theorem sum_moebius_divisors (I : Ideal O) (hI : I ≠ ⊥) : (∑ J ∈ idealDivisors I, (moebius J : ℂ)) = if I = ⊤ then 1 else 0 := byI:Ideal OhI:I ≠ ⊥⊢ ∑ J ∈ idealDivisors I, ↑(moebius J) = if I = ⊤ then 1 else 0 have hfilter : (∑ J ∈ idealDivisors I, (moebius J : ℂ)) = ∑ J ∈ (idealDivisors I).filter Squarefree, (moebius J : ℂ) := by symmI:Ideal OhI:I ≠ ⊥⊢ ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J) = ∑ J ∈ idealDivisors I, ↑(moebius J) apply Finset.sum_subset (Finset.filter_subset _ _)I:Ideal OhI:I ≠ ⊥⊢ ∀ x ∈ idealDivisors I, x ∉ filter Squarefree (idealDivisors I) → ↑(moebius x) = 0 intro J hJ hnotI:Ideal OhI:I ≠ ⊥J:Ideal OhJ:J ∈ idealDivisors Ihnot:J ∉ filter Squarefree (idealDivisors I)⊢ ↑(moebius J) = 0 have hn : ¬ Squarefree J := byI:Ideal OhI:I ≠ ⊥⊢ ∑ J ∈ idealDivisors I, ↑(moebius J) = if I = ⊤ then 1 else 0 simpa [hJ] using hnotI:Ideal OhI:I ≠ ⊥J:Ideal OhJ:J ∈ idealDivisors Ihnot:J ∉ filter Squarefree (idealDivisors I)hn:¬Squarefree J⊢ ↑(moebius J) = 0 rw [moebius_of_not_squarefree hn,I:Ideal OhI:I ≠ ⊥J:Ideal OhJ:J ∈ idealDivisors Ihnot:J ∉ filter Squarefree (idealDivisors I)hn:¬Squarefree J⊢ ↑0 = 0 Int.cast_zeroI:Ideal OhI:I ≠ ⊥J:Ideal OhJ:J ∈ idealDivisors Ihnot:J ∉ filter Squarefree (idealDivisors I)hn:¬Squarefree J⊢ 0 = 0]I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)⊢ ∑ J ∈ idealDivisors I, ↑(moebius J) = if I = ⊤ then 1 else 0 rw [hfilter,I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)⊢ ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J) = if I = ⊤ then 1 else 0 squarefree_divisors_eq_image I hI,I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)⊢ ∑ J ∈ Finset.image (fun S => ∏ P ∈ S, P) (primeSupport I).powerset, ↑(moebius J) = if I = ⊤ then 1 else 0 Finset.sum_imageI:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)⊢ ∑ x ∈ (primeSupport I).powerset, ↑(moebius (∏ P ∈ x, P)) = if I = ⊤ then 1 else 0I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)⊢ InjOn (fun S => ∏ P ∈ S, P) ↑(primeSupport I).powerset]I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)⊢ ∑ x ∈ (primeSupport I).powerset, ↑(moebius (∏ P ∈ x, P)) = if I = ⊤ then 1 else 0I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)⊢ InjOn (fun S => ∏ P ∈ S, P) ↑(primeSupport I).powerset ·I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)⊢ ∑ x ∈ (primeSupport I).powerset, ↑(moebius (∏ P ∈ x, P)) = if I = ⊤ then 1 else 0 have heq : (∑ S ∈ (primeSupport I).powerset, (moebius (∏ P ∈ S, P) : ℂ)) = ∑ S ∈ (primeSupport I).powerset, (-1 : ℂ) ^ S.card := byI:Ideal OhI:I ≠ ⊥⊢ ∑ J ∈ idealDivisors I, ↑(moebius J) = if I = ⊤ then 1 else 0 exact Finset.sum_congr rfl (fun S hS => moebius_support_product (Finset.mem_powerset.mp hS))I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)heq:∑ S ∈ (primeSupport I).powerset, ↑(moebius (∏ P ∈ S, P)) = ∑ S ∈ (primeSupport I).powerset, (-1) ^ #S⊢ ∑ x ∈ (primeSupport I).powerset, ↑(moebius (∏ P ∈ x, P)) = if I = ⊤ then 1 else 0 rw [heq,I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)heq:∑ S ∈ (primeSupport I).powerset, ↑(moebius (∏ P ∈ S, P)) = ∑ S ∈ (primeSupport I).powerset, (-1) ^ #S⊢ ∑ S ∈ (primeSupport I).powerset, (-1) ^ #S = if I = ⊤ then 1 else 0 CoprimeMobiusExtension.sum_subset_signI:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)heq:∑ S ∈ (primeSupport I).powerset, ↑(moebius (∏ P ∈ S, P)) = ∑ S ∈ (primeSupport I).powerset, (-1) ^ #S⊢ (if primeSupport I = ∅ then 1 else 0) = if I = ⊤ then 1 else 0]I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)heq:∑ S ∈ (primeSupport I).powerset, ↑(moebius (∏ P ∈ S, P)) = ∑ S ∈ (primeSupport I).powerset, (-1) ^ #S⊢ (if primeSupport I = ∅ then 1 else 0) = if I = ⊤ then 1 else 0 simp only [primeSupport_empty_iff I hI]All goals completed! 🐙 ·I:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)⊢ InjOn (fun S => ∏ P ∈ S, P) ↑(primeSupport I).powerset intro S hS T hT hSTI:Ideal OhI:I ≠ ⊥hfilter:∑ J ∈ idealDivisors I, ↑(moebius J) = ∑ J ∈ idealDivisors I with Squarefree J, ↑(moebius J)S:Finset (Ideal O)hS:S ∈ ↑(primeSupport I).powersetT:Finset (Ideal O)hT:T ∈ ↑(primeSupport I).powersethST:(fun S => ∏ P ∈ S, P) S = (fun S => ∏ P ∈ S, P) T⊢ S = T exact support_product_injective (Finset.mem_powerset.mp hS) (Finset.mem_powerset.mp hT) hSTAll goals completed! 🐙end IdealMobiusDivisorSumopen scoped BigOperators Classicalnamespace CompletedGausssectionabbrev O := ActualEisensteinCubic.Oopen ActualEisensteinCubicdef primaryPrime (P : Ideal O) : O := if h : P.IsMaximal ∧ lambda ∉ P then letI : P.IsMaximal := h.1 (cubicJacobi_exists_primary_generator P h.2).choose else 0theorem primaryPrime_spec (P : Ideal O) (h : primaryPrime P ≠ 0) : P.IsMaximal ∧ lambda ∉ P ∧ Ideal.span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1 := byP:Ideal Oh:primaryPrime P ≠ 0⊢ P.IsMaximal ∧ lambda ∉ P ∧ span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1 classical by_cases hg : P.IsMaximal ∧ lambda ∉ PposP:Ideal Oh:primaryPrime P ≠ 0hg:P.IsMaximal ∧ lambda ∉ P⊢ P.IsMaximal ∧ lambda ∉ P ∧ span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1negP:Ideal Oh:primaryPrime P ≠ 0hg:¬(P.IsMaximal ∧ lambda ∉ P)⊢ P.IsMaximal ∧ lambda ∉ P ∧ span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1 ·posP:Ideal Oh:primaryPrime P ≠ 0hg:P.IsMaximal ∧ lambda ∉ P⊢ P.IsMaximal ∧ lambda ∉ P ∧ span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1 let : P.IsMaximal := hg.1posP:Ideal Oh:primaryPrime P ≠ 0hg:P.IsMaximal ∧ lambda ∉ Pthis:P.IsMaximal := ···⊢ P.IsMaximal ∧ lambda ∉ P ∧ span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1 have hs := (cubicJacobi_exists_primary_generator P hg.2).choose_specposP:Ideal Oh:primaryPrime P ≠ 0hg:P.IsMaximal ∧ lambda ∉ Pthis:P.IsMaximal := ···hs:P = span {⋯.choose} ∧ lambda ^ 2 ∣ ⋯.choose - 1 ∧ jacobiSum (cubicChar P ⋯) (cubicChar P ⋯) = -⋯.choose⊢ P.IsMaximal ∧ lambda ∉ P ∧ span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1 simpa only [primaryPrime, dite_eq_left hg] using ⟨hg.1, hg.2, hs.1.symm, hs.2.1⟩All goals completed! 🐙 ·negP:Ideal Oh:primaryPrime P ≠ 0hg:¬(P.IsMaximal ∧ lambda ∉ P)⊢ P.IsMaximal ∧ lambda ∉ P ∧ span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1 simp only [primaryPrime, dite_eq_right hg, ne_eq, not_true_eq_false] at hAll goals completed! 🐙theorem primaryPrime_ne_zero (P : Ideal O) [P.IsMaximal] (hg : lambda ∉ P) : primaryPrime P ≠ 0 := byP:Ideal Oinst✝:P.IsMaximalhg:lambda ∉ P⊢ primaryPrime P ≠ 0 classical have hs := (cubicJacobi_exists_primary_generator P hg).choose_specP:Ideal Oinst✝:P.IsMaximalhg:lambda ∉ Phs:P = span {⋯.choose} ∧ lambda ^ 2 ∣ ⋯.choose - 1 ∧ jacobiSum (cubicChar P hg) (cubicChar P hg) = -⋯.choose⊢ primaryPrime P ≠ 0 have htest : P.IsMaximal ∧ lambda ∉ P := ⟨inferInstance, hg⟩P:Ideal Oinst✝:P.IsMaximalhg:lambda ∉ Phs:P = span {⋯.choose} ∧ lambda ^ 2 ∣ ⋯.choose - 1 ∧ jacobiSum (cubicChar P hg) (cubicChar P hg) = -⋯.choosehtest:P.IsMaximal ∧ lambda ∉ P⊢ primaryPrime P ≠ 0 intro hzP:Ideal Oinst✝:P.IsMaximalhg:lambda ∉ Phs:P = span {⋯.choose} ∧ lambda ^ 2 ∣ ⋯.choose - 1 ∧ jacobiSum (cubicChar P hg) (cubicChar P hg) = -⋯.choosehtest:P.IsMaximal ∧ lambda ∉ Phz:primaryPrime P = 0⊢ False have hp0 : (cubicJacobi_exists_primary_generator P hg).choose = 0 := byP:Ideal Oinst✝:P.IsMaximalhg:lambda ∉ P⊢ primaryPrime P ≠ 0 simpa only [primaryPrime, dite_eq_left htest] using hzP:Ideal Oinst✝:P.IsMaximalhg:lambda ∉ Phs:P = span {⋯.choose} ∧ lambda ^ 2 ∣ ⋯.choose - 1 ∧ jacobiSum (cubicChar P hg) (cubicChar P hg) = -⋯.choosehtest:P.IsMaximal ∧ lambda ∉ Phz:primaryPrime P = 0hp0:⋯.choose = 0⊢ False rw [hp0P:Ideal Oinst✝:P.IsMaximalhg:lambda ∉ Phs:P = span {0} ∧ lambda ^ 2 ∣ 0 - 1 ∧ jacobiSum (cubicChar P hg) (cubicChar P hg) = -0htest:P.IsMaximal ∧ lambda ∉ Phz:primaryPrime P = 0hp0:⋯.choose = 0⊢ False] at hsP:Ideal Oinst✝:P.IsMaximalhg:lambda ∉ Phs:P = span {0} ∧ lambda ^ 2 ∣ 0 - 1 ∧ jacobiSum (cubicChar P hg) (cubicChar P hg) = -0htest:P.IsMaximal ∧ lambda ∉ Phz:primaryPrime P = 0hp0:⋯.choose = 0⊢ False exact (NeZero.ne P) (byP:Ideal Oinst✝:P.IsMaximalhg:lambda ∉ Phs:P = span {0} ∧ lambda ^ 2 ∣ 0 - 1 ∧ jacobiSum (cubicChar P hg) (cubicChar P hg) = -0htest:P.IsMaximal ∧ lambda ∉ Phz:primaryPrime P = 0hp0:⋯.choose = 0⊢ P = 0 simpa using hs.1All goals completed! 🐙)def primaryGenerator (I : Ideal O) : O := if I = 0 then 0 else ((UniqueFactorizationMonoid.normalizedFactors I).map primaryPrime).prod@[simp] theorem primaryGenerator_zero : primaryGenerator 0 = 0 := by⊢ primaryGenerator 0 = 0 rw [primaryGenerator,⊢ (if 0 = 0 then 0 else (Multiset.map primaryPrime (normalizedFactors 0)).prod) = 0 ite_eq_left rfl⊢ 0 = 0]All goals completed! 🐙@[simp] theorem primaryGenerator_bot : primaryGenerator ⊥ = 0 := primaryGenerator_zero@[simp] theorem primaryGenerator_one : primaryGenerator 1 = 1 := by⊢ primaryGenerator 1 = 1 rw [primaryGenerator,⊢ (if 1 = 0 then 0 else (Multiset.map primaryPrime (normalizedFactors 1)).prod) = 1 ite_eq_right one_ne_zero,⊢ (Multiset.map primaryPrime (normalizedFactors 1)).prod = 1 UniqueFactorizationMonoid.normalizedFactors_one⊢ (Multiset.map primaryPrime 0).prod = 1]⊢ (Multiset.map primaryPrime 0).prod = 1 rflAll goals completed! 🐙theorem primaryGenerator_mul (I J : Ideal O) : primaryGenerator (I * J) = primaryGenerator I * primaryGenerator J := byI:Ideal OJ:Ideal O⊢ primaryGenerator (I * J) = primaryGenerator I * primaryGenerator J classical by_cases hI : I = 0posI:Ideal OJ:Ideal OhI:I = 0⊢ primaryGenerator (I * J) = primaryGenerator I * primaryGenerator JnegI:Ideal OJ:Ideal OhI:¬I = 0⊢ primaryGenerator (I * J) = primaryGenerator I * primaryGenerator J ·posI:Ideal OJ:Ideal OhI:I = 0⊢ primaryGenerator (I * J) = primaryGenerator I * primaryGenerator J simp [hI]All goals completed! 🐙 by_cases hJ : J = 0posI:Ideal OJ:Ideal OhI:¬I = 0hJ:J = 0⊢ primaryGenerator (I * J) = primaryGenerator I * primaryGenerator JnegI:Ideal OJ:Ideal OhI:¬I = 0hJ:¬J = 0⊢ primaryGenerator (I * J) = primaryGenerator I * primaryGenerator J ·posI:Ideal OJ:Ideal OhI:¬I = 0hJ:J = 0⊢ primaryGenerator (I * J) = primaryGenerator I * primaryGenerator J simp [hJ]All goals completed! 🐙 simp only [primaryGenerator, ite_eq_right hI, ite_eq_right hJ, ite_eq_right (mul_ne_zero hI hJ), UniqueFactorizationMonoid.normalizedFactors_mul hI hJ, Multiset.map_add, Multiset.prod_add]All goals completed! 🐙def primaryGeneratorHom : Ideal O →*₀ O where toFun := primaryGenerator map_zero' := primaryGenerator_zero map_one' := primaryGenerator_one map_mul' := primaryGenerator_multheorem primaryGenerator_ne_zero_ideal (I : Ideal O) (h : primaryGenerator I ≠ 0) : I ≠ 0 := byI:Ideal Oh:primaryGenerator I ≠ 0⊢ I ≠ 0 intro hII:Ideal Oh:primaryGenerator I ≠ 0hI:I = 0⊢ False exact h (byI:Ideal Oh:primaryGenerator I ≠ 0hI:I = 0⊢ primaryGenerator I = 0 simp [hI]All goals completed! 🐙)theorem primaryPrime_factor_ne_zero (I P : Ideal O) (hI : primaryGenerator I ≠ 0) (hP : P ∈ UniqueFactorizationMonoid.normalizedFactors I) : primaryPrime P ≠ 0 := byI:Ideal OP:Ideal OhI:primaryGenerator I ≠ 0hP:P ∈ normalizedFactors I⊢ primaryPrime P ≠ 0 have hI0 := primaryGenerator_ne_zero_ideal I hII:Ideal OP:Ideal OhI:primaryGenerator I ≠ 0hP:P ∈ normalizedFactors IhI0:I ≠ 0⊢ primaryPrime P ≠ 0 have hprod : ((UniqueFactorizationMonoid.normalizedFactors I).map primaryPrime).prod ≠ 0 := by simpa only [primaryGenerator, ite_eq_right hI0] using hII:Ideal OP:Ideal OhI:primaryGenerator I ≠ 0hP:P ∈ normalizedFactors IhI0:I ≠ 0hprod:(Multiset.map primaryPrime (normalizedFactors I)).prod ≠ 0⊢ primaryPrime P ≠ 0 intro hzI:Ideal OP:Ideal OhI:primaryGenerator I ≠ 0hP:P ∈ normalizedFactors IhI0:I ≠ 0hprod:(Multiset.map primaryPrime (normalizedFactors I)).prod ≠ 0hz:primaryPrime P = 0⊢ False exact hprod (Multiset.prod_eq_zero_iff.mpr (Multiset.mem_map.mpr ⟨P, hP, hz⟩))All goals completed! 🐙theorem span_multiset_prod (s : Multiset O) : Ideal.span {s.prod} = (s.map (fun x => Ideal.span {x})).prod := bys:Multiset O⊢ span {s.prod} = (Multiset.map (fun x => span {x}) s).prod induction s using Multiset.induction_on with | empty =>empty⊢ span {Multiset.prod 0} = (Multiset.map (fun x => span {x}) 0).prod simpAll goals completed! 🐙 | @cons a s ih =>consa:Os:Multiset Oih:span {s.prod} = (Multiset.map (fun x => span {x}) s).prod⊢ span {(a ::ₘ s).prod} = (Multiset.map (fun x => span {x}) (a ::ₘ s)).prod simp only [Multiset.prod_cons, Multiset.map_cons, ← Ideal.span_singleton_mul_span_singleton, ih]All goals completed! 🐙theorem primaryGenerator_spec (I : Ideal O) (h : primaryGenerator I ≠ 0) : Ideal.span {primaryGenerator I} = I ∧ lambda ^ 2 ∣ primaryGenerator I - 1 := byI:Ideal Oh:primaryGenerator I ≠ 0⊢ span {primaryGenerator I} = I ∧ lambda ^ 2 ∣ primaryGenerator I - 1 classical have hI0 := primaryGenerator_ne_zero_ideal I hI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0⊢ span {primaryGenerator I} = I ∧ lambda ^ 2 ∣ primaryGenerator I - 1 have hprime : ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, Ideal.span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1 := by intro P hPI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0P:Ideal OhP:P ∈ normalizedFactors I⊢ span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1 exact (primaryPrime_spec P (primaryPrime_factor_ne_zero I P h hP)).2.2I:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ span {primaryGenerator I} = I ∧ lambda ^ 2 ∣ primaryGenerator I - 1 rw [primaryGenerator,I:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ span {if I = 0 then 0 else (Multiset.map primaryPrime (normalizedFactors I)).prod} = I ∧ lambda ^ 2 ∣ (if I = 0 then 0 else (Multiset.map primaryPrime (normalizedFactors I)).prod) - 1 ite_eq_right hI0I:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ span {(Multiset.map primaryPrime (normalizedFactors I)).prod} = I ∧ lambda ^ 2 ∣ (Multiset.map primaryPrime (normalizedFactors I)).prod - 1]I:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ span {(Multiset.map primaryPrime (normalizedFactors I)).prod} = I ∧ lambda ^ 2 ∣ (Multiset.map primaryPrime (normalizedFactors I)).prod - 1 constructorleftI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ span {(Multiset.map primaryPrime (normalizedFactors I)).prod} = IrightI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ lambda ^ 2 ∣ (Multiset.map primaryPrime (normalizedFactors I)).prod - 1 ·leftI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ span {(Multiset.map primaryPrime (normalizedFactors I)).prod} = I rw [span_multiset_prod,leftI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ (Multiset.map (fun x => span {x}) (Multiset.map primaryPrime (normalizedFactors I))).prod = I Multiset.map_mapleftI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ (Multiset.map ((fun x => span {x}) ∘ primaryPrime) (normalizedFactors I)).prod = I]leftI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ (Multiset.map ((fun x => span {x}) ∘ primaryPrime) (normalizedFactors I)).prod = I have hm : (UniqueFactorizationMonoid.normalizedFactors I).map ((fun x => Ideal.span {x}) ∘ primaryPrime) = UniqueFactorizationMonoid.normalizedFactors I := byI:Ideal Oh:primaryGenerator I ≠ 0⊢ span {primaryGenerator I} = I ∧ lambda ^ 2 ∣ primaryGenerator I - 1 calc _ = (UniqueFactorizationMonoid.normalizedFactors I).map id := Multiset.map_congr rfl (fun P hP => (hprime P hP).1) _ = _ := Multiset.map_id' _leftI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1hm:Multiset.map ((fun x => span {x}) ∘ primaryPrime) (normalizedFactors I) = normalizedFactors I⊢ (Multiset.map ((fun x => span {x}) ∘ primaryPrime) (normalizedFactors I)).prod = I rw [hmleftI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1hm:Multiset.map ((fun x => span {x}) ∘ primaryPrime) (normalizedFactors I) = normalizedFactors I⊢ (normalizedFactors I).prod = I]leftI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1hm:Multiset.map ((fun x => span {x}) ∘ primaryPrime) (normalizedFactors I) = normalizedFactors I⊢ (normalizedFactors I).prod = I exact Ideal.prod_normalizedFactors_eq_self hI0All goals completed! 🐙 ·rightI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ lambda ^ 2 ∣ (Multiset.map primaryPrime (normalizedFactors I)).prod - 1 apply primary_multiset_prodrightI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1⊢ ∀ x ∈ Multiset.map primaryPrime (normalizedFactors I), lambda ^ 2 ∣ x - 1 intro r hrrightI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1r:ActualEisensteinCubic.Ohr:r ∈ Multiset.map primaryPrime (normalizedFactors I)⊢ lambda ^ 2 ∣ r - 1 obtain ⟨P, hP, rfl⟩ := Multiset.mem_map.mp hrrightI:Ideal Oh:primaryGenerator I ≠ 0hI0:I ≠ 0hprime:∀ P ∈ normalizedFactors I, span {primaryPrime P} = P ∧ lambda ^ 2 ∣ primaryPrime P - 1P:Ideal OhP:P ∈ normalizedFactors Ihr:primaryPrime P ∈ Multiset.map primaryPrime (normalizedFactors I)⊢ lambda ^ 2 ∣ primaryPrime P - 1 exact (hprime P hP).2All goals completed! 🐙theorem primaryGenerator_span (n : O) (hn : n ≠ 0) (hprimary : lambda ^ 2 ∣ n - 1) : primaryGenerator (Ideal.span {n}) = n := byn:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1⊢ primaryGenerator (span {n}) = n classical have hI0 : (Ideal.span {n} : Ideal O) ≠ 0 := Ideal.span_singleton_eq_bot.not.mpr hnn:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0⊢ primaryGenerator (span {n}) = n have hgen : primaryGenerator (Ideal.span {n}) ≠ 0 := by rw [primaryGenerator,n:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0⊢ (if span {n} = 0 then 0 else (Multiset.map primaryPrime (normalizedFactors (span {n}))).prod) ≠ 0 ite_eq_right hI0n:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0⊢ (Multiset.map primaryPrime (normalizedFactors (span {n}))).prod ≠ 0]n:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0⊢ (Multiset.map primaryPrime (normalizedFactors (span {n}))).prod ≠ 0 apply Multiset.prod_ne_zeron:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0⊢ 0 ∉ Multiset.map primaryPrime (normalizedFactors (span {n})) intro hzeron:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0hzero:0 ∈ Multiset.map primaryPrime (normalizedFactors (span {n}))⊢ False obtain ⟨P, hP, hz⟩ := Multiset.mem_map.mp hzeron:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0hzero:0 ∈ Multiset.map primaryPrime (normalizedFactors (span {n}))P:Ideal OhP:P ∈ normalizedFactors (span {n})hz:primaryPrime P = 0⊢ False have hp := UniqueFactorizationMonoid.prime_of_normalized_factor P hPn:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0hzero:0 ∈ Multiset.map primaryPrime (normalizedFactors (span {n}))P:Ideal OhP:P ∈ normalizedFactors (span {n})hz:primaryPrime P = 0hp:Prime P⊢ False let : P.IsMaximal := (Ideal.isPrime_of_prime hp).isMaximal hp.ne_zeron:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0hzero:0 ∈ Multiset.map primaryPrime (normalizedFactors (span {n}))P:Ideal OhP:P ∈ normalizedFactors (span {n})hz:primaryPrime P = 0hp:Prime Pthis:P.IsMaximal := ···⊢ False have hle := ((Ideal.mem_normalizedFactors_iff hI0).mp hP).2n:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0hzero:0 ∈ Multiset.map primaryPrime (normalizedFactors (span {n}))P:Ideal OhP:P ∈ normalizedFactors (span {n})hz:primaryPrime P = 0hp:Prime Pthis:P.IsMaximal := ···hle:span {n} ≤ P⊢ False have hnP : n ∈ P := hle (Ideal.subset_span (byn:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0hzero:0 ∈ Multiset.map primaryPrime (normalizedFactors (span {n}))P:Ideal OhP:P ∈ normalizedFactors (span {n})hz:primaryPrime P = 0hp:Prime Pthis:P.IsMaximal := ···hle:span {n} ≤ P⊢ n ∈ {n} simpAll goals completed! 🐙))n:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0hzero:0 ∈ Multiset.map primaryPrime (normalizedFactors (span {n}))P:Ideal OhP:P ∈ normalizedFactors (span {n})hz:primaryPrime P = 0hp:Prime Pthis:P.IsMaximal := ···hle:span {n} ≤ PhnP:n ∈ P⊢ False exact primaryPrime_ne_zero P (primary_maximal_divisor_good n hprimary P hnP) hzn:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0hgen:primaryGenerator (span {n}) ≠ 0⊢ primaryGenerator (span {n}) = n have hspec := primaryGenerator_spec (Ideal.span {n}) hgenn:Ohn:n ≠ 0hprimary:lambda ^ 2 ∣ n - 1hI0:span {n} ≠ 0hgen:primaryGenerator (span {n}) ≠ 0hspec:span {primaryGenerator (span {n})} = span {n} ∧ lambda ^ 2 ∣ primaryGenerator (span {n}) - 1⊢ primaryGenerator (span {n}) = n exact primary_associated_eq _ _ (Ideal.span_singleton_eq_span_singleton.mp hspec.1) hspec.2 hprimaryAll goals completed! 🐙theorem primaryGenerator_norm_sq (I : Ideal O) (h : primaryGenerator I ≠ 0) : ‖ConcreteTraceCRT.eisEmbedding (primaryGenerator I)‖ ^ 2 = (Ideal.absNorm I : ℝ) := byI:Ideal Oh:primaryGenerator I ≠ 0⊢ ‖eisEmbedding (primaryGenerator I)‖ ^ 2 = ↑(absNorm I) rw [eisEmbedding_norm_sq_eq_absNorm_span,I:Ideal Oh:primaryGenerator I ≠ 0⊢ ↑(absNorm (span {primaryGenerator I})) = ↑(absNorm I) (primaryGenerator_spec I h).1I:Ideal Oh:primaryGenerator I ≠ 0⊢ ↑(absNorm I) = ↑(absNorm I)]All goals completed! 🐙open ActualEisensteinCubictheorem compact_window_bound (W : ℝ → ℂ) (hW : HasCompactSupport W) : ∃ B : ℝ, 0 < B ∧ ∀ y, W y ≠ 0 → y ≤ B := byW:ℝ → ℂhW:HasCompactSupport W⊢ ∃ B, 0 < B ∧ ∀ (y : ℝ), W y ≠ 0 → y ≤ B obtain ⟨B, hB⟩ := hW.bddAboveW:ℝ → ℂhW:HasCompactSupport WB:ℝhB:B ∈ upperBounds (tsupport W)⊢ ∃ B, 0 < B ∧ ∀ (y : ℝ), W y ≠ 0 → y ≤ B refine ⟨max B 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), ?_⟩W:ℝ → ℂhW:HasCompactSupport WB:ℝhB:B ∈ upperBounds (tsupport W)⊢ ∀ (y : ℝ), W y ≠ 0 → y ≤ max B 1 intro y hyW:ℝ → ℂhW:HasCompactSupport WB:ℝhB:B ∈ upperBounds (tsupport W)y:ℝhy:W y ≠ 0⊢ y ≤ max B 1 exact (hB (subset_tsupport W hy)).trans (le_max_left _ _)All goals completed! 🐙theorem norm_at_least_one (I : Ideal O) (hI : I ≠ 0) : (1 : ℝ) ≤ Ideal.absNorm I := byI:Ideal OhI:I ≠ 0⊢ 1 ≤ ↑(absNorm I) exact_mod_cast Nat.one_le_iff_ne_zero.mpr (Ideal.absNorm_eq_zero_iff.not.mpr hI)All goals completed! 🐙theorem triple_scale_bounds (a b c : ℝ) (ha : 1 ≤ a) (hb : 1 ≤ b) (hc : 1 ≤ c) : a ≤ a * b ^ 3 * c ^ 3 ∧ b ≤ a * b ^ 3 * c ^ 3 ∧ c ≤ a * b ^ 3 * c ^ 3 := bya:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ c⊢ a ≤ a * b ^ 3 * c ^ 3 ∧ b ≤ a * b ^ 3 * c ^ 3 ∧ c ≤ a * b ^ 3 * c ^ 3 have ha0 : 0 ≤ a := by linaritha:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ a⊢ a ≤ a * b ^ 3 * c ^ 3 ∧ b ≤ a * b ^ 3 * c ^ 3 ∧ c ≤ a * b ^ 3 * c ^ 3 have hb0 : 0 ≤ b := by linaritha:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ b⊢ a ≤ a * b ^ 3 * c ^ 3 ∧ b ≤ a * b ^ 3 * c ^ 3 ∧ c ≤ a * b ^ 3 * c ^ 3 have hc0 : 0 ≤ c := by linaritha:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ c⊢ a ≤ a * b ^ 3 * c ^ 3 ∧ b ≤ a * b ^ 3 * c ^ 3 ∧ c ≤ a * b ^ 3 * c ^ 3 have hb3 : 1 ≤ b ^ 3 := one_le_pow₀ hba:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3⊢ a ≤ a * b ^ 3 * c ^ 3 ∧ b ≤ a * b ^ 3 * c ^ 3 ∧ c ≤ a * b ^ 3 * c ^ 3 have hc3 : 1 ≤ c ^ 3 := one_le_pow₀ hca:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ a ≤ a * b ^ 3 * c ^ 3 ∧ b ≤ a * b ^ 3 * c ^ 3 ∧ c ≤ a * b ^ 3 * c ^ 3 constructorlefta:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ a ≤ a * b ^ 3 * c ^ 3righta:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ b ≤ a * b ^ 3 * c ^ 3 ∧ c ≤ a * b ^ 3 * c ^ 3 ·lefta:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ a ≤ a * b ^ 3 * c ^ 3 calc a = a * 1 * 1 := bya:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ a = a * 1 * 1 ringAll goals completed! 🐙 _ ≤ a * b ^ 3 * c ^ 3 := bya:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ a * 1 * 1 ≤ a * b ^ 3 * c ^ 3 gcongrAll goals completed! 🐙 constructorright.lefta:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ b ≤ a * b ^ 3 * c ^ 3right.righta:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ c ≤ a * b ^ 3 * c ^ 3 ·right.lefta:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ b ≤ a * b ^ 3 * c ^ 3 calc b ≤ b ^ 3 := le_self_pow₀ hb (bya:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ 3 ≠ 0 decideAll goals completed! 🐙) _ = 1 * b ^ 3 * 1 := bya:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ b ^ 3 = 1 * b ^ 3 * 1 ringAll goals completed! 🐙 _ ≤ a * b ^ 3 * c ^ 3 := bya:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ 1 * b ^ 3 * 1 ≤ a * b ^ 3 * c ^ 3 gcongrAll goals completed! 🐙 ·right.righta:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ c ≤ a * b ^ 3 * c ^ 3 calc c ≤ c ^ 3 := le_self_pow₀ hc (bya:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ 3 ≠ 0 decideAll goals completed! 🐙) _ = 1 * 1 * c ^ 3 := bya:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ c ^ 3 = 1 * 1 * c ^ 3 ringAll goals completed! 🐙 _ ≤ a * b ^ 3 * c ^ 3 := bya:ℝb:ℝc:ℝha:1 ≤ ahb:1 ≤ bhc:1 ≤ cha0:0 ≤ ahb0:0 ≤ bhc0:0 ≤ chb3:1 ≤ b ^ 3hc3:1 ≤ c ^ 3⊢ 1 * 1 * c ^ 3 ≤ a * b ^ 3 * c ^ 3 gcongrAll goals completed! 🐙theorem finite_support_norm_triple (W : ℝ → ℂ) (hW : HasCompactSupport W) (X : ℝ) (hX : 0 < X) (F : Ideal O × Ideal O × Ideal O → ℂ) (hzero : ∀ I J H, I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0) (hwindow : ∀ I J H, W ((Ideal.absNorm I : ℝ) * (Ideal.absNorm J : ℝ) ^ 3 * (Ideal.absNorm H : ℝ) ^ 3 / X) = 0 → F (I, J, H) = 0) : (Function.support F).Finite := byW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0⊢ (Function.support F).Finite obtain ⟨B, hB, hbound⟩ := compact_window_bound W hWW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ B⊢ (Function.support F).Finite obtain ⟨M, hM⟩ := exists_nat_gt (B * X)W:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑M⊢ (Function.support F).Finite let S := {I : Ideal O | Ideal.absNorm I ≤ M}W:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}⊢ (Function.support F).Finite have hS : S.Finite := Ideal.finite_setOfPred_absNorm_le MW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.Finite⊢ (Function.support F).Finite apply (hS.prod (hS.prod hS)).subsetW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.Finite⊢ Function.support F ⊆ S ×ˢ S ×ˢ S rintro ⟨I, J, H⟩ hFW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support F⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hF0 : F (I, J, H) ≠ 0 := hFW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hI : I ≠ 0 := fun h => hF0 (hzero I J H (Or.inl h))W:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0hI:I ≠ 0⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hJ : J ≠ 0 := fun h => hF0 (hzero I J H (Or.inr (Or.inl h)))W:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0hI:I ≠ 0hJ:J ≠ 0⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hH : H ≠ 0 := fun h => hF0 (hzero I J H (Or.inr (Or.inr h)))W:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0hI:I ≠ 0hJ:J ≠ 0hH:H ≠ 0⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hw : W ((Ideal.absNorm I : ℝ) * (Ideal.absNorm J : ℝ) ^ 3 * (Ideal.absNorm H : ℝ) ^ 3 / X) ≠ 0 := fun h => hF0 (hwindow I J H h)W:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0hI:I ≠ 0hJ:J ≠ 0hH:H ≠ 0hw:W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) ≠ 0⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hsize := (div_le_iff₀ hX).mp (hbound _ hw)W:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0hI:I ≠ 0hJ:J ≠ 0hH:H ≠ 0hw:W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) ≠ 0hsize:↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ≤ B * X⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hb := triple_scale_bounds _ _ _ (norm_at_least_one I hI) (norm_at_least_one J hJ) (norm_at_least_one H hH)W:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0hI:I ≠ 0hJ:J ≠ 0hH:H ≠ 0hw:W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) ≠ 0hsize:↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ≤ B * Xhb:↑(absNorm I) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ∧ ↑(absNorm J) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ∧ ↑(absNorm H) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hIM : Ideal.absNorm I ≤ M := byW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0⊢ (Function.support F).Finite exact_mod_cast (hb.1.trans hsize).trans hM.leW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0hI:I ≠ 0hJ:J ≠ 0hH:H ≠ 0hw:W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) ≠ 0hsize:↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ≤ B * Xhb:↑(absNorm I) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ∧ ↑(absNorm J) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ∧ ↑(absNorm H) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3hIM:absNorm I ≤ M⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hJM : Ideal.absNorm J ≤ M := byW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0⊢ (Function.support F).Finite exact_mod_cast (hb.2.1.trans hsize).trans hM.leW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0hI:I ≠ 0hJ:J ≠ 0hH:H ≠ 0hw:W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) ≠ 0hsize:↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ≤ B * Xhb:↑(absNorm I) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ∧ ↑(absNorm J) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ∧ ↑(absNorm H) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3hIM:absNorm I ≤ MhJM:absNorm J ≤ M⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S have hHM : Ideal.absNorm H ≤ M := byW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0⊢ (Function.support F).Finite exact_mod_cast (hb.2.2.trans hsize).trans hM.leW:ℝ → ℂhW:HasCompactSupport WX:ℝhX:0 < XF:Ideal O × Ideal O × Ideal O → ℂhzero:∀ (I J H : Ideal O), I = 0 ∨ J = 0 ∨ H = 0 → F (I, J, H) = 0hwindow:∀ (I J H : Ideal O), W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) = 0 → F (I, J, H) = 0B:ℝhB:0 < Bhbound:∀ (y : ℝ), W y ≠ 0 → y ≤ BM:ℕhM:B * X < ↑MS:Set (Ideal O) := {I | absNorm I ≤ M}hS:S.FiniteI:Ideal OJ:Ideal OH:Ideal OhF:(I, J, H) ∈ Function.support FhF0:F (I, J, H) ≠ 0hI:I ≠ 0hJ:J ≠ 0hH:H ≠ 0hw:W (↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 / X) ≠ 0hsize:↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ≤ B * Xhb:↑(absNorm I) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ∧ ↑(absNorm J) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3 ∧ ↑(absNorm H) ≤ ↑(absNorm I) * ↑(absNorm J) ^ 3 * ↑(absNorm H) ^ 3hIM:absNorm I ≤ MhJM:absNorm J ≤ MhHM:absNorm H ≤ M⊢ (I, J, H) ∈ S ×ˢ S ×ˢ S exact ⟨hIM, hJM, hHM⟩All goals completed! 🐙endsectionopen ActualEisensteinCubic ConcreteTraceCRTdef primeSupport (I : Ideal O) : Finset (Ideal O) := (UniqueFactorizationMonoid.normalizedFactors I).toFinsetabbrev PrimeIndex (I : Ideal O) := {P : Ideal O // P ∈ primeSupport I}instance primeIndexMaximal (I : Ideal O) (P : PrimeIndex I) : P.val.IsMaximal := byI:Ideal OP:PrimeIndex I⊢ (↑P).IsMaximal have hp := UniqueFactorizationMonoid.prime_of_normalized_factor P.val (Multiset.mem_toFinset.mp P.property)I:Ideal OP:PrimeIndex Ihp:Prime ↑P⊢ (↑P).IsMaximal exact (Ideal.isPrime_of_prime hp).isMaximal hp.ne_zeroAll goals completed! 🐙theorem primeIndex_good (I : Ideal O) (hI : primaryGenerator I ≠ 0) (P : PrimeIndex I) : lambda ∉ P.val := (primaryPrime_spec P.val (primaryPrime_factor_ne_zero I P.val hI (Multiset.mem_toFinset.mp P.property))).2.1theorem primeIndex_le (I : Ideal O) (hI : I ≠ 0) (P : PrimeIndex I) : I ≤ P.val := ((Ideal.mem_normalizedFactors_iff hI).mp (Multiset.mem_toFinset.mp P.property)).2def cubicRow (I : Ideal O) (hI : primaryGenerator I ≠ 0) (x : O ⧸ I) : ℂ := ∏ P : PrimeIndex I, (canonicalSextic P.val (primeIndex_good I hI P) ^ 2) (Ideal.Quotient.factor (primeIndex_le I (primaryGenerator_ne_zero_ideal I hI) P) x)def gaussTwo (I : Ideal O) (hI : primaryGenerator I ≠ 0) : ℂ := byI:Ideal OhI:primaryGenerator I ≠ 0⊢ ℂ let n := primaryGenerator II:Ideal OhI:primaryGenerator I ≠ 0n:O := primaryGenerator I⊢ ℂ letI : Finite (O ⧸ Ideal.span {n}) := finite_quotient_span hII:Ideal OhI:primaryGenerator I ≠ 0n:O := primaryGenerator Ithis:Finite (O ⧸ span {n}) := ···⊢ ℂ letI : Fintype (O ⧸ Ideal.span {n}) := Fintype.ofFinite _I:Ideal OhI:primaryGenerator I ≠ 0n:O := primaryGenerator Ithis✝:Finite (O ⧸ span {n}) := ···this:Fintype (O ⧸ span {n}) := Fintype.ofFinite (O ⧸ span {n})⊢ ℂ let e := Ideal.quotEquivOfEq (primaryGenerator_spec I hI).1I:Ideal OhI:primaryGenerator I ≠ 0n:O := primaryGenerator Ithis✝:Finite (O ⧸ span {n}) := ···this:Fintype (O ⧸ span {n}) := Fintype.ofFinite (O ⧸ span {n})e:O ⧸ span {primaryGenerator I} ≃+* O ⧸ I := quotEquivOfEq ⋯⊢ ℂ let ψ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates n hII:Ideal OhI:primaryGenerator I ≠ 0n:O := primaryGenerator Ithis✝:Finite (O ⧸ span {n}) := ···this:Fintype (O ⧸ span {n}) := Fintype.ofFinite (O ⧸ span {n})e:O ⧸ span {primaryGenerator I} ≃+* O ⧸ I := quotEquivOfEq ⋯ψ:AddChar (EisensteinEmbedding.O ⧸ span {n}) ℂ := eisTraceModChar ShortDraftTrace.breveE ConcreteBreveE.breveE_period_coordinates n hI⊢ ℂ exact (∑ x : O ⧸ Ideal.span {n}, cubicRow I hI (e x) * ψ x) / (‖eisEmbedding n‖ : ℂ)All goals completed! 🐙def squarefreeGaussCoefficient (I : Ideal O) : ℂ := if h : Squarefree I ∧ primaryGenerator I ≠ 0 then star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I h.2 else 0@[simp] theorem squarefreeGaussCoefficient_zero : squarefreeGaussCoefficient 0 = 0 := by⊢ squarefreeGaussCoefficient 0 = 0 simp [squarefreeGaussCoefficient]All goals completed! 🐙@[simp] theorem squarefreeGaussCoefficient_bot : squarefreeGaussCoefficient ⊥ = 0 := squarefreeGaussCoefficient_zerotheorem squarefreeGaussCoefficient_eq (I : Ideal O) (hs : Squarefree I) (hI : primaryGenerator I ≠ 0) : squarefreeGaussCoefficient I = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI := byI:Ideal Ohs:Squarefree IhI:primaryGenerator I ≠ 0⊢ squarefreeGaussCoefficient I = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI rw [squarefreeGaussCoefficient,I:Ideal Ohs:Squarefree IhI:primaryGenerator I ≠ 0⊢ (if h : Squarefree I ∧ primaryGenerator I ≠ 0 then star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I ⋯ else 0) = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI dite_eq_left ⟨hs, hI⟩I:Ideal Ohs:Squarefree IhI:primaryGenerator I ≠ 0⊢ star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I ⋯ = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI]All goals completed! 🐙theorem angularFactor_mul (a b : O) : FiniteGaussPhase.angularFactor (a * b) = FiniteGaussPhase.angularFactor a * FiniteGaussPhase.angularFactor b := bya:Ob:O⊢ FiniteGaussPhase.angularFactor (a * b) = FiniteGaussPhase.angularFactor a * FiniteGaussPhase.angularFactor b simp only [FiniteGaussPhase.angularFactor, map_mul, norm_mul, Complex.ofReal_mul]a:Ob:O⊢ eisEmbedding a * eisEmbedding b / (↑‖eisEmbedding a‖ * ↑‖eisEmbedding b‖) = eisEmbedding a / ↑‖eisEmbedding a‖ * (eisEmbedding b / ↑‖eisEmbedding b‖) ringAll goals completed! 🐙def cubeWeight (Ψ : O →* ℂ) : Ideal O →* ℂ where toFun I := star (FiniteGaussPhase.angularFactor (primaryGenerator I)) ^ 3 * Ψ (primaryGenerator I) ^ 3 / (Ideal.absNorm I : ℂ) map_one' := byΨ:O →* ℂ⊢ star (FiniteGaussPhase.angularFactor (primaryGenerator 1)) ^ 3 * Ψ (primaryGenerator 1) ^ 3 / ↑(absNorm 1) = 1 simp only [primaryGenerator_one, FiniteGaussPhase.angularFactor, map_one, norm_one, Complex.ofReal_one, div_one, star_one, one_pow, one_mul, Nat.cast_one]All goals completed! 🐙 map_mul' I J := byΨ:O →* ℂI:Ideal OJ:Ideal O⊢ star (FiniteGaussPhase.angularFactor (primaryGenerator (I * J))) ^ 3 * Ψ (primaryGenerator (I * J)) ^ 3 / ↑(absNorm (I * J)) = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) ^ 3 * Ψ (primaryGenerator I) ^ 3 / ↑(absNorm I) * (star (FiniteGaussPhase.angularFactor (primaryGenerator J)) ^ 3 * Ψ (primaryGenerator J) ^ 3 / ↑(absNorm J)) simp only [primaryGenerator_mul, angularFactor_mul, map_mul, star_mul, mul_pow, Nat.cast_mul]Ψ:O →* ℂI:Ideal OJ:Ideal O⊢ star (FiniteGaussPhase.angularFactor (primaryGenerator J)) ^ 3 * star (FiniteGaussPhase.angularFactor (primaryGenerator I)) ^ 3 * (Ψ (primaryGenerator I) ^ 3 * Ψ (primaryGenerator J) ^ 3) / (↑(absNorm I) * ↑(absNorm J)) = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) ^ 3 * Ψ (primaryGenerator I) ^ 3 / ↑(absNorm I) * (star (FiniteGaussPhase.angularFactor (primaryGenerator J)) ^ 3 * Ψ (primaryGenerator J) ^ 3 / ↑(absNorm J)) ringAll goals completed! 🐙@[simp] theorem cubeWeight_zero (Ψ : O →* ℂ) : cubeWeight Ψ 0 = 0 := byΨ:O →* ℂ⊢ (cubeWeight Ψ) 0 = 0 simp [cubeWeight, FiniteGaussPhase.angularFactor]All goals completed! 🐙@[simp] theorem cubeWeight_bot (Ψ : O →* ℂ) : cubeWeight Ψ ⊥ = 0 := cubeWeight_zero Ψdef columnWeight (Ψ : O →* ℂ) (I : Ideal O) : ℂ := squarefreeGaussCoefficient I * Ψ (primaryGenerator I)@[simp] theorem columnWeight_zero (Ψ : O →* ℂ) : columnWeight Ψ 0 = 0 := byΨ:O →* ℂ⊢ columnWeight Ψ 0 = 0 simp [columnWeight]All goals completed! 🐙@[simp] theorem columnWeight_bot (Ψ : O →* ℂ) : columnWeight Ψ ⊥ = 0 := columnWeight_zero Ψdef Vstar (W : ℝ → ℂ) (y : ℝ) : ℂ := (Real.sqrt y : ℂ) * W ydef summand (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) (I J : Ideal O) : ℂ := columnWeight Ψ I / (Real.sqrt (Ideal.absNorm I : ℝ) : ℂ) * cubeWeight Ψ J * Vstar W ((Ideal.absNorm I : ℝ) * (Ideal.absNorm J : ℝ) ^ 3 / X)def completedT (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) : ℂ := ∑' I : Ideal O, ∑' J : Ideal O, summand Ψ W X I Jtheorem summand_zero_left (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) (J : Ideal O) : summand Ψ W X 0 J = 0 := byΨ:O →* ℂW:ℝ → ℂX:ℝJ:Ideal O⊢ summand Ψ W X 0 J = 0 simp [summand]All goals completed! 🐙theorem summand_zero_right (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) (I : Ideal O) : summand Ψ W X I 0 = 0 := byΨ:O →* ℂW:ℝ → ℂX:ℝI:Ideal O⊢ summand Ψ W X I 0 = 0 simp [summand]All goals completed! 🐙theorem summand_zero_window (Ψ : O →* ℂ) (W : ℝ → ℂ) (X : ℝ) (I J : Ideal O) (h : W ((Ideal.absNorm I : ℝ) * (Ideal.absNorm J : ℝ) ^ 3 / X) = 0) : summand Ψ W X I J = 0 := byΨ:O →* ℂW:ℝ → ℂX:ℝI:Ideal OJ:Ideal Oh:W (↑(absNorm I) * ↑(absNorm J) ^ 3 / X) = 0⊢ summand Ψ W X I J = 0 simp [summand, Vstar, h]All goals completed! 🐙theorem cubicRow_mk (I : Ideal O) (hI : primaryGenerator I ≠ 0) (a : O) : cubicRow I hI (Ideal.Quotient.mk I a) = ∏ P : PrimeIndex I, (canonicalSextic P.val (primeIndex_good I hI P) ^ 2) (Ideal.Quotient.mk P.val a) := byI:Ideal OhI:primaryGenerator I ≠ 0a:O⊢ cubicRow I hI ((Ideal.Quotient.mk I) a) = ∏ P, (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) simp only [cubicRow, Ideal.Quotient.factor_mk]All goals completed! 🐙theorem cubicRow_zero_iff (I : Ideal O) (hI : primaryGenerator I ≠ 0) (a : O) : cubicRow I hI (Ideal.Quotient.mk I a) = 0 ↔ ∃ P ∈ primeSupport I, a ∈ P := byI:Ideal OhI:primaryGenerator I ≠ 0a:O⊢ cubicRow I hI ((Ideal.Quotient.mk I) a) = 0 ↔ ∃ P ∈ primeSupport I, a ∈ P rw [cubicRow_mk,I:Ideal OhI:primaryGenerator I ≠ 0a:O⊢ ∏ P, (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0 ↔ ∃ P ∈ primeSupport I, a ∈ P Finset.prod_eq_zero_iffI:Ideal OhI:primaryGenerator I ≠ 0a:O⊢ (∃ a_1 ∈ Finset.univ, (canonicalSextic ↑a_1 ⋯ ^ 2) ((Ideal.Quotient.mk ↑a_1) a) = 0) ↔ ∃ P ∈ primeSupport I, a ∈ P]I:Ideal OhI:primaryGenerator I ≠ 0a:O⊢ (∃ a_1 ∈ Finset.univ, (canonicalSextic ↑a_1 ⋯ ^ 2) ((Ideal.Quotient.mk ↑a_1) a) = 0) ↔ ∃ P ∈ primeSupport I, a ∈ P have hlocal (P : PrimeIndex I) : (canonicalSextic P.val (primeIndex_good I hI P) ^ 2) (Ideal.Quotient.mk P.val a) = 0 ↔ a ∈ P.val := byI:Ideal OhI:primaryGenerator I ≠ 0a:O⊢ cubicRow I hI ((Ideal.Quotient.mk I) a) = 0 ↔ ∃ P ∈ primeSupport I, a ∈ P let : Field (O ⧸ P.val) := Ideal.Quotient.field P.valI:Ideal OhI:primaryGenerator I ≠ 0a:OP:PrimeIndex Ithis:Field (O ⧸ ↑P) := Quotient.field ↑P⊢ (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0 ↔ a ∈ ↑P rw [MulChar.apply_eq_zero_iffI:Ideal OhI:primaryGenerator I ≠ 0a:OP:PrimeIndex Ithis:Field (O ⧸ ↑P) := Quotient.field ↑P⊢ ¬IsUnit ((Ideal.Quotient.mk ↑P) a) ↔ a ∈ ↑P]I:Ideal OhI:primaryGenerator I ≠ 0a:OP:PrimeIndex Ithis:Field (O ⧸ ↑P) := Quotient.field ↑P⊢ ¬IsUnit ((Ideal.Quotient.mk ↑P) a) ↔ a ∈ ↑P simp only [isUnit_iff_ne_zero, not_not, Ideal.Quotient.eq_zero_iff_mem]I:Ideal OhI:primaryGenerator I ≠ 0a:Ohlocal:∀ (P : PrimeIndex I), (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0 ↔ a ∈ ↑P⊢ (∃ a_1 ∈ Finset.univ, (canonicalSextic ↑a_1 ⋯ ^ 2) ((Ideal.Quotient.mk ↑a_1) a) = 0) ↔ ∃ P ∈ primeSupport I, a ∈ P constructormpI:Ideal OhI:primaryGenerator I ≠ 0a:Ohlocal:∀ (P : PrimeIndex I), (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0 ↔ a ∈ ↑P⊢ (∃ a_1 ∈ Finset.univ, (canonicalSextic ↑a_1 ⋯ ^ 2) ((Ideal.Quotient.mk ↑a_1) a) = 0) → ∃ P ∈ primeSupport I, a ∈ PmprI:Ideal OhI:primaryGenerator I ≠ 0a:Ohlocal:∀ (P : PrimeIndex I), (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0 ↔ a ∈ ↑P⊢ (∃ P ∈ primeSupport I, a ∈ P) → ∃ a_2 ∈ Finset.univ, (canonicalSextic ↑a_2 ⋯ ^ 2) ((Ideal.Quotient.mk ↑a_2) a) = 0 ·mpI:Ideal OhI:primaryGenerator I ≠ 0a:Ohlocal:∀ (P : PrimeIndex I), (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0 ↔ a ∈ ↑P⊢ (∃ a_1 ∈ Finset.univ, (canonicalSextic ↑a_1 ⋯ ^ 2) ((Ideal.Quotient.mk ↑a_1) a) = 0) → ∃ P ∈ primeSupport I, a ∈ P rintro ⟨P, _, hP⟩mpI:Ideal OhI:primaryGenerator I ≠ 0a:Ohlocal:∀ (P : PrimeIndex I), (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0 ↔ a ∈ ↑PP:PrimeIndex Ileft✝:P ∈ Finset.univhP:(canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0⊢ ∃ P ∈ primeSupport I, a ∈ P exact ⟨P.val, P.property, (hlocal P).mp hP⟩All goals completed! 🐙 ·mprI:Ideal OhI:primaryGenerator I ≠ 0a:Ohlocal:∀ (P : PrimeIndex I), (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0 ↔ a ∈ ↑P⊢ (∃ P ∈ primeSupport I, a ∈ P) → ∃ a_2 ∈ Finset.univ, (canonicalSextic ↑a_2 ⋯ ^ 2) ((Ideal.Quotient.mk ↑a_2) a) = 0 rintro ⟨P, hP, ha⟩mprI:Ideal OhI:primaryGenerator I ≠ 0a:Ohlocal:∀ (P : PrimeIndex I), (canonicalSextic ↑P ⋯ ^ 2) ((Ideal.Quotient.mk ↑P) a) = 0 ↔ a ∈ ↑PP:Ideal OhP:P ∈ primeSupport Iha:a ∈ P⊢ ∃ a_1 ∈ Finset.univ, (canonicalSextic ↑a_1 ⋯ ^ 2) ((Ideal.Quotient.mk ↑a_1) a) = 0 exact ⟨⟨P, hP⟩, Finset.mem_univ _, (hlocal ⟨P, hP⟩).mpr ha⟩All goals completed! 🐙theorem primaryGenerator_norm (I : Ideal O) (hI : primaryGenerator I ≠ 0) : ‖eisEmbedding (primaryGenerator I)‖ = Real.sqrt (Ideal.absNorm I : ℝ) := byI:Ideal OhI:primaryGenerator I ≠ 0⊢ ‖eisEmbedding (primaryGenerator I)‖ = √↑(absNorm I) rw [← primaryGenerator_norm_sq I hI,I:Ideal OhI:primaryGenerator I ≠ 0⊢ ‖eisEmbedding (primaryGenerator I)‖ = √(‖eisEmbedding (primaryGenerator I)‖ ^ 2) Real.sqrt_sq_eq_abs,I:Ideal OhI:primaryGenerator I ≠ 0⊢ ‖eisEmbedding (primaryGenerator I)‖ = |‖eisEmbedding (primaryGenerator I)‖| abs_of_nonneg (norm_nonneg _)I:Ideal OhI:primaryGenerator I ≠ 0⊢ ‖eisEmbedding (primaryGenerator I)‖ = ‖eisEmbedding (primaryGenerator I)‖]All goals completed! 🐙theorem cubeWeight_span (Ψ : O →* ℂ) (n : O) (hn : n ≠ 0) (hp : lambda ^ 2 ∣ n - 1) : cubeWeight Ψ (Ideal.span {n}) = star (FiniteGaussPhase.angularFactor n) ^ 3 * Ψ n ^ 3 / (ShortDraftLatticeCount.qNat n : ℂ) := byΨ:O →* ℂn:Ohn:n ≠ 0hp:lambda ^ 2 ∣ n - 1⊢ (cubeWeight Ψ) (span {n}) = star (FiniteGaussPhase.angularFactor n) ^ 3 * Ψ n ^ 3 / ↑(qNat n) change star (FiniteGaussPhase.angularFactor (primaryGenerator (Ideal.span {n}))) ^ 3 * Ψ (primaryGenerator (Ideal.span {n})) ^ 3 / (Ideal.absNorm (Ideal.span {n}) : ℂ) = _Ψ:O →* ℂn:Ohn:n ≠ 0hp:lambda ^ 2 ∣ n - 1⊢ star (FiniteGaussPhase.angularFactor (primaryGenerator (span {n}))) ^ 3 * Ψ (primaryGenerator (span {n})) ^ 3 / ↑(absNorm (span {n})) = star (FiniteGaussPhase.angularFactor n) ^ 3 * Ψ n ^ 3 / ↑(qNat n) rw [primaryGenerator_span n hn hp,Ψ:O →* ℂn:Ohn:n ≠ 0hp:lambda ^ 2 ∣ n - 1⊢ star (FiniteGaussPhase.angularFactor n) ^ 3 * Ψ n ^ 3 / ↑(absNorm (span {n})) = star (FiniteGaussPhase.angularFactor n) ^ 3 * Ψ n ^ 3 / ↑(qNat n) qNat_eq_absNorm_spanΨ:O →* ℂn:Ohn:n ≠ 0hp:lambda ^ 2 ∣ n - 1⊢ star (FiniteGaussPhase.angularFactor n) ^ 3 * Ψ n ^ 3 / ↑(absNorm (span {n})) = star (FiniteGaussPhase.angularFactor n) ^ 3 * Ψ n ^ 3 / ↑(absNorm (span {n}))]All goals completed! 🐙theorem columnWeight_eq (Ψ : O →* ℂ) (I : Ideal O) (hs : Squarefree I) (hI : primaryGenerator I ≠ 0) : columnWeight Ψ I = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI * Ψ (primaryGenerator I) := byΨ:O →* ℂI:Ideal Ohs:Squarefree IhI:primaryGenerator I ≠ 0⊢ columnWeight Ψ I = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI * Ψ (primaryGenerator I) rw [columnWeight,Ψ:O →* ℂI:Ideal Ohs:Squarefree IhI:primaryGenerator I ≠ 0⊢ squarefreeGaussCoefficient I * Ψ (primaryGenerator I) = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI * Ψ (primaryGenerator I) squarefreeGaussCoefficient_eq I hs hIΨ:O →* ℂI:Ideal Ohs:Squarefree IhI:primaryGenerator I ≠ 0⊢ star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI * Ψ (primaryGenerator I) = star (FiniteGaussPhase.angularFactor (primaryGenerator I)) * gaussTwo I hI * Ψ (primaryGenerator I)]All goals completed! 🐙theorem columnWeight_zero_of_mask (Ψ : O →* ℂ) (I : Ideal O) (h : Ψ (primaryGenerator I) = 0) : columnWeight Ψ I = 0 := byΨ:O →* ℂI:Ideal Oh:Ψ (primaryGenerator I) = 0⊢ columnWeight Ψ I = 0 simp only [columnWeight, h, mul_zero]All goals completed! 🐙theorem cubeWeight_zero_of_mask (Ψ : O →* ℂ) (I : Ideal O) (h : Ψ (primaryGenerator I) = 0) : cubeWeight Ψ I = 0 := byΨ:O →* ℂI:Ideal Oh:Ψ (primaryGenerator I) = 0⊢ (cubeWeight Ψ) I = 0 change _ * Ψ (primaryGenerator I) ^ 3 / _ = 0Ψ:O →* ℂI:Ideal Oh:Ψ (primaryGenerator I) = 0⊢ star (FiniteGaussPhase.angularFactor (primaryGenerator I)) ^ 3 * Ψ (primaryGenerator I) ^ 3 / ↑(absNorm I) = 0 rw [h,Ψ:O →* ℂI:Ideal Oh:Ψ (primaryGenerator I) = 0⊢ star (FiniteGaussPhase.angularFactor (primaryGenerator I)) ^ 3 * 0 ^ 3 / ↑(absNorm I) = 0 zero_pow (byΨ:O →* ℂI:Ideal Oh:Ψ (primaryGenerator I) = 0⊢ 3 ≠ 0 decideAll goals completed! 🐙), mul_zero,Ψ:O →* ℂI:Ideal Oh:Ψ (primaryGenerator I) = 0⊢ 0 / ↑(absNorm I) = 0 zero_divΨ:O →* ℂI:Ideal Oh:Ψ (primaryGenerator I) = 0⊢ 0 = 0]All goals completed! 🐙endopen ActualEisensteinCubicopen IdealMobiusDivisorSum (idealDivisors mem_idealDivisors sum_moebius_divisors)def MulFiber (B : Ideal O) := {p : Ideal O × Ideal O // p.1 * p.2 = B}def mulFiberDivisorEquiv (B : Ideal O) (hB : B ≠ 0) : MulFiber B ≃ {D : Ideal O // D ∈ idealDivisors B} := byB:Ideal OhB:B ≠ 0⊢ MulFiber B ≃ ↥(idealDivisors B) let f : MulFiber B → {D : Ideal O // D ∈ idealDivisors B} := fun p => ⟨p.val.1, (mem_idealDivisors hB).mpr ⟨p.val.2, p.property.symm⟩⟩B:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩⊢ MulFiber B ≃ ↥(idealDivisors B) apply Equiv.ofBijective fB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩⊢ Function.Bijective f constructorleftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩⊢ Function.Injective frightB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩⊢ Function.Surjective f ·leftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩⊢ Function.Injective f intro p q hpqleftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f q⊢ p = q have hfst : p.val.1 = q.val.1 := congrArg Subtype.val hpqleftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1⊢ p = q apply Subtype.extleftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1⊢ ↑p = ↑q apply Prod.ext hfstleftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1⊢ (↑p).2 = (↑q).2 have hn : p.val.1 ≠ 0 := byB:Ideal OhB:B ≠ 0⊢ MulFiber B ≃ ↥(idealDivisors B) intro hzB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hz:(↑p).1 = 0⊢ False have he := p.propertyB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hz:(↑p).1 = 0he:(↑p).1 * (↑p).2 = B⊢ False rw [hz,B:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hz:(↑p).1 = 0he:0 * (↑p).2 = B⊢ False zero_mulB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hz:(↑p).1 = 0he:0 = B⊢ False] at heB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hz:(↑p).1 = 0he:0 = B⊢ False exact hB he.symmleftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hn:(↑p).1 ≠ 0⊢ (↑p).2 = (↑q).2 apply mul_left_cancel₀ hnleftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hn:(↑p).1 ≠ 0⊢ (↑p).1 * (↑p).2 = (↑p).1 * (↑q).2 rw [p.property,leftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hn:(↑p).1 ≠ 0⊢ B = (↑p).1 * (↑q).2 hfst,leftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hn:(↑p).1 ≠ 0⊢ B = (↑q).1 * (↑q).2 q.propertyleftB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩p:MulFiber Bq:MulFiber Bhpq:f p = f qhfst:(↑p).1 = (↑q).1hn:(↑p).1 ≠ 0⊢ B = B]All goals completed! 🐙 ·rightB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩⊢ Function.Surjective f intro DrightB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩D:↥(idealDivisors B)⊢ ∃ a, f a = D obtain ⟨J, hJ⟩ := (mem_idealDivisors hB).mp D.propertyrightB:Ideal OhB:B ≠ 0f:MulFiber B → ↥(idealDivisors B) := fun p => ⟨(↑p).1, ⋯⟩D:↥(idealDivisors B)J:Ideal IdealMobiusDivisorSum.OhJ:B = ↑D * J⊢ ∃ a, f a = D exact ⟨⟨(D.val, J), hJ.symm⟩, rfl⟩All goals completed! 🐙theorem mulFiber_moebius_sum (B : Ideal O) (hB : B ≠ 0) : (∑' p : MulFiber B, (UniqueFactorizationMonoid.moebius p.val.1 : ℂ)) = if B = 1 then 1 else 0 := byB:Ideal OhB:B ≠ 0⊢ ∑' (p : MulFiber B), ↑(moebius (↑p).1) = if B = 1 then 1 else 0 let e := mulFiberDivisorEquiv B hBB:Ideal OhB:B ≠ 0e:MulFiber B ≃ ↥(idealDivisors B) := mulFiberDivisorEquiv B hB⊢ ∑' (p : MulFiber B), ↑(moebius (↑p).1) = if B = 1 then 1 else 0 calc _ = ∑' D : {D : Ideal O // D ∈ idealDivisors B}, (UniqueFactorizationMonoid.moebius D.val : ℂ) := byB:Ideal OhB:B ≠ 0e:MulFiber B ≃ ↥(idealDivisors B) := mulFiberDivisorEquiv B hB⊢ ∑' (p : MulFiber B), ↑(moebius (↑p).1) = ∑' (D : ↥(idealDivisors B)), ↑(moebius ↑D) exact e.tsum_eq (fun D => (UniqueFactorizationMonoid.moebius D.val : ℂ))All goals completed! 🐙 _ = ∑ D ∈ idealDivisors B, (UniqueFactorizationMonoid.moebius D : ℂ) := byB:Ideal OhB:B ≠ 0e:MulFiber B ≃ ↥(idealDivisors B) := mulFiberDivisorEquiv B hB⊢ ∑' (D : ↥(idealDivisors B)), ↑(moebius ↑D) = ∑ D ∈ idealDivisors B, ↑(moebius D) rw [tsum_fintypeB:Ideal OhB:B ≠ 0e:MulFiber B ≃ ↥(idealDivisors B) := mulFiberDivisorEquiv B hB⊢ ∑ b, ↑(moebius ↑b) = ∑ D ∈ idealDivisors B, ↑(moebius D)]B:Ideal OhB:B ≠ 0e:MulFiber B ≃ ↥(idealDivisors B) := mulFiberDivisorEquiv B hB⊢ ∑ b, ↑(moebius ↑b) = ∑ D ∈ idealDivisors B, ↑(moebius D) exact (Finset.sum_subtype (idealDivisors B) (fun D => Iff.rfl) (fun D => (UniqueFactorizationMonoid.moebius D : ℂ))).symmAll goals completed! 🐙 _ = if B = 1 then 1 else 0 := byB:Ideal OhB:B ≠ 0e:MulFiber B ≃ ↥(idealDivisors B) := mulFiberDivisorEquiv B hB⊢ ∑ D ∈ idealDivisors B, ↑(moebius D) = if B = 1 then 1 else 0 simpa only [Ideal.one_eq_top] using sum_moebius_divisors B hBAll goals completed! 🐙theorem ideal_cube_convolution (c : Ideal O →* ℂ) (hc0 : c 0 = 0) (f : Ideal O → ℂ) (hfinite : (Function.support (fun p : Ideal O × Ideal O => (UniqueFactorizationMonoid.moebius p.1 : ℂ) * c (p.1 * p.2) * f (p.1 * p.2))).Finite) : (∑' H : Ideal O, ∑' J : Ideal O, (UniqueFactorizationMonoid.moebius H : ℂ) * c (H * J) * f (H * J)) = f 1 := byc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).Finite⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1 let F : Ideal O × Ideal O → ℂ := fun p => (UniqueFactorizationMonoid.moebius p.1 : ℂ) * c (p.1 * p.2) * f (p.1 * p.2)c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1 have hF : Summable F := summable_of_hasFiniteSupport hfinitec:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable F⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1 have hfiber (B : Ideal O) : (∑' p : MulFiber B, F p.val) = if B = 1 then f 1 else 0 := by by_cases hB : B = 0posc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:B = 0⊢ ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0negc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0⊢ ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0 ·posc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:B = 0⊢ ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0 subst Bposc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable F⊢ ∑' (p : MulFiber 0), F ↑p = if 0 = 1 then f 1 else 0 have heach : ∀ p : MulFiber 0, F p.val = 0 := byc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).Finite⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1 intro pc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fp:MulFiber 0⊢ F ↑p = 0 dsimp [F]c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fp:MulFiber 0⊢ ↑(moebius (↑p).1) * c ((↑p).1 * (↑p).2) * f ((↑p).1 * (↑p).2) = 0 rw [p.property,c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fp:MulFiber 0⊢ ↑(moebius (↑p).1) * c 0 * f 0 = 0 hc0,c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fp:MulFiber 0⊢ ↑(moebius (↑p).1) * 0 * f 0 = 0 mul_zero,c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fp:MulFiber 0⊢ 0 * f 0 = 0 zero_mulc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fp:MulFiber 0⊢ 0 = 0]posc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fheach:∀ (p : MulFiber 0), F ↑p = 0⊢ ∑' (p : MulFiber 0), F ↑p = if 0 = 1 then f 1 else 0 simp only [heach, tsum_zero, zero_ne_one, ite_false]All goals completed! 🐙 ·negc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0⊢ ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0 calc _ = ∑' p : MulFiber B, (UniqueFactorizationMonoid.moebius p.val.1 : ℂ) * (c B * f B) := byc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0⊢ ∑' (p : MulFiber B), F ↑p = ∑' (p : MulFiber B), ↑(moebius (↑p).1) * (c B * f B) apply tsum_congrc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0⊢ ∀ (b : MulFiber B), F ↑b = ↑(moebius (↑b).1) * (c B * f B) intro pc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0p:MulFiber B⊢ F ↑p = ↑(moebius (↑p).1) * (c B * f B) dsimp [F]c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0p:MulFiber B⊢ ↑(moebius (↑p).1) * c ((↑p).1 * (↑p).2) * f ((↑p).1 * (↑p).2) = ↑(moebius (↑p).1) * (c B * f B) rw [p.property,c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0p:MulFiber B⊢ ↑(moebius (↑p).1) * c B * f B = ↑(moebius (↑p).1) * (c B * f B) mul_assocc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0p:MulFiber B⊢ ↑(moebius (↑p).1) * (c B * f B) = ↑(moebius (↑p).1) * (c B * f B)]All goals completed! 🐙 _ = (∑' p : MulFiber B, (UniqueFactorizationMonoid.moebius p.val.1 : ℂ)) * (c B * f B) := byc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0⊢ ∑' (p : MulFiber B), ↑(moebius (↑p).1) * (c B * f B) = (∑' (p : MulFiber B), ↑(moebius (↑p).1)) * (c B * f B) rw [tsum_mul_rightc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0⊢ (∑' (x : MulFiber B), ↑(moebius (↑x).1)) * (c B * f B) = (∑' (p : MulFiber B), ↑(moebius (↑p).1)) * (c B * f B)]All goals completed! 🐙 _ = if B = 1 then f 1 else 0 := byc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0⊢ (∑' (p : MulFiber B), ↑(moebius (↑p).1)) * (c B * f B) = if B = 1 then f 1 else 0 rw [mulFiber_moebius_sum B hBc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0⊢ (if B = 1 then 1 else 0) * (c B * f B) = if B = 1 then f 1 else 0]c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0⊢ (if B = 1 then 1 else 0) * (c B * f B) = if B = 1 then f 1 else 0 split_ifs with hposc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0h:B = 1⊢ 1 * (c B * f B) = f 1negc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0h:¬B = 1⊢ 0 * (c B * f B) = 0 ·posc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0h:B = 1⊢ 1 * (c B * f B) = f 1 subst Bposc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FhB:¬1 = 0⊢ 1 * (c 1 * f 1) = f 1; simp only [map_one, one_mul]All goals completed! 🐙 ·negc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable FB:Ideal OhB:¬B = 0h:¬B = 1⊢ 0 * (c B * f B) = 0 simpc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fhfiber:∀ (B : Ideal O), ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1 have hs := hF.hasSum.tsum_fiberwise (fun p : Ideal O × Ideal O => p.1 * p.2)c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fhfiber:∀ (B : Ideal O), ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0hs:HasSum (fun c => ∑' (b : ↑((fun p => p.1 * p.2) ⁻¹' {c})), F ↑b) (∑' (b : Ideal O × Ideal O), F b)⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1 change HasSum (fun B : Ideal O => ∑' p : MulFiber B, F p.val) (∑' p, F p) at hsc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fhfiber:∀ (B : Ideal O), ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0hs:HasSum (fun B => ∑' (p : MulFiber B), F ↑p) (∑' (p : Ideal O × Ideal O), F p)⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1 simp_rw [c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fhfiber:∀ (B : Ideal O), ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0hs:HasSum (fun B => ∑' (p : MulFiber B), F ↑p) (∑' (p : Ideal O × Ideal O), F p)⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1hfiberc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fhfiber:∀ (B : Ideal O), ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0hs:HasSum (fun B => if B = 1 then f 1 else 0) (∑' (p : Ideal O × Ideal O), F p)⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1] at hs have hsum : (∑' p, F p) = f 1 := by have he := hs.tsum_eq.symmc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fhfiber:∀ (B : Ideal O), ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0hs:HasSum (fun B => if B = 1 then f 1 else 0) (∑' (p : Ideal O × Ideal O), F p)he:∑' (p : Ideal O × Ideal O), F p = ∑' (b : Ideal O), if b = 1 then f 1 else 0⊢ ∑' (p : Ideal O × Ideal O), F p = f 1 simpa only [tsum_ite_eq, one_ne_zero] using hec:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fhfiber:∀ (B : Ideal O), ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0hs:HasSum (fun B => if B = 1 then f 1 else 0) (∑' (p : Ideal O × Ideal O), F p)hsum:∑' (p : Ideal O × Ideal O), F p = f 1⊢ ∑' (H : Ideal O) (J : Ideal O), ↑(moebius H) * c (H * J) * f (H * J) = f 1 rw [← hF.tsum_prodc:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fhfiber:∀ (B : Ideal O), ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0hs:HasSum (fun B => if B = 1 then f 1 else 0) (∑' (p : Ideal O × Ideal O), F p)hsum:∑' (p : Ideal O × Ideal O), F p = f 1⊢ ∑' (p : Ideal O × Ideal O), F p = f 1]c:Ideal O →* ℂhc0:c 0 = 0f:Ideal O → ℂhfinite:(Function.support fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)).FiniteF:Ideal O × Ideal O → ℂ := fun p => ↑(moebius p.1) * c (p.1 * p.2) * f (p.1 * p.2)hF:Summable Fhfiber:∀ (B : Ideal O), ∑' (p : MulFiber B), F ↑p = if B = 1 then f 1 else 0hs:HasSum (fun B => if B = 1 then f 1 else 0) (∑' (p : Ideal O × Ideal O), F p)hsum:∑' (p : Ideal O × Ideal O), F p = f 1⊢ ∑' (p : Ideal O × Ideal O), F p = f 1 exact hsumAll goals completed! 🐙end CompletedGaussendend OAI