import OAI.NumberTheory.DirichletL.Mellin.SixthPowerAveragenamespace OAInoncomputable sectionnamespace SmoothMobiusCorrectionopen 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 BigOperatorsopen scoped BigOperatorsopen scoped BigOperators Classical SchwartzMapopen scoped BigOperators Classicalopen scoped BigOperators Classicalsectionopen ActualEisensteinCubicopen IdealMobiusDivisorSum hiding Oopen UniqueFactorizationMonoidopen CanonicalRowCompletion (primeValueHom primeValueHom_prime)abbrev PrimeIdeal := {P : Ideal ActualEisensteinCubic.O // Prime P}def primeProduct (s : Finset PrimeIdeal) : Ideal ActualEisensteinCubic.O := ∏ P ∈ s, P.valdef primeSet (I : Ideal ActualEisensteinCubic.O) : Finset PrimeIdeal := (primeSupport I).attach.image (fun P => ⟨P.val, support_prime P.property⟩)@[simp] theorem mem_primeSet (I : Ideal ActualEisensteinCubic.O) (P : PrimeIdeal) : P ∈ primeSet I ↔ P.val ∈ primeSupport I := byI:Ideal ActualEisensteinCubic.OP:PrimeIdeal⊢ P ∈ primeSet I ↔ ↑P ∈ primeSupport I simp only [primeSet, Finset.mem_image, Finset.mem_attach, true_and]I:Ideal ActualEisensteinCubic.OP:PrimeIdeal⊢ (∃ a, ⟨↑a, ⋯⟩ = P) ↔ ↑P ∈ primeSupport I constructormpI:Ideal ActualEisensteinCubic.OP:PrimeIdeal⊢ (∃ a, ⟨↑a, ⋯⟩ = P) → ↑P ∈ primeSupport ImprI:Ideal ActualEisensteinCubic.OP:PrimeIdeal⊢ ↑P ∈ primeSupport I → ∃ a, ⟨↑a, ⋯⟩ = P ·mpI:Ideal ActualEisensteinCubic.OP:PrimeIdeal⊢ (∃ a, ⟨↑a, ⋯⟩ = P) → ↑P ∈ primeSupport I rintro ⟨Q,hQ⟩mpI:Ideal ActualEisensteinCubic.OP:PrimeIdealQ:↥(primeSupport I)hQ:⟨↑Q, ⋯⟩ = P⊢ ↑P ∈ primeSupport I have hv := congrArg Subtype.val hQmpI:Ideal ActualEisensteinCubic.OP:PrimeIdealQ:↥(primeSupport I)hQ:⟨↑Q, ⋯⟩ = Phv:↑⟨↑Q, ⋯⟩ = ↑P⊢ ↑P ∈ primeSupport I simpa only [←hv] using Q.propertyAll goals completed! 🐙 ·mprI:Ideal ActualEisensteinCubic.OP:PrimeIdeal⊢ ↑P ∈ primeSupport I → ∃ a, ⟨↑a, ⋯⟩ = P intro hmprI:Ideal ActualEisensteinCubic.OP:PrimeIdealh:↑P ∈ primeSupport I⊢ ∃ a, ⟨↑a, ⋯⟩ = P exact ⟨⟨P.val,h⟩,rfl⟩All goals completed! 🐙theorem primeProduct_ne_zero (s : Finset PrimeIdeal) : primeProduct s ≠ 0 := Finset.prod_ne_zero_iff.mpr (fun P _ => P.property.ne_zero)theorem factors_primeProduct (s : Finset PrimeIdeal) : normalizedFactors (primeProduct s) = s.val.map Subtype.val := bys:Finset PrimeIdeal⊢ normalizedFactors (primeProduct s) = Multiset.map Subtype.val s.val have h := normalizedFactors_prod_of_prime (m := s.val.map (fun P : PrimeIdeal => P.val)) (bys:Finset PrimeIdeal⊢ ∀ p ∈ Multiset.map (fun P => ↑P) s.val, Prime p intro P hPs:Finset PrimeIdealP:Ideal ActualEisensteinCubic.OhP:P ∈ Multiset.map (fun P => ↑P) s.val⊢ Prime P obtain ⟨Q,hQ,rfl⟩ := Multiset.mem_map.mp hPs:Finset PrimeIdealQ:PrimeIdealhQ:Q ∈ s.valhP:↑Q ∈ Multiset.map (fun P => ↑P) s.val⊢ Prime ↑Q exact Q.propertyAll goals completed! 🐙)s:Finset PrimeIdealh:normalizedFactors (Multiset.map (fun P => ↑P) s.val).prod = Multiset.map (fun P => ↑P) s.val⊢ normalizedFactors (primeProduct s) = Multiset.map Subtype.val s.val simpa only [primeProduct, Finset.prod_eq_multiset_prod] using hAll goals completed! 🐙theorem primeSet_primeProduct (s : Finset PrimeIdeal) : primeSet (primeProduct s) = s := bys:Finset PrimeIdeal⊢ primeSet (primeProduct s) = s ext Ps:Finset PrimeIdealP:PrimeIdeal⊢ P ∈ primeSet (primeProduct s) ↔ P ∈ s rw [mem_primeSets:Finset PrimeIdealP:PrimeIdeal⊢ ↑P ∈ primeSupport (primeProduct s) ↔ P ∈ s]s:Finset PrimeIdealP:PrimeIdeal⊢ ↑P ∈ primeSupport (primeProduct s) ↔ P ∈ s simp only [primeSupport, factors_primeProduct, Multiset.mem_toFinset, Multiset.mem_map, Finset.mem_val]s:Finset PrimeIdealP:PrimeIdeal⊢ (∃ a ∈ s, ↑a = ↑P) ↔ P ∈ s constructormps:Finset PrimeIdealP:PrimeIdeal⊢ (∃ a ∈ s, ↑a = ↑P) → P ∈ smprs:Finset PrimeIdealP:PrimeIdeal⊢ P ∈ s → ∃ a ∈ s, ↑a = ↑P ·mps:Finset PrimeIdealP:PrimeIdeal⊢ (∃ a ∈ s, ↑a = ↑P) → P ∈ s rintro ⟨Q,hQ,he⟩mps:Finset PrimeIdealP:PrimeIdealQ:{ P // Prime P }hQ:Q ∈ she:↑Q = ↑P⊢ P ∈ s have : Q=P := Subtype.ext hemps:Finset PrimeIdealP:PrimeIdealQ:{ P // Prime P }hQ:Q ∈ she:↑Q = ↑Pthis:Q = P⊢ P ∈ s simpa [this] using hQAll goals completed! 🐙 ·mprs:Finset PrimeIdealP:PrimeIdeal⊢ P ∈ s → ∃ a ∈ s, ↑a = ↑P intro hmprs:Finset PrimeIdealP:PrimeIdealh:P ∈ s⊢ ∃ a ∈ s, ↑a = ↑P exact ⟨P,h,rfl⟩All goals completed! 🐙theorem primeProduct_injective : Function.Injective primeProduct := by⊢ Function.Injective primeProduct intro s t hs:Finset PrimeIdealt:Finset PrimeIdealh:primeProduct s = primeProduct t⊢ s = t simpa only [primeSet_primeProduct] using congrArg primeSet hAll goals completed! 🐙theorem primeProduct_squarefree (s : Finset PrimeIdeal) : Squarefree (primeProduct s) := bys:Finset PrimeIdeal⊢ Squarefree (primeProduct s) rw [squarefree_iff_nodup_normalizedFactors (primeProduct_ne_zero s),s:Finset PrimeIdeal⊢ (normalizedFactors (primeProduct s)).Nodupfactors_primeProducts:Finset PrimeIdeal⊢ (Multiset.map Subtype.val s.val).Nodup]s:Finset PrimeIdeal⊢ (Multiset.map Subtype.val s.val).Nodup exact s.nodup.map Subtype.val_injectiveAll goals completed! 🐙theorem primeProduct_primeSet (I : Ideal ActualEisensteinCubic.O) (hI : Squarefree I) : primeProduct (primeSet I) = I := byI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ primeProduct (primeSet I) = I unfold primeProduct primeSetI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ∏ P ∈ Finset.image (fun P => ⟨↑P, ⋯⟩) (primeSupport I).attach, ↑P = I rw [Finset.prod_imageI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ∏ x ∈ (primeSupport I).attach, ↑⟨↑x, ⋯⟩ = II:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ InjOn (fun P => ⟨↑P, ⋯⟩) ↑(primeSupport I).attach]I:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ∏ x ∈ (primeSupport I).attach, ↑⟨↑x, ⋯⟩ = II:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ InjOn (fun P => ⟨↑P, ⋯⟩) ↑(primeSupport I).attach ·I:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ∏ x ∈ (primeSupport I).attach, ↑⟨↑x, ⋯⟩ = I change (∏ P ∈ (primeSupport I).attach, (fun Q : Ideal ActualEisensteinCubic.O => Q) P.val) = II:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ∏ P ∈ (primeSupport I).attach, (fun Q => Q) ↑P = I exact (Finset.prod_attach (primeSupport I) (fun Q : Ideal ActualEisensteinCubic.O => Q)).trans (squarefree_support_product_self hI)All goals completed! 🐙 ·I:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ InjOn (fun P => ⟨↑P, ⋯⟩) ↑(primeSupport I).attach intro P hP Q hQ heI:Ideal ActualEisensteinCubic.OhI:Squarefree IP:↥(primeSupport I)hP:P ∈ ↑(primeSupport I).attachQ:↥(primeSupport I)hQ:Q ∈ ↑(primeSupport I).attachhe:(fun P => ⟨↑P, ⋯⟩) P = (fun P => ⟨↑P, ⋯⟩) Q⊢ P = Q exact Subtype.ext (congrArg (fun R : PrimeIdeal => R.val) he)All goals completed! 🐙def mobiusPrimeCoeff (w : Ideal ActualEisensteinCubic.O → ℂ) (I : Ideal ActualEisensteinCubic.O) : ℂ := (moebius I : ℂ) * primeValueHom w Itheorem mobiusPrimeCoeff_nonsquarefree (w : Ideal ActualEisensteinCubic.O → ℂ) (I : Ideal ActualEisensteinCubic.O) (hI : ¬Squarefree I) : mobiusPrimeCoeff w I=0 := byw:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:¬Squarefree I⊢ mobiusPrimeCoeff w I = 0 simp [mobiusPrimeCoeff,moebius_of_not_squarefree hI]All goals completed! 🐙theorem mobiusPrimeCoeff_primeProduct (w : Ideal ActualEisensteinCubic.O → ℂ) (s : Finset PrimeIdeal) : mobiusPrimeCoeff w (primeProduct s) = ∏ P ∈ s, -w P.val := byw:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdeal⊢ mobiusPrimeCoeff w (primeProduct s) = ∏ P ∈ s, -w ↑P have hm : (moebius (primeProduct s) : ℂ)=(-1:ℂ)^s.card := by rw [(primeProduct_squarefree s).moebius_eq,w:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdeal⊢ ↑((-1) ^ (factors (primeProduct s)).card) = (-1) ^ #sfactors_eq_normalizedFactors,w:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdeal⊢ ↑((-1) ^ (normalizedFactors (primeProduct s)).card) = (-1) ^ #s factors_primeProductw:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdeal⊢ ↑((-1) ^ (Multiset.map Subtype.val s.val).card) = (-1) ^ #s]w:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdeal⊢ ↑((-1) ^ (Multiset.map Subtype.val s.val).card) = (-1) ^ #s simpw:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdealhm:↑(moebius (primeProduct s)) = (-1) ^ #s⊢ mobiusPrimeCoeff w (primeProduct s) = ∏ P ∈ s, -w ↑P rw [mobiusPrimeCoeff,w:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdealhm:↑(moebius (primeProduct s)) = (-1) ^ #s⊢ ↑(moebius (primeProduct s)) * (primeValueHom w) (primeProduct s) = ∏ P ∈ s, -w ↑Phmw:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdealhm:↑(moebius (primeProduct s)) = (-1) ^ #s⊢ (-1) ^ #s * (primeValueHom w) (primeProduct s) = ∏ P ∈ s, -w ↑P]w:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdealhm:↑(moebius (primeProduct s)) = (-1) ^ #s⊢ (-1) ^ #s * (primeValueHom w) (primeProduct s) = ∏ P ∈ s, -w ↑P simp only [primeProduct,map_prod,primeValueHom_prime _ _ (Subtype.property _)]w:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdealhm:↑(moebius (primeProduct s)) = (-1) ^ #s⊢ (-1) ^ #s * ∏ x ∈ s, w ↑x = ∏ P ∈ s, -w ↑P rw [Finset.prod_negw:Ideal ActualEisensteinCubic.O → ℂs:Finset PrimeIdealhm:↑(moebius (primeProduct s)) = (-1) ^ #s⊢ (-1) ^ #s * ∏ x ∈ s, w ↑x = (-1) ^ #s * ∏ x ∈ s, w ↑x]All goals completed! 🐙theorem mobiusPrimeCoeff_tsum (w : Ideal ActualEisensteinCubic.O → ℂ) : (∑' I : Ideal ActualEisensteinCubic.O, mobiusPrimeCoeff w I) = ∑' s : Finset PrimeIdeal, ∏ P ∈ s, -w P.val := byw:Ideal ActualEisensteinCubic.O → ℂ⊢ ∑' (I : Ideal ActualEisensteinCubic.O), mobiusPrimeCoeff w I = ∑' (s : Finset PrimeIdeal), ∏ P ∈ s, -w ↑P apply tsum_eq_tsum_of_ne_zero_bij (fun s => primeProduct s.val)hiw:Ideal ActualEisensteinCubic.O → ℂ⊢ Function.Injective fun s => primeProduct ↑shfw:Ideal ActualEisensteinCubic.O → ℂ⊢ Function.support (mobiusPrimeCoeff w) ⊆ Set.range fun s => primeProduct ↑shfgw:Ideal ActualEisensteinCubic.O → ℂ⊢ ∀ (x : ↑(Function.support fun y => ∏ P ∈ y, -w ↑P)), mobiusPrimeCoeff w (primeProduct ↑x) = ∏ P ∈ ↑x, -w ↑P ·hiw:Ideal ActualEisensteinCubic.O → ℂ⊢ Function.Injective fun s => primeProduct ↑s exact primeProduct_injective.comp Subtype.val_injectiveAll goals completed! 🐙 ·hfw:Ideal ActualEisensteinCubic.O → ℂ⊢ Function.support (mobiusPrimeCoeff w) ⊆ Set.range fun s => primeProduct ↑s intro I hIhfw:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:I ∈ Function.support (mobiusPrimeCoeff w)⊢ I ∈ Set.range fun s => primeProduct ↑s have hs : Squarefree I := byw:Ideal ActualEisensteinCubic.O → ℂ⊢ ∑' (I : Ideal ActualEisensteinCubic.O), mobiusPrimeCoeff w I = ∑' (s : Finset PrimeIdeal), ∏ P ∈ s, -w ↑P by_contra hsw:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:I ∈ Function.support (mobiusPrimeCoeff w)hs:¬Squarefree I⊢ False exact hI (mobiusPrimeCoeff_nonsquarefree w I hs)hfw:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:I ∈ Function.support (mobiusPrimeCoeff w)hs:Squarefree I⊢ I ∈ Set.range fun s => primeProduct ↑s have hp : (∏ P ∈ primeSet I, -w P.val) ≠ 0 := byw:Ideal ActualEisensteinCubic.O → ℂ⊢ ∑' (I : Ideal ActualEisensteinCubic.O), mobiusPrimeCoeff w I = ∑' (s : Finset PrimeIdeal), ∏ P ∈ s, -w ↑P rw [←mobiusPrimeCoeff_primeProduct,w:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:I ∈ Function.support (mobiusPrimeCoeff w)hs:Squarefree I⊢ mobiusPrimeCoeff w (primeProduct (primeSet I)) ≠ 0primeProduct_primeSet I hsw:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:I ∈ Function.support (mobiusPrimeCoeff w)hs:Squarefree I⊢ mobiusPrimeCoeff w I ≠ 0]w:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:I ∈ Function.support (mobiusPrimeCoeff w)hs:Squarefree I⊢ mobiusPrimeCoeff w I ≠ 0 exact hIhfw:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:I ∈ Function.support (mobiusPrimeCoeff w)hs:Squarefree Ihp:∏ P ∈ primeSet I, -w ↑P ≠ 0⊢ I ∈ Set.range fun s => primeProduct ↑s exact ⟨⟨primeSet I,hp⟩,primeProduct_primeSet I hs⟩All goals completed! 🐙 ·hfgw:Ideal ActualEisensteinCubic.O → ℂ⊢ ∀ (x : ↑(Function.support fun y => ∏ P ∈ y, -w ↑P)), mobiusPrimeCoeff w (primeProduct ↑x) = ∏ P ∈ ↑x, -w ↑P intro shfgw:Ideal ActualEisensteinCubic.O → ℂs:↑(Function.support fun y => ∏ P ∈ y, -w ↑P)⊢ mobiusPrimeCoeff w (primeProduct ↑s) = ∏ P ∈ ↑s, -w ↑P exact mobiusPrimeCoeff_primeProduct w s.valAll goals completed! 🐙theorem mobiusPrimeCoeff_euler (w : Ideal ActualEisensteinCubic.O → ℂ) (hw : Summable (fun P : PrimeIdeal => ‖w P.val‖)) : (∑' I : Ideal ActualEisensteinCubic.O, mobiusPrimeCoeff w I) = ∏' P : PrimeIdeal, (1-w P.val) := byw:Ideal ActualEisensteinCubic.O → ℂhw:Summable fun P => ‖w ↑P‖⊢ ∑' (I : Ideal ActualEisensteinCubic.O), mobiusPrimeCoeff w I = ∏' (P : PrimeIdeal), (1 - w ↑P) rw [mobiusPrimeCoeff_tsumw:Ideal ActualEisensteinCubic.O → ℂhw:Summable fun P => ‖w ↑P‖⊢ ∑' (s : Finset PrimeIdeal), ∏ P ∈ s, -w ↑P = ∏' (P : PrimeIdeal), (1 - w ↑P)]w:Ideal ActualEisensteinCubic.O → ℂhw:Summable fun P => ‖w ↑P‖⊢ ∑' (s : Finset PrimeIdeal), ∏ P ∈ s, -w ↑P = ∏' (P : PrimeIdeal), (1 - w ↑P) have hs : Summable (fun P : PrimeIdeal => ‖-w P.val‖) := byw:Ideal ActualEisensteinCubic.O → ℂhw:Summable fun P => ‖w ↑P‖⊢ ∑' (I : Ideal ActualEisensteinCubic.O), mobiusPrimeCoeff w I = ∏' (P : PrimeIdeal), (1 - w ↑P) simpa using hww:Ideal ActualEisensteinCubic.O → ℂhw:Summable fun P => ‖w ↑P‖hs:Summable fun P => ‖-w ↑P‖⊢ ∑' (s : Finset PrimeIdeal), ∏ P ∈ s, -w ↑P = ∏' (P : PrimeIdeal), (1 - w ↑P) simpa only [sub_eq_add_neg] using (tprod_one_add (summable_finsetProd_of_summable_norm hs)).symmAll goals completed! 🐙endsectionopen ActualEisensteinCubicopen Filterlemma prime_norm_two_le (P : PrimeIdeal) : 2 ≤ Ideal.absNorm P.val := byP:PrimeIdeal⊢ 2 ≤ absNorm ↑P have h0 : Ideal.absNorm P.val ≠ 0 := fun h => P.property.ne_zero (Ideal.absNorm_eq_zero_iff.mp h)P:PrimeIdealh0:absNorm ↑P ≠ 0⊢ 2 ≤ absNorm ↑P have h1 : Ideal.absNorm P.val ≠ 1 := by intro hP:PrimeIdealh0:absNorm ↑P ≠ 0h:absNorm ↑P = 1⊢ False apply P.property.not_isUnitP:PrimeIdealh0:absNorm ↑P ≠ 0h:absNorm ↑P = 1⊢ IsUnit ↑P rw [Ideal.absNorm_eq_one_iff.mp hP:PrimeIdealh0:absNorm ↑P ≠ 0h:absNorm ↑P = 1⊢ IsUnit ⊤]P:PrimeIdealh0:absNorm ↑P ≠ 0h:absNorm ↑P = 1⊢ IsUnit ⊤ simpa only [Ideal.one_eq_top] using (show IsUnit (1 : Ideal ActualEisensteinCubic.O) from isUnit_one)P:PrimeIdealh0:absNorm ↑P ≠ 0h1:absNorm ↑P ≠ 1⊢ 2 ≤ absNorm ↑P omegaAll goals completed! 🐙lemma prime_norm_pos (P : PrimeIdeal) : (0 : ℝ) < Ideal.absNorm P.val := byP:PrimeIdeal⊢ 0 < ↑(absNorm ↑P) have h := prime_norm_two_le PP:PrimeIdealh:2 ≤ absNorm ↑P⊢ 0 < ↑(absNorm ↑P) exact_mod_cast (byP:PrimeIdealh:2 ≤ absNorm ↑P⊢ 0 < absNorm ↑P omegaAll goals completed! 🐙 : 0 < Ideal.absNorm P.val)def primeNormPower (P : PrimeIdeal) (s : ℂ) : ℂ := (Ideal.absNorm P.val : ℂ)^(-s)def primeCharacterTerm {q : ℕ} (χ : DirichletCharacter ℂ q) (P : PrimeIdeal) (s : ℂ) : ℂ := χ (Ideal.absNorm P.val) * primeNormPower P sdef primeDensity (P : PrimeIdeal) : ℂ := 1-(1:ℂ)/(Ideal.absNorm P.val:ℂ)lemma norm_primeNormPower (P : PrimeIdeal) (s : ℂ) : ‖primeNormPower P s‖=(Ideal.absNorm P.val : ℝ)^(-s.re) := byP:PrimeIdeals:ℂ⊢ ‖primeNormPower P s‖ = ↑(absNorm ↑P) ^ (-s.re) exact Complex.norm_cpow_eq_rpow_re_of_pos (prime_norm_pos P) (-s)All goals completed! 🐙lemma primeDensity_norm_le_one (P : PrimeIdeal) : ‖primeDensity P‖≤1 := byP:PrimeIdeal⊢ ‖primeDensity P‖ ≤ 1 have hn := prime_norm_pos PP:PrimeIdealhn:0 < ↑(absNorm ↑P)⊢ ‖primeDensity P‖ ≤ 1 have hn1 : (1:ℝ)≤Ideal.absNorm P.val := by exact_mod_cast (byP:PrimeIdealhn:0 < ↑(absNorm ↑P)⊢ 1 ≤ absNorm ↑P have:=prime_norm_two_le PP:PrimeIdealhn:0 < ↑(absNorm ↑P)this:2 ≤ absNorm ↑P⊢ 1 ≤ absNorm ↑P;omegaAll goals completed! 🐙)P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)⊢ ‖primeDensity P‖ ≤ 1 have he : primeDensity P = ((1-(1:ℝ)/(Ideal.absNorm P.val:ℝ):ℝ):ℂ) := by simp [primeDensity]P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ ‖primeDensity P‖ ≤ 1 rw [he,P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ ‖↑(1 - 1 / ↑(absNorm ↑P))‖ ≤ 1Complex.norm_real,P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ ‖1 - 1 / ↑(absNorm ↑P)‖ ≤ 1Real.norm_eq_abs,P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ |1 - 1 / ↑(absNorm ↑P)| ≤ 1abs_of_nonnegP:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ 1 - 1 / ↑(absNorm ↑P) ≤ 1P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ 0 ≤ 1 - 1 / ↑(absNorm ↑P)]P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ 1 - 1 / ↑(absNorm ↑P) ≤ 1P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ 0 ≤ 1 - 1 / ↑(absNorm ↑P) ·P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ 1 - 1 / ↑(absNorm ↑P) ≤ 1 have : (0:ℝ)≤1/(Ideal.absNorm P.val:ℝ) := byP:PrimeIdeal⊢ ‖primeDensity P‖ ≤ 1 positivityP:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))this:0 ≤ 1 / ↑(absNorm ↑P)⊢ 1 - 1 / ↑(absNorm ↑P) ≤ 1 linarithAll goals completed! 🐙 ·P:PrimeIdealhn:0 < ↑(absNorm ↑P)hn1:1 ≤ ↑(absNorm ↑P)he:primeDensity P = ↑(1 - 1 / ↑(absNorm ↑P))⊢ 0 ≤ 1 - 1 / ↑(absNorm ↑P) exact sub_nonneg.mpr ((div_le_one hn).mpr hn1)All goals completed! 🐙lemma primeCharacterTerm_norm_le {q : ℕ} (χ : DirichletCharacter ℂ q) (P : PrimeIdeal) (s : ℂ) (σ : ℝ) (hs : σ≤s.re) : ‖primeCharacterTerm χ P s‖≤(Ideal.absNorm P.val:ℝ)^(-σ) := byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.re⊢ ‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ) rw [primeCharacterTerm,q:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.re⊢ ‖χ ↑(absNorm ↑P) * primeNormPower P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)norm_mul,q:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.re⊢ ‖χ ↑(absNorm ↑P)‖ * ‖primeNormPower P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)norm_primeNormPowerq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.re⊢ ‖χ ↑(absNorm ↑P)‖ * ↑(absNorm ↑P) ^ (-s.re) ≤ ↑(absNorm ↑P) ^ (-σ)]q:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.re⊢ ‖χ ↑(absNorm ↑P)‖ * ↑(absNorm ↑P) ^ (-s.re) ≤ ↑(absNorm ↑P) ^ (-σ) have hn1 : (1:ℝ)≤Ideal.absNorm P.val := byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.re⊢ ‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ) exact_mod_cast (byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.re⊢ 1 ≤ absNorm ↑P have:=prime_norm_two_le Pq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.rethis:2 ≤ absNorm ↑P⊢ 1 ≤ absNorm ↑P;omegaAll goals completed! 🐙)q:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.rehn1:1 ≤ ↑(absNorm ↑P)⊢ ‖χ ↑(absNorm ↑P)‖ * ↑(absNorm ↑P) ^ (-s.re) ≤ ↑(absNorm ↑P) ^ (-σ) calc _ ≤ 1*(Ideal.absNorm P.val:ℝ)^(-s.re) := mul_le_mul_of_nonneg_right (χ.norm_le_one _) (byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.rehn1:1 ≤ ↑(absNorm ↑P)⊢ 0 ≤ ↑(absNorm ↑P) ^ (-s.re) positivityAll goals completed! 🐙) _ ≤ _ := byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.rehn1:1 ≤ ↑(absNorm ↑P)⊢ 1 * ↑(absNorm ↑P) ^ (-s.re) ≤ ↑(absNorm ↑P) ^ (-σ) rw [one_mulq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.rehn1:1 ≤ ↑(absNorm ↑P)⊢ ↑(absNorm ↑P) ^ (-s.re) ≤ ↑(absNorm ↑P) ^ (-σ)]q:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂσ:ℝhs:σ ≤ s.rehn1:1 ≤ ↑(absNorm ↑P)⊢ ↑(absNorm ↑P) ^ (-s.re) ≤ ↑(absNorm ↑P) ^ (-σ); exact Real.rpow_le_rpow_of_exponent_le hn1 (neg_le_neg hs)All goals completed! 🐙lemma primeCharacterTerm_norm_lt_one {q : ℕ} (χ : DirichletCharacter ℂ q) (P : PrimeIdeal) (s : ℂ) (hs : 0<s.re) : ‖primeCharacterTerm χ P s‖<1 := byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ ‖primeCharacterTerm χ P s‖ < 1 apply (primeCharacterTerm_norm_le χ P s s.re le_rfl).trans_ltq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ ↑(absNorm ↑P) ^ (-s.re) < 1 exact Real.rpow_lt_one_of_one_lt_of_neg (byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ 1 < ↑(absNorm ↑P) have:=prime_norm_two_le Pq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.rethis:2 ≤ absNorm ↑P⊢ 1 < ↑(absNorm ↑P);exact_mod_cast (byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.rethis:2 ≤ absNorm ↑P⊢ 1 < absNorm ↑P omegaAll goals completed! 🐙:1<Ideal.absNorm P.val)) (byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ -s.re < 0 linarithAll goals completed! 🐙)lemma one_sub_ne_zero {x : ℂ} (hx : ‖x‖<1) : 1-x≠0 := byx:ℂhx:‖x‖ < 1⊢ 1 - x ≠ 0 intro hx:ℂhx:‖x‖ < 1h:1 - x = 0⊢ False have he : x=1 := (sub_eq_zero.mp h).symmx:ℂhx:‖x‖ < 1h:1 - x = 0he:x = 1⊢ False simp [he] at hxAll goals completed! 🐙lemma correctionDenominator_ne_zero {q : ℕ} (χ : DirichletCharacter ℂ q) (P : PrimeIdeal) (s : ℂ) (hs : 0<s.re) : 1-primeDensity P*primeCharacterTerm χ P s≠0 := byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ 1 - primeDensity P * primeCharacterTerm χ P s ≠ 0 apply one_sub_ne_zeroq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ ‖primeDensity P * primeCharacterTerm χ P s‖ < 1 rw [norm_mulq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ ‖primeDensity P‖ * ‖primeCharacterTerm χ P s‖ < 1]q:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ ‖primeDensity P‖ * ‖primeCharacterTerm χ P s‖ < 1 calc _ ≤ 1*‖primeCharacterTerm χ P s‖ := mul_le_mul_of_nonneg_right (primeDensity_norm_le_one P) (norm_nonneg _) _ < 1 := byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ 1 * ‖primeCharacterTerm χ P s‖ < 1 rw [one_mulq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ ‖primeCharacterTerm χ P s‖ < 1]q:ℕχ:DirichletCharacter ℂ qP:PrimeIdeals:ℂhs:0 < s.re⊢ ‖primeCharacterTerm χ P s‖ < 1;exact primeCharacterTerm_norm_lt_one χ P s hsAll goals completed! 🐙def correctionTerm {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (P : PrimeIdeal) (s : ℂ) : ℂ := if P.val∈S then 0 else -((1:ℂ)/(Ideal.absNorm P.val:ℂ))*primeCharacterTerm χ P s / (1-primeDensity P*primeCharacterTerm χ P s)def eulerCorrection {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) : ℂ := ∏' P : PrimeIdeal, (1+correctionTerm χ S P s)lemma correctionTerm_factor {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (P : PrimeIdeal) (s : ℂ) (hs : 0<s.re) : 1+correctionTerm χ S P s = if P.val∈S then 1 else (1-primeCharacterTerm χ P s)/(1-primeDensity P*primeCharacterTerm χ P s) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.re⊢ 1 + correctionTerm χ S P s = if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s) by_cases hP : P.val∈Sposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∈ S⊢ 1 + correctionTerm χ S P s = if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ S⊢ 1 + correctionTerm χ S P s = if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s) ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∈ S⊢ 1 + correctionTerm χ S P s = if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s) simp [correctionTerm,hP]All goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ S⊢ 1 + correctionTerm χ S P s = if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s) simp only [correctionTerm,ite_eq_right hP]negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ S⊢ 1 + -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s) = (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s) have hd := correctionDenominator_ne_zero χ P s hsnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ Shd:1 - primeDensity P * primeCharacterTerm χ P s ≠ 0⊢ 1 + -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s) = (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s) apply (eq_div_iff hd).mprnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ Shd:1 - primeDensity P * primeCharacterTerm χ P s ≠ 0⊢ (1 + -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)) * (1 - primeDensity P * primeCharacterTerm χ P s) = 1 - primeCharacterTerm χ P s rw [add_mul,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ Shd:1 - primeDensity P * primeCharacterTerm χ P s ≠ 0⊢ 1 * (1 - primeDensity P * primeCharacterTerm χ P s) + -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s) * (1 - primeDensity P * primeCharacterTerm χ P s) = 1 - primeCharacterTerm χ P s one_mul,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ Shd:1 - primeDensity P * primeCharacterTerm χ P s ≠ 0⊢ 1 - primeDensity P * primeCharacterTerm χ P s + -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s) * (1 - primeDensity P * primeCharacterTerm χ P s) = 1 - primeCharacterTerm χ P s div_mul_cancel₀ _ hdnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ Shd:1 - primeDensity P * primeCharacterTerm χ P s ≠ 0⊢ 1 - primeDensity P * primeCharacterTerm χ P s + -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s = 1 - primeCharacterTerm χ P s]negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ Shd:1 - primeDensity P * primeCharacterTerm χ P s ≠ 0⊢ 1 - primeDensity P * primeCharacterTerm χ P s + -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s = 1 - primeCharacterTerm χ P s dsimp [primeDensity]negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ Shd:1 - primeDensity P * primeCharacterTerm χ P s ≠ 0⊢ 1 - (1 - 1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s + -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s = 1 - primeCharacterTerm χ P s ringAll goals completed! 🐙lemma correctionFactor_ne_zero {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (P : PrimeIdeal) (s : ℂ) (hs : 0<s.re) : 1+correctionTerm χ S P s≠0 := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.re⊢ 1 + correctionTerm χ S P s ≠ 0 rw [correctionTerm_factor χ S P s hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.re⊢ (if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) ≠ 0]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.re⊢ (if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) ≠ 0 split_ifsposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.reh✝:↑P ∈ S⊢ 1 ≠ 0negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.reh✝:↑P ∉ S⊢ (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s) ≠ 0 ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.reh✝:↑P ∈ S⊢ 1 ≠ 0 exact one_ne_zeroAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.reh✝:↑P ∉ S⊢ (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s) ≠ 0 exact div_ne_zero (one_sub_ne_zero (primeCharacterTerm_norm_lt_one χ P s hs)) (correctionDenominator_ne_zero χ P s hs)All goals completed! 🐙lemma correctionTerm_uniform_bound {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (σ : ℝ) (hσ : 0<σ) (P : PrimeIdeal) (s : ℂ) (hs : σ≤s.re) : ‖correctionTerm χ S P s‖ ≤ (1-(2:ℝ)^(-σ))⁻¹*(Ideal.absNorm P.val:ℝ)^(-(1+σ)) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.re⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) have hn := prime_norm_pos Pq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) have hn2 : (2:ℝ)≤Ideal.absNorm P.val := by exact_mod_cast prime_norm_two_le Pq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) have hr : (2:ℝ)^(-σ)<1 := Real.rpow_lt_one_of_one_lt_of_neg (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)⊢ 1 < 2 norm_numAll goals completed! 🐙) (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)⊢ -σ < 0 linarithAll goals completed! 🐙)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) have hr0 : 0<1-(2:ℝ)^(-σ) := sub_pos.mpr hrq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) have hx := primeCharacterTerm_norm_le χ P s σ hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) have hx2 : ‖primeCharacterTerm χ P s‖≤(2:ℝ)^(-σ) := hx.trans (Real.rpow_le_rpow_of_nonpos (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)⊢ 0 < 2 norm_numAll goals completed! 🐙) hn2 (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)⊢ -σ ≤ 0 linarithAll goals completed! 🐙))q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) have hd : 1-(2:ℝ)^(-σ)≤‖1-primeDensity P*primeCharacterTerm χ P s‖ := by have hb : ‖primeDensity P*primeCharacterTerm χ P s‖≤(2:ℝ)^(-σ) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.re⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) rw [norm_mulq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)⊢ ‖primeDensity P‖ * ‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)⊢ ‖primeDensity P‖ * ‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ) calc _ ≤ 1*‖primeCharacterTerm χ P s‖ := mul_le_mul_of_nonneg_right (primeDensity_norm_le_one P) (norm_nonneg _) _ ≤ _ := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)⊢ 1 * ‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ) simpa using hx2q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hb:‖primeDensity P * primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)⊢ 1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖ have hh := norm_sub_norm_le (1:ℂ) (primeDensity P*primeCharacterTerm χ P s)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hb:‖primeDensity P * primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hh:‖1‖ - ‖primeDensity P * primeCharacterTerm χ P s‖ ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖⊢ 1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖ simpa only [norm_one] using (show 1-(2:ℝ)^(-σ) ≤ ‖(1:ℂ)‖-‖primeDensity P*primeCharacterTerm χ P s‖ from byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hb:‖primeDensity P * primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hh:‖1‖ - ‖primeDensity P * primeCharacterTerm χ P s‖ ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖⊢ 1 - 2 ^ (-σ) ≤ ‖1‖ - ‖primeDensity P * primeCharacterTerm χ P s‖ simpa using sub_le_sub_left hb 1All goals completed! 🐙) |>.trans hhq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) by_cases hP : P.val∈Sposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∈ S⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ))negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∈ S⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) simp only [correctionTerm,ite_eq_left hP,norm_zero]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∈ S⊢ 0 ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) positivityAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ ‖correctionTerm χ S P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) rw [correctionTerm,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ ‖if ↑P ∈ S then 0 else -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ))ite_eq_right hP,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ ‖-(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ))norm_div,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ ‖-(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s‖ / ‖1 - primeDensity P * primeCharacterTerm χ P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ))norm_mul,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ ‖-(1 / ↑(absNorm ↑P))‖ * ‖primeCharacterTerm χ P s‖ / ‖1 - primeDensity P * primeCharacterTerm χ P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ))norm_neg,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ ‖1 / ↑(absNorm ↑P)‖ * ‖primeCharacterTerm χ P s‖ / ‖1 - primeDensity P * primeCharacterTerm χ P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ))norm_div,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ ‖1‖ / ‖↑(absNorm ↑P)‖ * ‖primeCharacterTerm χ P s‖ / ‖1 - primeDensity P * primeCharacterTerm χ P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ))norm_one,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 1 / ‖↑(absNorm ↑P)‖ * ‖primeCharacterTerm χ P s‖ / ‖1 - primeDensity P * primeCharacterTerm χ P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ))Complex.norm_natCastnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 1 / ↑(absNorm ↑P) * ‖primeCharacterTerm χ P s‖ / ‖1 - primeDensity P * primeCharacterTerm χ P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ))]negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 1 / ↑(absNorm ↑P) * ‖primeCharacterTerm χ P s‖ / ‖1 - primeDensity P * primeCharacterTerm χ P s‖ ≤ (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) calc _ ≤ ((1:ℝ)/(Ideal.absNorm P.val:ℝ)*(Ideal.absNorm P.val:ℝ)^(-σ))/(1-(2:ℝ)^(-σ)) := div_le_div₀ (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 0 ≤ 1 / ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-σ) positivityAll goals completed! 🐙) (mul_le_mul_of_nonneg_left hx (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 0 ≤ 1 / ↑(absNorm ↑P) positivityAll goals completed! 🐙)) hr0 hd _ = _ := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 1 / ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-σ) / (1 - 2 ^ (-σ)) = (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) rw [show -(1+σ)=(-1)+(-σ) byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 1 / ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-σ) / (1 - 2 ^ (-σ)) = (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + σ)) ringAll goals completed! 🐙,Real.rpow_add hn,q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 1 / ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-σ) / (1 - 2 ^ (-σ)) = (1 - 2 ^ (-σ))⁻¹ * (↑(absNorm ↑P) ^ (-1) * ↑(absNorm ↑P) ^ (-σ))Real.rpow_neg_oneq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 1 / ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-σ) / (1 - 2 ^ (-σ)) = (1 - 2 ^ (-σ))⁻¹ * ((↑(absNorm ↑P))⁻¹ * ↑(absNorm ↑P) ^ (-σ))]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σP:PrimeIdeals:ℂhs:σ ≤ s.rehn:0 < ↑(absNorm ↑P)hn2:2 ≤ ↑(absNorm ↑P)hr:2 ^ (-σ) < 1hr0:0 < 1 - 2 ^ (-σ)hx:‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-σ)hx2:‖primeCharacterTerm χ P s‖ ≤ 2 ^ (-σ)hd:1 - 2 ^ (-σ) ≤ ‖1 - primeDensity P * primeCharacterTerm χ P s‖hP:↑P ∉ S⊢ 1 / ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-σ) / (1 - 2 ^ (-σ)) = (1 - 2 ^ (-σ))⁻¹ * ((↑(absNorm ↑P))⁻¹ * ↑(absNorm ↑P) ^ (-σ)) ringAll goals completed! 🐙lemma prime_norm_series_summable (σ : ℝ) (hσ : 0<σ) : Summable (fun P : PrimeIdeal => (Ideal.absNorm P.val:ℝ)^(-(1+σ))) := byσ:ℝhσ:0 < σ⊢ Summable fun P => ↑(absNorm ↑P) ^ (-(1 + σ)) have ht := (CubicEisenstein.fullIdealWeight_summable_norm (1+(σ:ℂ)) (byσ:ℝhσ:0 < σ⊢ 1 < (1 + ↑σ).re simpσ:ℝhσ:0 < σ⊢ 0 < σ;linarithAll goals completed! 🐙)).comp_injective (i := fun P : PrimeIdeal => P.val) Subtype.val_injectiveσ:ℝhσ:0 < σht:Summable ((fun I => ‖CubicEisenstein.fullIdealWeight (1 + ↑σ) I‖) ∘ fun P => ↑P)⊢ Summable fun P => ↑(absNorm ↑P) ^ (-(1 + σ)) apply ht.congrσ:ℝhσ:0 < σht:Summable ((fun I => ‖CubicEisenstein.fullIdealWeight (1 + ↑σ) I‖) ∘ fun P => ↑P)⊢ ∀ (b : PrimeIdeal), ((fun I => ‖CubicEisenstein.fullIdealWeight (1 + ↑σ) I‖) ∘ fun P => ↑P) b = ↑(absNorm ↑b) ^ (-(1 + σ)) intro Pσ:ℝhσ:0 < σht:Summable ((fun I => ‖CubicEisenstein.fullIdealWeight (1 + ↑σ) I‖) ∘ fun P => ↑P)P:PrimeIdeal⊢ ((fun I => ‖CubicEisenstein.fullIdealWeight (1 + ↑σ) I‖) ∘ fun P => ↑P) P = ↑(absNorm ↑P) ^ (-(1 + σ)) simp only [Function.comp_def,CubicEisenstein.fullIdealWeight,ite_eq_right P.property.ne_zero]σ:ℝhσ:0 < σht:Summable ((fun I => ‖CubicEisenstein.fullIdealWeight (1 + ↑σ) I‖) ∘ fun P => ↑P)P:PrimeIdeal⊢ ‖↑(absNorm ↑P) ^ (-(1 + ↑σ))‖ = ↑(absNorm ↑P) ^ (-(1 + σ)) simpa only [Complex.neg_re, Complex.add_re, Complex.one_re, Complex.ofReal_re, Complex.ofReal_natCast] using (Complex.norm_cpow_eq_rpow_re_of_pos (prime_norm_pos P) (-(1+(σ:ℂ))))All goals completed! 🐙lemma correctionTerm_summable {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (hs : 0<s.re) : Summable (fun P : PrimeIdeal => ‖correctionTerm χ S P s‖) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:0 < s.re⊢ Summable fun P => ‖correctionTerm χ S P s‖ apply Summable.of_nonneg_of_le (fun _ => norm_nonneg _) (fun P => correctionTerm_uniform_bound χ S s.re hs P s le_rfl)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:0 < s.re⊢ Summable fun P => (1 - 2 ^ (-s.re))⁻¹ * ↑(absNorm ↑P) ^ (-(1 + s.re)) exact (prime_norm_series_summable s.re hs).mul_left _All goals completed! 🐙theorem eulerCorrection_ne_zero {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (hs : 0<s.re) : eulerCorrection χ S s≠0 := tprod_one_add_ne_zero_of_summable (fun P => correctionFactor_ne_zero χ S P s hs) (correctionTerm_summable χ S s hs)lemma primeCharacterTerm_differentiable {q : ℕ} (χ : DirichletCharacter ℂ q) (P : PrimeIdeal) : Differentiable ℂ (primeCharacterTerm χ P) := byq:ℕχ:DirichletCharacter ℂ qP:PrimeIdeal⊢ Differentiable ℂ (primeCharacterTerm χ P) have hn : (Ideal.absNorm P.val:ℂ)≠0 := by exact_mod_cast (ne_of_gt (prime_norm_pos P))q:ℕχ:DirichletCharacter ℂ qP:PrimeIdealhn:↑(absNorm ↑P) ≠ 0⊢ Differentiable ℂ (primeCharacterTerm χ P) exact ((differentiable_id.neg).const_cpow (Or.inl hn)).const_mul _All goals completed! 🐙lemma correctionTerm_differentiableOn {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (P : PrimeIdeal) (σ : ℝ) (hσ : 0≤σ) : DifferentiableOn ℂ (correctionTerm χ S P) {s:ℂ | σ<s.re} := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdealσ:ℝhσ:0 ≤ σ⊢ DifferentiableOn ℂ (correctionTerm χ S P) {s | σ < s.re} unfold correctionTermq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdealσ:ℝhσ:0 ≤ σ⊢ DifferentiableOn ℂ (fun s => if ↑P ∈ S then 0 else -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)) {s | σ < s.re} by_cases hP : P.val∈Sposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdealσ:ℝhσ:0 ≤ σhP:↑P ∈ S⊢ DifferentiableOn ℂ (fun s => if ↑P ∈ S then 0 else -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)) {s | σ < s.re}negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdealσ:ℝhσ:0 ≤ σhP:↑P ∉ S⊢ DifferentiableOn ℂ (fun s => if ↑P ∈ S then 0 else -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)) {s | σ < s.re} ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdealσ:ℝhσ:0 ≤ σhP:↑P ∈ S⊢ DifferentiableOn ℂ (fun s => if ↑P ∈ S then 0 else -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)) {s | σ < s.re} simpa only [ite_eq_left hP] using (differentiableOn_const (𝕜 := ℂ) (s := {s:ℂ | σ<s.re}) (c := (0:ℂ)))All goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdealσ:ℝhσ:0 ≤ σhP:↑P ∉ S⊢ DifferentiableOn ℂ (fun s => if ↑P ∈ S then 0 else -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)) {s | σ < s.re} simp only [ite_eq_right hP]negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdealσ:ℝhσ:0 ≤ σhP:↑P ∉ S⊢ DifferentiableOn ℂ (fun s => -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)) {s | σ < s.re} intro s hsnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdealσ:ℝhσ:0 ≤ σhP:↑P ∉ Ss:ℂhs:s ∈ {s | σ < s.re}⊢ DifferentiableWithinAt ℂ (fun s => -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)) {s | σ < s.re} s have hx := primeCharacterTerm_differentiable χ P snegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdealσ:ℝhσ:0 ≤ σhP:↑P ∉ Ss:ℂhs:s ∈ {s | σ < s.re}hx:DifferentiableAt ℂ (primeCharacterTerm χ P) s⊢ DifferentiableWithinAt ℂ (fun s => -(1 / ↑(absNorm ↑P)) * primeCharacterTerm χ P s / (1 - primeDensity P * primeCharacterTerm χ P s)) {s | σ < s.re} s convert ((hx.const_mul (-((1:ℂ)/(Ideal.absNorm P.val:ℂ)))).div ((differentiableAt_const (1:ℂ)).sub (hx.const_mul (primeDensity P))) (correctionDenominator_ne_zero χ P s (lt_of_le_of_lt hσ hs))).differentiableWithinAt using 1All goals completed! 🐙lemma eulerCorrection_locally_uniform {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (σ : ℝ) (hσ : 0<σ) : HasProdLocallyUniformlyOn (fun P s => 1+correctionTerm χ S P s) (eulerCorrection χ S) {s:ℂ | σ<s.re} := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σ⊢ HasProdLocallyUniformlyOn (fun P s => 1 + correctionTerm χ S P s) (eulerCorrection χ S) {s | σ < s.re} have hu := (prime_norm_series_summable σ hσ).mul_left ((1-(2:ℝ)^(-σ))⁻¹)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σhu:Summable fun i => (1 - 2 ^ (-σ))⁻¹ * ↑(absNorm ↑i) ^ (-(1 + σ))⊢ HasProdLocallyUniformlyOn (fun P s => 1 + correctionTerm χ S P s) (eulerCorrection χ S) {s | σ < s.re} exact hu.hasProdLocallyUniformlyOn_one_add (isOpen_lt continuous_const Complex.continuous_re) (Filter.Eventually.of_forall (fun P s hs => correctionTerm_uniform_bound χ S σ hσ P s hs.le)) (fun P => (correctionTerm_differentiableOn χ S P σ hσ.le).continuousOn)All goals completed! 🐙theorem eulerCorrection_differentiableOn_halfplane {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (σ : ℝ) (hσ : 0<σ) : DifferentiableOn ℂ (eulerCorrection χ S) {s:ℂ | σ<s.re} := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σ⊢ DifferentiableOn ℂ (eulerCorrection χ S) {s | σ < s.re} apply (eulerCorrection_locally_uniform χ S σ hσ).differentiableOnhFq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σ⊢ ∀ᶠ (n : Finset PrimeIdeal) in atTop, DifferentiableOn ℂ (fun x2 => ∏ i ∈ n, (fun P s => 1 + correctionTerm χ S P s) i x2) {s | σ < s.re}hUq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σ⊢ IsOpen {s | σ < s.re} ·hFq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σ⊢ ∀ᶠ (n : Finset PrimeIdeal) in atTop, DifferentiableOn ℂ (fun x2 => ∏ i ∈ n, (fun P s => 1 + correctionTerm χ S P s) i x2) {s | σ < s.re} apply Filter.Eventually.of_forallhFq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σ⊢ ∀ (x : Finset PrimeIdeal), DifferentiableOn ℂ (fun x2 => ∏ i ∈ x, (fun P s => 1 + correctionTerm χ S P s) i x2) {s | σ < s.re} intro thFq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σt:Finset PrimeIdeal⊢ DifferentiableOn ℂ (fun x2 => ∏ i ∈ t, (fun P s => 1 + correctionTerm χ S P s) i x2) {s | σ < s.re} change DifferentiableOn ℂ (fun z => ∏ P ∈ t, (1+correctionTerm χ S P z)) _hFq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σt:Finset PrimeIdeal⊢ DifferentiableOn ℂ (fun z => ∏ P ∈ t, (1 + correctionTerm χ S P z)) {s | σ < s.re} apply DifferentiableOn.fun_finsetProdhFq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σt:Finset PrimeIdeal⊢ ∀ i ∈ t, DifferentiableOn ℂ (fun x => 1 + correctionTerm χ S i x) {s | σ < s.re} intro P hPhFq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σt:Finset PrimeIdealP:PrimeIdealhP:P ∈ t⊢ DifferentiableOn ℂ (fun x => 1 + correctionTerm χ S P x) {s | σ < s.re} exact (differentiableOn_const (𝕜 := ℂ) (c := (1:ℂ))).add (correctionTerm_differentiableOn χ S P σ hσ.le)All goals completed! 🐙 ·hUq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)σ:ℝhσ:0 < σ⊢ IsOpen {s | σ < s.re} exact isOpen_lt continuous_const Complex.continuous_reAll goals completed! 🐙theorem eulerCorrection_differentiableOn {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) : DifferentiableOn ℂ (eulerCorrection χ S) {s:ℂ | 0<s.re} := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)⊢ DifferentiableOn ℂ (eulerCorrection χ S) {s | 0 < s.re} intro s hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:s ∈ {s | 0 < s.re}⊢ DifferentiableWithinAt ℂ (eulerCorrection χ S) {s | 0 < s.re} s have hh := eulerCorrection_differentiableOn_halfplane χ S (s.re/2) (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:s ∈ {s | 0 < s.re}⊢ 0 < s.re / 2 dsimp at hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:0 < s.re⊢ 0 < s.re / 2;linarithAll goals completed! 🐙)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:s ∈ {s | 0 < s.re}hh:DifferentiableOn ℂ (eulerCorrection χ S) {s_1 | s.re / 2 < s_1.re}⊢ DifferentiableWithinAt ℂ (eulerCorrection χ S) {s | 0 < s.re} s exact (hh.differentiableAt ((isOpen_lt continuous_const Complex.continuous_re).mem_nhds (show s∈{z:ℂ | s.re/2<z.re} byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)⊢ DifferentiableOn ℂ (eulerCorrection χ S) {s | 0 < s.re} dsimp at *q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:0 < s.rehh:DifferentiableOn ℂ (eulerCorrection χ S) {s_1 | s.re / 2 < s_1.re}⊢ s.re / 2 < s.re;linarithAll goals completed! 🐙))).differentiableWithinAtendsectionopen ActualEisensteinCubicopen ShortDraftHeckeBridge hiding Oopen IdealMobiusDivisorSum hiding Oopen UniqueFactorizationMonoidopen CanonicalRowCompletion (primeValueHom primeValueHom_prime)lemma prod_primeSet {M : Type*} [CommMonoid M] (I : Ideal ActualEisensteinCubic.O) (f : Ideal ActualEisensteinCubic.O→M) : (∏P∈primeSet I,f P.val)=∏P∈primeSupport I,f P := byM:Type u_1inst✝:CommMonoid MI:Ideal ActualEisensteinCubic.Of:Ideal ActualEisensteinCubic.O → M⊢ ∏ P ∈ primeSet I, f ↑P = ∏ P ∈ primeSupport I, f P unfold primeSetM:Type u_1inst✝:CommMonoid MI:Ideal ActualEisensteinCubic.Of:Ideal ActualEisensteinCubic.O → M⊢ ∏ P ∈ Finset.image (fun P => ⟨↑P, ⋯⟩) (primeSupport I).attach, f ↑P = ∏ P ∈ primeSupport I, f P rw [Finset.prod_imageM:Type u_1inst✝:CommMonoid MI:Ideal ActualEisensteinCubic.Of:Ideal ActualEisensteinCubic.O → M⊢ ∏ x ∈ (primeSupport I).attach, f ↑⟨↑x, ⋯⟩ = ∏ P ∈ primeSupport I, f PM:Type u_1inst✝:CommMonoid MI:Ideal ActualEisensteinCubic.Of:Ideal ActualEisensteinCubic.O → M⊢ InjOn (fun P => ⟨↑P, ⋯⟩) ↑(primeSupport I).attach]M:Type u_1inst✝:CommMonoid MI:Ideal ActualEisensteinCubic.Of:Ideal ActualEisensteinCubic.O → M⊢ ∏ x ∈ (primeSupport I).attach, f ↑⟨↑x, ⋯⟩ = ∏ P ∈ primeSupport I, f PM:Type u_1inst✝:CommMonoid MI:Ideal ActualEisensteinCubic.Of:Ideal ActualEisensteinCubic.O → M⊢ InjOn (fun P => ⟨↑P, ⋯⟩) ↑(primeSupport I).attach ·M:Type u_1inst✝:CommMonoid MI:Ideal ActualEisensteinCubic.Of:Ideal ActualEisensteinCubic.O → M⊢ ∏ x ∈ (primeSupport I).attach, f ↑⟨↑x, ⋯⟩ = ∏ P ∈ primeSupport I, f P exact Finset.prod_attach (primeSupport I) fAll goals completed! 🐙 ·M:Type u_1inst✝:CommMonoid MI:Ideal ActualEisensteinCubic.Of:Ideal ActualEisensteinCubic.O → M⊢ InjOn (fun P => ⟨↑P, ⋯⟩) ↑(primeSupport I).attach intro P hP Q hQ heM:Type u_1inst✝:CommMonoid MI:Ideal ActualEisensteinCubic.Of:Ideal ActualEisensteinCubic.O → MP:↥(primeSupport I)hP:P ∈ ↑(primeSupport I).attachQ:↥(primeSupport I)hQ:Q ∈ ↑(primeSupport I).attachhe:(fun P => ⟨↑P, ⋯⟩) P = (fun P => ⟨↑P, ⋯⟩) Q⊢ P = Q exact Subtype.ext (congrArg (fun R : PrimeIdeal => R.val) he)All goals completed! 🐙lemma primeValueHom_squarefree (w : Ideal ActualEisensteinCubic.O→ℂ) (I : Ideal ActualEisensteinCubic.O) (hI : Squarefree I) : primeValueHom w I=∏P∈primeSet I,w P.val := byw:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ (primeValueHom w) I = ∏ P ∈ primeSet I, w ↑P calc _ = primeValueHom w (primeProduct (primeSet I)) := congrArg (primeValueHom w) (primeProduct_primeSet I hI).symm _ = _ := byw:Ideal ActualEisensteinCubic.O → ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ (primeValueHom w) (primeProduct (primeSet I)) = ∏ P ∈ primeSet I, w ↑P simp only [primeProduct,map_prod,primeValueHom_prime _ _ (Subtype.property _)]All goals completed! 🐙lemma outside_primeProduct_iff (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : ∀P∈S,Prime P) (t : Finset PrimeIdeal) : (∀P∈S,¬P∣primeProduct t) ↔ ∀Q∈t,Q.val∉S := byS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdeal⊢ (∀ P ∈ S, ¬P ∣ primeProduct t) ↔ ∀ Q ∈ t, ↑Q ∉ S constructormpS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdeal⊢ (∀ P ∈ S, ¬P ∣ primeProduct t) → ∀ Q ∈ t, ↑Q ∉ SmprS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdeal⊢ (∀ Q ∈ t, ↑Q ∉ S) → ∀ P ∈ S, ¬P ∣ primeProduct t ·mpS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdeal⊢ (∀ P ∈ S, ¬P ∣ primeProduct t) → ∀ Q ∈ t, ↑Q ∉ S intro h Q hQ hQSmpS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealh:∀ P ∈ S, ¬P ∣ primeProduct tQ:PrimeIdealhQ:Q ∈ thQS:↑Q ∈ S⊢ False apply h Q.val hQSmpS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealh:∀ P ∈ S, ¬P ∣ primeProduct tQ:PrimeIdealhQ:Q ∈ thQS:↑Q ∈ S⊢ ↑Q ∣ primeProduct t exact Finset.dvd_prod_of_mem (fun P : PrimeIdeal => P.val) hQAll goals completed! 🐙 ·mprS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdeal⊢ (∀ Q ∈ t, ↑Q ∉ S) → ∀ P ∈ S, ¬P ∣ primeProduct t intro h P hP hdmprS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealh:∀ Q ∈ t, ↑Q ∉ SP:Ideal ActualEisensteinCubic.OhP:P ∈ Shd:P ∣ primeProduct t⊢ False obtain ⟨Q,hQ,hPQ⟩ := ((hS P hP).dvd_finsetProd_iff (fun Q : PrimeIdeal => Q.val)).mp hdmprS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealh:∀ Q ∈ t, ↑Q ∉ SP:Ideal ActualEisensteinCubic.OhP:P ∈ Shd:P ∣ primeProduct tQ:PrimeIdealhQ:Q ∈ thPQ:P ∣ ↑Q⊢ False have he : P=Q.val := associated_iff_eq.mp (((hS P hP).dvd_prime_iff_associated Q.property).mp hPQ)mprS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealh:∀ Q ∈ t, ↑Q ∉ SP:Ideal ActualEisensteinCubic.OhP:P ∈ Shd:P ∣ primeProduct tQ:PrimeIdealhQ:Q ∈ thPQ:P ∣ ↑Qhe:P = ↑Q⊢ False exact h Q hQ (he ▸ hP)All goals completed! 🐙def outsideMask (S : Finset (Ideal ActualEisensteinCubic.O)) (I : Ideal ActualEisensteinCubic.O) : ℂ := if ∀P∈S,¬P∣I then 1 else 0lemma prod_cut_primes (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : ∀P∈S,Prime P) (t : Finset PrimeIdeal) (f : Ideal ActualEisensteinCubic.O→ℂ) : (∏Q∈t,if Q.val∈S then 0 else f Q.val)=outsideMask S (primeProduct t)*(∏Q∈t,f Q.val) := byS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂ⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = outsideMask S (primeProduct t) * ∏ Q ∈ t, f ↑Q by_cases ho : ∀P∈S,¬P∣primeProduct tposS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = outsideMask S (primeProduct t) * ∏ Q ∈ t, f ↑QnegS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:¬∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = outsideMask S (primeProduct t) * ∏ Q ∈ t, f ↑Q ·posS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = outsideMask S (primeProduct t) * ∏ Q ∈ t, f ↑Q rw [outsideMask,posS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = (if ∀ P ∈ S, ¬P ∣ primeProduct t then 1 else 0) * ∏ Q ∈ t, f ↑Qite_eq_left ho,posS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = 1 * ∏ Q ∈ t, f ↑Qone_mulposS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = ∏ Q ∈ t, f ↑Q]posS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = ∏ Q ∈ t, f ↑Q apply Finset.prod_congr rflposS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:∀ P ∈ S, ¬P ∣ primeProduct t⊢ ∀ x ∈ t, (if ↑x ∈ S then 0 else f ↑x) = f ↑x intro Q hQposS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:∀ P ∈ S, ¬P ∣ primeProduct tQ:PrimeIdealhQ:Q ∈ t⊢ (if ↑Q ∈ S then 0 else f ↑Q) = f ↑Q exact ite_eq_right ((outside_primeProduct_iff S hS t).mp ho Q hQ)All goals completed! 🐙 ·negS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:¬∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = outsideMask S (primeProduct t) * ∏ Q ∈ t, f ↑Q rw [outsideMask,negS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:¬∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = (if ∀ P ∈ S, ¬P ∣ primeProduct t then 1 else 0) * ∏ Q ∈ t, f ↑Qite_eq_right ho,negS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:¬∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = 0 * ∏ Q ∈ t, f ↑Qzero_mulnegS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:¬∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = 0]negS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:¬∀ P ∈ S, ¬P ∣ primeProduct t⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = 0 have hh : ¬∀Q∈t,Q.val∉S := fun h => ho ((outside_primeProduct_iff S hS t).mpr h)negS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:¬∀ P ∈ S, ¬P ∣ primeProduct thh:¬∀ Q ∈ t, ↑Q ∉ S⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = 0 push Not at hhnegS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:¬∀ P ∈ S, ¬P ∣ primeProduct thh:∃ Q ∈ t, ↑Q ∈ S⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = 0 obtain ⟨Q,hQ,hQS⟩ := hhnegS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Pt:Finset PrimeIdealf:Ideal ActualEisensteinCubic.O → ℂho:¬∀ P ∈ S, ¬P ∣ primeProduct tQ:PrimeIdealhQ:Q ∈ thQS:↑Q ∈ S⊢ (∏ Q ∈ t, if ↑Q ∈ S then 0 else f ↑Q) = 0 exact Finset.prod_eq_zero hQ (ite_eq_left hQS)All goals completed! 🐙lemma nat_cpow_prod {ι : Type*} (t : Finset ι) (N : ι→ℕ) (s : ℂ) : ((∏i∈t,N i : ℕ):ℂ)^s=∏i∈t,(N i:ℂ)^s := byι:Type u_1t:Finset ιN:ι → ℕs:ℂ⊢ ↑(∏ i ∈ t, N i) ^ s = ∏ i ∈ t, ↑(N i) ^ s classical induction t using Finset.induction_on with | empty =>emptyι:Type u_1N:ι → ℕs:ℂ⊢ ↑(∏ i ∈ ∅, N i) ^ s = ∏ i ∈ ∅, ↑(N i) ^ s simpAll goals completed! 🐙 | @insert i t hi ih =>insertι:Type u_1N:ι → ℕs:ℂi:ιt:Finset ιhi:i ∉ tih:↑(∏ i ∈ t, N i) ^ s = ∏ i ∈ t, ↑(N i) ^ s⊢ ↑(∏ i ∈ insert i t, N i) ^ s = ∏ i ∈ insert i t, ↑(N i) ^ s rw [Finset.prod_insert hi,insertι:Type u_1N:ι → ℕs:ℂi:ιt:Finset ιhi:i ∉ tih:↑(∏ i ∈ t, N i) ^ s = ∏ i ∈ t, ↑(N i) ^ s⊢ ↑(N i * ∏ x ∈ t, N x) ^ s = ∏ i ∈ insert i t, ↑(N i) ^ sFinset.prod_insert hi,insertι:Type u_1N:ι → ℕs:ℂi:ιt:Finset ιhi:i ∉ tih:↑(∏ i ∈ t, N i) ^ s = ∏ i ∈ t, ↑(N i) ^ s⊢ ↑(N i * ∏ x ∈ t, N x) ^ s = ↑(N i) ^ s * ∏ x ∈ t, ↑(N x) ^ sNat.cast_mul,insertι:Type u_1N:ι → ℕs:ℂi:ιt:Finset ιhi:i ∉ tih:↑(∏ i ∈ t, N i) ^ s = ∏ i ∈ t, ↑(N i) ^ s⊢ (↑(N i) * ↑(∏ x ∈ t, N x)) ^ s = ↑(N i) ^ s * ∏ x ∈ t, ↑(N x) ^ sComplex.natCast_mul_natCast_cpow,insertι:Type u_1N:ι → ℕs:ℂi:ιt:Finset ιhi:i ∉ tih:↑(∏ i ∈ t, N i) ^ s = ∏ i ∈ t, ↑(N i) ^ s⊢ ↑(N i) ^ s * ↑(∏ x ∈ t, N x) ^ s = ↑(N i) ^ s * ∏ x ∈ t, ↑(N x) ^ sihinsertι:Type u_1N:ι → ℕs:ℂi:ιt:Finset ιhi:i ∉ tih:↑(∏ i ∈ t, N i) ^ s = ∏ i ∈ t, ↑(N i) ^ s⊢ ↑(N i) ^ s * ∏ i ∈ t, ↑(N i) ^ s = ↑(N i) ^ s * ∏ x ∈ t, ↑(N x) ^ s]All goals completed! 🐙lemma primeNormTerm_prod {q : ℕ} (χ : DirichletCharacter ℂ q) (t : Finset PrimeIdeal) (s : ℂ) : (∏P∈t,χ (Ideal.absNorm P.val)*(Ideal.absNorm P.val:ℂ)^(-s))= χ (Ideal.absNorm (primeProduct t))*(Ideal.absNorm (primeProduct t):ℂ)^(-s) := byq:ℕχ:DirichletCharacter ℂ qt:Finset PrimeIdeals:ℂ⊢ ∏ P ∈ t, χ ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-s) = χ ↑(absNorm (primeProduct t)) * ↑(absNorm (primeProduct t)) ^ (-s) rw [Finset.prod_mul_distribq:ℕχ:DirichletCharacter ℂ qt:Finset PrimeIdeals:ℂ⊢ (∏ x ∈ t, χ ↑(absNorm ↑x)) * ∏ x ∈ t, ↑(absNorm ↑x) ^ (-s) = χ ↑(absNorm (primeProduct t)) * ↑(absNorm (primeProduct t)) ^ (-s)]q:ℕχ:DirichletCharacter ℂ qt:Finset PrimeIdeals:ℂ⊢ (∏ x ∈ t, χ ↑(absNorm ↑x)) * ∏ x ∈ t, ↑(absNorm ↑x) ^ (-s) = χ ↑(absNorm (primeProduct t)) * ↑(absNorm (primeProduct t)) ^ (-s) simp only [primeProduct,map_prod,Nat.cast_prod]q:ℕχ:DirichletCharacter ℂ qt:Finset PrimeIdeals:ℂ⊢ (∏ x ∈ t, χ ↑(absNorm ↑x)) * ∏ x ∈ t, ↑(absNorm ↑x) ^ (-s) = (∏ x ∈ t, χ ↑(absNorm ↑x)) * (∏ i ∈ t, ↑(absNorm ↑i)) ^ (-s) congr 1e_aq:ℕχ:DirichletCharacter ℂ qt:Finset PrimeIdeals:ℂ⊢ ∏ x ∈ t, ↑(absNorm ↑x) ^ (-s) = (∏ i ∈ t, ↑(absNorm ↑i)) ^ (-s) simpa only [Nat.cast_prod] using (nat_cpow_prod t (fun P=>Ideal.absNorm P.val) (-s)).symmAll goals completed! 🐙def ordinaryPrimeValue {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (I : Ideal ActualEisensteinCubic.O) : ℂ := if I∈S then 0 else χ (Ideal.absNorm I)*(Ideal.absNorm I:ℂ)^(-s)def dampedPrimeValue {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (I : Ideal ActualEisensteinCubic.O) : ℂ := if I∈S then 0 else (1-(1:ℂ)/(Ideal.absNorm I:ℂ))*(χ (Ideal.absNorm I)*(Ideal.absNorm I:ℂ)^(-s))def ordinarySeriesTerm {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (I : Ideal ActualEisensteinCubic.O) : ℂ := outsideMask S I * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s Idef dampedSeriesTerm {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (I : Ideal ActualEisensteinCubic.O) : ℂ := ordinarySeriesTerm χ S s I * SixthPowerAverage.totientDensity Ilemma ordinarySeriesTerm_eq {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : ∀P∈S,Prime P) (s : ℂ) (I : Ideal ActualEisensteinCubic.O) : ordinarySeriesTerm χ S s I = mobiusPrimeCoeff (ordinaryPrimeValue χ S s) I := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.O⊢ ordinarySeriesTerm χ S s I = mobiusPrimeCoeff (ordinaryPrimeValue χ S s) I by_cases hI : Squarefree Iposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = mobiusPrimeCoeff (ordinaryPrimeValue χ S s) Inegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:¬Squarefree I⊢ ordinarySeriesTerm χ S s I = mobiusPrimeCoeff (ordinaryPrimeValue χ S s) I ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = mobiusPrimeCoeff (ordinaryPrimeValue χ S s) I rw [mobiusPrimeCoeff,posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = ↑(moebius I) * (primeValueHom (ordinaryPrimeValue χ S s)) IprimeValueHom_squarefree _ I hIposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = ↑(moebius I) * ∏ P ∈ primeSet I, ordinaryPrimeValue χ S s ↑P]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = ↑(moebius I) * ∏ P ∈ primeSet I, ordinaryPrimeValue χ S s ↑P simp only [ordinaryPrimeValue]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = ↑(moebius I) * ∏ P ∈ primeSet I, if ↑P ∈ S then 0 else χ ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-s) rw [prod_cut_primes S hS (primeSet I) (fun P => χ (Ideal.absNorm P)*(Ideal.absNorm P:ℂ)^(-s)),posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = ↑(moebius I) * (outsideMask S (primeProduct (primeSet I)) * ∏ Q ∈ primeSet I, χ ↑(absNorm ↑Q) * ↑(absNorm ↑Q) ^ (-s)) primeNormTerm_prod,posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = ↑(moebius I) * (outsideMask S (primeProduct (primeSet I)) * (χ ↑(absNorm (primeProduct (primeSet I))) * ↑(absNorm (primeProduct (primeSet I))) ^ (-s)))primeProduct_primeSet I hIposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = ↑(moebius I) * (outsideMask S I * (χ ↑(absNorm I) * ↑(absNorm I) ^ (-s)))]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ ordinarySeriesTerm χ S s I = ↑(moebius I) * (outsideMask S I * (χ ↑(absNorm I) * ↑(absNorm I) ^ (-s))) simp only [ordinarySeriesTerm,baseChangeWeight,CubicEisenstein.fullIdealWeight,ite_eq_right hI.ne_zero]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ outsideMask S I * (↑(moebius I) * χ ↑(absNorm I)) * ↑(absNorm I) ^ (-s) = ↑(moebius I) * (outsideMask S I * (χ ↑(absNorm I) * ↑(absNorm I) ^ (-s))) ringAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:¬Squarefree I⊢ ordinarySeriesTerm χ S s I = mobiusPrimeCoeff (ordinaryPrimeValue χ S s) I simp [ordinarySeriesTerm,baseChangeWeight,mobiusPrimeCoeff_nonsquarefree _ I hI, moebius_of_not_squarefree hI]All goals completed! 🐙lemma dampedSeriesTerm_eq {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : ∀P∈S,Prime P) (s : ℂ) (I : Ideal ActualEisensteinCubic.O) : dampedSeriesTerm χ S s I = mobiusPrimeCoeff (dampedPrimeValue χ S s) I := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.O⊢ dampedSeriesTerm χ S s I = mobiusPrimeCoeff (dampedPrimeValue χ S s) I by_cases hI : Squarefree Iposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = mobiusPrimeCoeff (dampedPrimeValue χ S s) Inegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:¬Squarefree I⊢ dampedSeriesTerm χ S s I = mobiusPrimeCoeff (dampedPrimeValue χ S s) I ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = mobiusPrimeCoeff (dampedPrimeValue χ S s) I rw [mobiusPrimeCoeff,posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * (primeValueHom (dampedPrimeValue χ S s)) IprimeValueHom_squarefree _ I hIposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * ∏ P ∈ primeSet I, dampedPrimeValue χ S s ↑P]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * ∏ P ∈ primeSet I, dampedPrimeValue χ S s ↑P simp only [dampedPrimeValue]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * ∏ P ∈ primeSet I, if ↑P ∈ S then 0 else (1 - 1 / ↑(absNorm ↑P)) * (χ ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-s)) rw [prod_cut_primes S hS (primeSet I) (fun P => (1-(1:ℂ)/(Ideal.absNorm P:ℂ))*(χ (Ideal.absNorm P)*(Ideal.absNorm P:ℂ)^(-s))),posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * (outsideMask S (primeProduct (primeSet I)) * ∏ Q ∈ primeSet I, (1 - 1 / ↑(absNorm ↑Q)) * (χ ↑(absNorm ↑Q) * ↑(absNorm ↑Q) ^ (-s))) Finset.prod_mul_distrib,posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * (outsideMask S (primeProduct (primeSet I)) * ((∏ x ∈ primeSet I, (1 - 1 / ↑(absNorm ↑x))) * ∏ x ∈ primeSet I, χ ↑(absNorm ↑x) * ↑(absNorm ↑x) ^ (-s)))primeNormTerm_prod,posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * (outsideMask S (primeProduct (primeSet I)) * ((∏ x ∈ primeSet I, (1 - 1 / ↑(absNorm ↑x))) * (χ ↑(absNorm (primeProduct (primeSet I))) * ↑(absNorm (primeProduct (primeSet I))) ^ (-s)))) prod_primeSet I (fun P => (1-(1:ℂ)/(Ideal.absNorm P:ℂ))),posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * (outsideMask S (primeProduct (primeSet I)) * ((∏ P ∈ primeSupport I, (1 - 1 / ↑(absNorm P))) * (χ ↑(absNorm (primeProduct (primeSet I))) * ↑(absNorm (primeProduct (primeSet I))) ^ (-s)))) primeProduct_primeSet I hIposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * (outsideMask S I * ((∏ P ∈ primeSupport I, (1 - 1 / ↑(absNorm P))) * (χ ↑(absNorm I) * ↑(absNorm I) ^ (-s))))]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ dampedSeriesTerm χ S s I = ↑(moebius I) * (outsideMask S I * ((∏ P ∈ primeSupport I, (1 - 1 / ↑(absNorm P))) * (χ ↑(absNorm I) * ↑(absNorm I) ^ (-s)))) simp only [dampedSeriesTerm,ordinarySeriesTerm,baseChangeWeight,SixthPowerAverage.totientDensity, CubicEisenstein.fullIdealWeight,ite_eq_right hI.ne_zero]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:Squarefree I⊢ outsideMask S I * (↑(moebius I) * χ ↑(absNorm I)) * ↑(absNorm I) ^ (-s) * ∏ P ∈ primeSupport I, (1 - 1 / ↑(absNorm P)) = ↑(moebius I) * (outsideMask S I * ((∏ P ∈ primeSupport I, (1 - 1 / ↑(absNorm P))) * (χ ↑(absNorm I) * ↑(absNorm I) ^ (-s)))) ringAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂI:Ideal ActualEisensteinCubic.OhI:¬Squarefree I⊢ dampedSeriesTerm χ S s I = mobiusPrimeCoeff (dampedPrimeValue χ S s) I simp [dampedSeriesTerm,ordinarySeriesTerm,baseChangeWeight,mobiusPrimeCoeff_nonsquarefree _ I hI, moebius_of_not_squarefree hI]All goals completed! 🐙endopen ActualEisensteinCubiclemma ordinaryPrimeValue_norm_le {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (P : PrimeIdeal) (s : ℂ) : ‖ordinaryPrimeValue χ S s P.val‖≤(Ideal.absNorm P.val:ℝ)^(-s.re) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂ⊢ ‖ordinaryPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re) by_cases hP : P.val∈Sposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∈ S⊢ ‖ordinaryPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re)negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∉ S⊢ ‖ordinaryPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re) ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∈ S⊢ ‖ordinaryPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re) simp only [ordinaryPrimeValue,ite_eq_left hP,norm_zero]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∈ S⊢ 0 ≤ ↑(absNorm ↑P) ^ (-s.re) positivityAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∉ S⊢ ‖ordinaryPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re) simpa only [ordinaryPrimeValue,ite_eq_right hP,primeCharacterTerm,primeNormPower] using primeCharacterTerm_norm_le χ P s s.re le_rflAll goals completed! 🐙lemma dampedPrimeValue_norm_le {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (P : PrimeIdeal) (s : ℂ) : ‖dampedPrimeValue χ S s P.val‖≤(Ideal.absNorm P.val:ℝ)^(-s.re) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂ⊢ ‖dampedPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re) by_cases hP : P.val∈Sposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∈ S⊢ ‖dampedPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re)negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∉ S⊢ ‖dampedPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re) ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∈ S⊢ ‖dampedPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re) simp only [dampedPrimeValue,ite_eq_left hP,norm_zero]posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∈ S⊢ 0 ≤ ↑(absNorm ↑P) ^ (-s.re) positivityAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∉ S⊢ ‖dampedPrimeValue χ S s ↑P‖ ≤ ↑(absNorm ↑P) ^ (-s.re) change ‖if P.val∈S then 0 else primeDensity P*primeCharacterTerm χ P s‖≤_negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∉ S⊢ ‖if ↑P ∈ S then 0 else primeDensity P * primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-s.re) rw [ite_eq_right hP,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∉ S⊢ ‖primeDensity P * primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-s.re)norm_mulnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∉ S⊢ ‖primeDensity P‖ * ‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-s.re)]negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∉ S⊢ ‖primeDensity P‖ * ‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-s.re) exact (mul_le_mul_of_nonneg_right (primeDensity_norm_le_one P) (norm_nonneg _)).trans (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhP:↑P ∉ S⊢ 1 * ‖primeCharacterTerm χ P s‖ ≤ ↑(absNorm ↑P) ^ (-s.re) simpa using primeCharacterTerm_norm_le χ P s s.re le_rflAll goals completed! 🐙)lemma prime_reciprocal_series_summable (s : ℂ) (hs : 1<s.re) : Summable (fun P : PrimeIdeal => (Ideal.absNorm P.val:ℝ)^(-s.re)) := bys:ℂhs:1 < s.re⊢ Summable fun P => ↑(absNorm ↑P) ^ (-s.re) have hh := prime_norm_series_summable (s.re-1) (bys:ℂhs:1 < s.re⊢ 0 < s.re - 1 linarithAll goals completed! 🐙)s:ℂhs:1 < s.rehh:Summable fun P => ↑(absNorm ↑P) ^ (-(1 + (s.re - 1)))⊢ Summable fun P => ↑(absNorm ↑P) ^ (-s.re) simpa only [show 1+(s.re-1)=s.re bys:ℂhs:1 < s.re⊢ Summable fun P => ↑(absNorm ↑P) ^ (-s.re) ringAll goals completed! 🐙] using hhlemma ordinaryPrimeValue_summable {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (hs : 1<s.re) : Summable (fun P : PrimeIdeal => ‖ordinaryPrimeValue χ S s P.val‖) := Summable.of_nonneg_of_le (fun _ => norm_nonneg _) (fun P => ordinaryPrimeValue_norm_le χ S P s) (prime_reciprocal_series_summable s hs)lemma dampedPrimeValue_summable {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (hs : 1<s.re) : Summable (fun P : PrimeIdeal => ‖dampedPrimeValue χ S s P.val‖) := Summable.of_nonneg_of_le (fun _ => norm_nonneg _) (fun P => dampedPrimeValue_norm_le χ S P s) (prime_reciprocal_series_summable s hs)lemma ordinarySeries_euler {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : ∀P∈S,Prime P) (s : ℂ) (hs : 1<s.re) : (∑'I : Ideal ActualEisensteinCubic.O,ordinarySeriesTerm χ S s I)= ∏'P : PrimeIdeal,(1-ordinaryPrimeValue χ S s P.val) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) simp_rw [q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P)ordinarySeriesTerm_eq χ S hSq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), mobiusPrimeCoeff (ordinaryPrimeValue χ S s) I = ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P)] exact mobiusPrimeCoeff_euler _ (ordinaryPrimeValue_summable χ S s hs)All goals completed! 🐙lemma dampedSeries_euler {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : ∀P∈S,Prime P) (s : ℂ) (hs : 1<s.re) : (∑'I : Ideal ActualEisensteinCubic.O,dampedSeriesTerm χ S s I)= ∏'P : PrimeIdeal,(1-dampedPrimeValue χ S s P.val) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s I = ∏' (P : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑P) simp_rw [q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s I = ∏' (P : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑P)dampedSeriesTerm_eq χ S hSq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), mobiusPrimeCoeff (dampedPrimeValue χ S s) I = ∏' (P : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑P)] exact mobiusPrimeCoeff_euler _ (dampedPrimeValue_summable χ S s hs)All goals completed! 🐙lemma local_correction_identity {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (P : PrimeIdeal) (s : ℂ) (hs : 0<s.re) : (1-dampedPrimeValue χ S s P.val)*(1+correctionTerm χ S P s)= 1-ordinaryPrimeValue χ S s P.val := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.re⊢ (1 - dampedPrimeValue χ S s ↑P) * (1 + correctionTerm χ S P s) = 1 - ordinaryPrimeValue χ S s ↑P rw [correctionTerm_factor χ S P s hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.re⊢ ((1 - dampedPrimeValue χ S s ↑P) * if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) = 1 - ordinaryPrimeValue χ S s ↑P]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.re⊢ ((1 - dampedPrimeValue χ S s ↑P) * if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) = 1 - ordinaryPrimeValue χ S s ↑P by_cases hP : P.val∈Sposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∈ S⊢ ((1 - dampedPrimeValue χ S s ↑P) * if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) = 1 - ordinaryPrimeValue χ S s ↑Pnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ S⊢ ((1 - dampedPrimeValue χ S s ↑P) * if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) = 1 - ordinaryPrimeValue χ S s ↑P ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∈ S⊢ ((1 - dampedPrimeValue χ S s ↑P) * if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) = 1 - ordinaryPrimeValue χ S s ↑P simp [dampedPrimeValue,ordinaryPrimeValue,hP]All goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ S⊢ ((1 - dampedPrimeValue χ S s ↑P) * if ↑P ∈ S then 1 else (1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) = 1 - ordinaryPrimeValue χ S s ↑P simp only [dampedPrimeValue,ordinaryPrimeValue,ite_eq_right hP]negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ S⊢ (1 - (1 - 1 / ↑(absNorm ↑P)) * (χ ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-s))) * ((1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) = 1 - χ ↑(absNorm ↑P) * ↑(absNorm ↑P) ^ (-s) change (1-primeDensity P*primeCharacterTerm χ P s)* ((1-primeCharacterTerm χ P s)/(1-primeDensity P*primeCharacterTerm χ P s))= 1-primeCharacterTerm χ P snegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)P:PrimeIdeals:ℂhs:0 < s.rehP:↑P ∉ S⊢ (1 - primeDensity P * primeCharacterTerm χ P s) * ((1 - primeCharacterTerm χ P s) / (1 - primeDensity P * primeCharacterTerm χ P s)) = 1 - primeCharacterTerm χ P s exact mul_div_cancel₀ _ (correctionDenominator_ne_zero χ P s hs)All goals completed! 🐙theorem actual_dirichlet_correction {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : ∀P∈S,Prime P) (s : ℂ) (hs : 1<s.re) : (∑'I : Ideal ActualEisensteinCubic.O,ordinarySeriesTerm χ S s I)= eulerCorrection χ S s*(∑'I : Ideal ActualEisensteinCubic.O,dampedSeriesTerm χ S s I) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = eulerCorrection χ S s * ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s I rw [ordinarySeries_euler χ S hS s hs,q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) = eulerCorrection χ S s * ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s IdampedSeries_euler χ S hS s hs,q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) = eulerCorrection χ S s * ∏' (P : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑P)mul_commq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) = (∏' (P : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑P)) * eulerCorrection χ S s]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) = (∏' (P : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑P)) * eulerCorrection χ S s have hd : Multipliable (fun P : PrimeIdeal => 1-dampedPrimeValue χ S s P.val) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = eulerCorrection χ S s * ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s I simpa only [sub_eq_add_neg] using multipliable_one_add_of_summable (show Summable (fun P : PrimeIdeal => ‖-dampedPrimeValue χ S s P.val‖) byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = eulerCorrection χ S s * ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s I simpa only [norm_neg] using dampedPrimeValue_summable χ S s hsAll goals completed! 🐙)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.rehd:Multipliable fun P => 1 - dampedPrimeValue χ S s ↑P⊢ ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) = (∏' (P : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑P)) * eulerCorrection χ S s have hc := multipliable_one_add_of_summable (correctionTerm_summable χ S s (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.rehd:Multipliable fun P => 1 - dampedPrimeValue χ S s ↑P⊢ 0 < s.re linarithAll goals completed! 🐙))q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.rehd:Multipliable fun P => 1 - dampedPrimeValue χ S s ↑Phc:Multipliable fun i => 1 + correctionTerm χ S i s⊢ ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) = (∏' (P : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑P)) * eulerCorrection χ S s change _ = (∏' P : PrimeIdeal, (1-dampedPrimeValue χ S s P.val))*(∏' P : PrimeIdeal, (1+correctionTerm χ S P s))q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.rehd:Multipliable fun P => 1 - dampedPrimeValue χ S s ↑Phc:Multipliable fun i => 1 + correctionTerm χ S i s⊢ ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) = (∏' (P : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑P)) * ∏' (P : PrimeIdeal), (1 + correctionTerm χ S P s) rw [←hd.tprod_mul hcq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.rehd:Multipliable fun P => 1 - dampedPrimeValue χ S s ↑Phc:Multipliable fun i => 1 + correctionTerm χ S i s⊢ ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) = ∏' (b : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑b) * (1 + correctionTerm χ S b s)]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.rehd:Multipliable fun P => 1 - dampedPrimeValue χ S s ↑Phc:Multipliable fun i => 1 + correctionTerm χ S i s⊢ ∏' (P : PrimeIdeal), (1 - ordinaryPrimeValue χ S s ↑P) = ∏' (b : PrimeIdeal), (1 - dampedPrimeValue χ S s ↑b) * (1 + correctionTerm χ S b s) apply tprod_congrq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.rehd:Multipliable fun P => 1 - dampedPrimeValue χ S s ↑Phc:Multipliable fun i => 1 + correctionTerm χ S i s⊢ ∀ (b : PrimeIdeal), 1 - ordinaryPrimeValue χ S s ↑b = (1 - dampedPrimeValue χ S s ↑b) * (1 + correctionTerm χ S b s) intro Pq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.rehd:Multipliable fun P => 1 - dampedPrimeValue χ S s ↑Phc:Multipliable fun i => 1 + correctionTerm χ S i sP:PrimeIdeal⊢ 1 - ordinaryPrimeValue χ S s ↑P = (1 - dampedPrimeValue χ S s ↑P) * (1 + correctionTerm χ S P s) exact (local_correction_identity χ S P s (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.rehd:Multipliable fun P => 1 - dampedPrimeValue χ S s ↑Phc:Multipliable fun i => 1 + correctionTerm χ S i sP:PrimeIdeal⊢ 0 < s.re linarithAll goals completed! 🐙)).symmopen scoped BigOperators Classicalopen ActualEisensteinCubicopen ShortDraftHeckeBridge hiding Olemma normFiber_tsum (a : Ideal ActualEisensteinCubic.O→ℂ) (n : ℕ) : (∑'I : {I : Ideal ActualEisensteinCubic.O // Ideal.absNorm I=n},a I.val)=normFiberCoeff a n := bya:Ideal ActualEisensteinCubic.O → ℂn:ℕ⊢ ∑' (I : { I // absNorm I = n }), a ↑I = normFiberCoeff a n let : Fintype {I : Ideal ActualEisensteinCubic.O // Ideal.absNorm I=n} := (Ideal.finite_setOfPred_absNorm_eq (S := ActualEisensteinCubic.O) n).fintypea:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∑' (I : { I // absNorm I = n }), a ↑I = normFiberCoeff a n rw [tsum_fintypea:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∑ b, a ↑b = normFiberCoeff a n]a:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∑ b, a ↑b = normFiberCoeff a n symma:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ normFiberCoeff a n = ∑ b, a ↑b change (∑I∈FiniteSFactor.fiber n,a I)=_a:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∑ I ∈ FiniteSFactor.fiber n, a I = ∑ b, a ↑b apply Finset.sum_bij (fun I hI => (⟨I,FiniteSFactor.mem_fiber.mp hI⟩ : {I : Ideal ActualEisensteinCubic.O // Ideal.absNorm I=n}))hia:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∀ (a : Ideal ActualEisensteinCubic.O) (ha : a ∈ FiniteSFactor.fiber n), ⟨a, ⋯⟩ ∈ Finset.univi_inja:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∀ (a₁ : Ideal ActualEisensteinCubic.O) (ha₁ : a₁ ∈ FiniteSFactor.fiber n) (a₂ : Ideal ActualEisensteinCubic.O) (ha₂ : a₂ ∈ FiniteSFactor.fiber n), ⟨a₁, ⋯⟩ = ⟨a₂, ⋯⟩ → a₁ = a₂i_surja:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∀ b ∈ Finset.univ, ∃ a, ∃ (ha : a ∈ FiniteSFactor.fiber n), ⟨a, ⋯⟩ = bha:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∀ (a_1 : Ideal ActualEisensteinCubic.O) (ha : a_1 ∈ FiniteSFactor.fiber n), a a_1 = a ↑⟨a_1, ⋯⟩ ·hia:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∀ (a : Ideal ActualEisensteinCubic.O) (ha : a ∈ FiniteSFactor.fiber n), ⟨a, ⋯⟩ ∈ Finset.univ intro I hIhia:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintypeI:Ideal ActualEisensteinCubic.OhI:I ∈ FiniteSFactor.fiber n⊢ ⟨I, ⋯⟩ ∈ Finset.univ exact Finset.mem_univ _All goals completed! 🐙 ·i_inja:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∀ (a₁ : Ideal ActualEisensteinCubic.O) (ha₁ : a₁ ∈ FiniteSFactor.fiber n) (a₂ : Ideal ActualEisensteinCubic.O) (ha₂ : a₂ ∈ FiniteSFactor.fiber n), ⟨a₁, ⋯⟩ = ⟨a₂, ⋯⟩ → a₁ = a₂ intro I hI J hJ hei_inja:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintypeI:Ideal ActualEisensteinCubic.OhI:I ∈ FiniteSFactor.fiber nJ:Ideal ActualEisensteinCubic.OhJ:J ∈ FiniteSFactor.fiber nhe:⟨I, ⋯⟩ = ⟨J, ⋯⟩⊢ I = J exact congrArg Subtype.val heAll goals completed! 🐙 ·i_surja:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∀ b ∈ Finset.univ, ∃ a, ∃ (ha : a ∈ FiniteSFactor.fiber n), ⟨a, ⋯⟩ = b intro I hIi_surja:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintypeI:{ I // absNorm I = n }hI:I ∈ Finset.univ⊢ ∃ a, ∃ (ha : a ∈ FiniteSFactor.fiber n), ⟨a, ⋯⟩ = I exact ⟨I.val,FiniteSFactor.mem_fiber.mpr I.property,rfl⟩All goals completed! 🐙 ·ha:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintype⊢ ∀ (a_1 : Ideal ActualEisensteinCubic.O) (ha : a_1 ∈ FiniteSFactor.fiber n), a a_1 = a ↑⟨a_1, ⋯⟩ intro I hIha:Ideal ActualEisensteinCubic.O → ℂn:ℕthis:Fintype { I // absNorm I = n } := ⋯.fintypeI:Ideal ActualEisensteinCubic.OhI:I ∈ FiniteSFactor.fiber n⊢ a I = a ↑⟨I, ⋯⟩ rflAll goals completed! 🐙lemma idealDirichlet_fiber (a : Ideal ActualEisensteinCubic.O→ℂ) (s : ℂ) (n : ℕ) : (∑'I : {I : Ideal ActualEisensteinCubic.O // Ideal.absNorm I=n},a I.val*CubicEisenstein.fullIdealWeight s I.val)= LSeries.term (normFiberCoeff a) s n := bya:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕ⊢ ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s n by_cases hn : n=0posa:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:n = 0⊢ ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s nnega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0⊢ ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s n ·posa:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:n = 0⊢ ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s n subst nposa:Ideal ActualEisensteinCubic.O → ℂs:ℂ⊢ ∑' (I : { I // absNorm I = 0 }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s 0 have hz (I : {I : Ideal ActualEisensteinCubic.O // Ideal.absNorm I=0}) : CubicEisenstein.fullIdealWeight s I.val=0 := bya:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕ⊢ ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s n have hI : I.val=0 := Ideal.absNorm_eq_zero_iff.mp I.propertya:Ideal ActualEisensteinCubic.O → ℂs:ℂI:{ I // absNorm I = 0 }hI:↑I = 0⊢ CubicEisenstein.fullIdealWeight s ↑I = 0 simp [CubicEisenstein.fullIdealWeight,hI]posa:Ideal ActualEisensteinCubic.O → ℂs:ℂhz:∀ (I : { I // absNorm I = 0 }), CubicEisenstein.fullIdealWeight s ↑I = 0⊢ ∑' (I : { I // absNorm I = 0 }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s 0 simp only [hz,mul_zero,tsum_zero,LSeries.term_zero]All goals completed! 🐙 ·nega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0⊢ ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s n have ht (I : {I : Ideal ActualEisensteinCubic.O // Ideal.absNorm I=n}) : CubicEisenstein.fullIdealWeight s I.val=(n:ℂ)^(-s) := by have hI : I.val≠0 := fun h => hn (bya:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0I:{ I // absNorm I = n }h:↑I = 0⊢ n = 0 rw [←I.property,a:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0I:{ I // absNorm I = n }h:↑I = 0⊢ absNorm ↑I = 0h,a:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0I:{ I // absNorm I = n }h:↑I = 0⊢ absNorm 0 = 0map_zeroa:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0I:{ I // absNorm I = n }h:↑I = 0⊢ 0 = 0]All goals completed! 🐙)a:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0I:{ I // absNorm I = n }hI:↑I ≠ 0⊢ CubicEisenstein.fullIdealWeight s ↑I = ↑n ^ (-s) rw [CubicEisenstein.fullIdealWeight,a:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0I:{ I // absNorm I = n }hI:↑I ≠ 0⊢ (if ↑I = 0 then 0 else ↑(absNorm ↑I) ^ (-s)) = ↑n ^ (-s)ite_eq_right hI,a:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0I:{ I // absNorm I = n }hI:↑I ≠ 0⊢ ↑(absNorm ↑I) ^ (-s) = ↑n ^ (-s)I.propertya:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0I:{ I // absNorm I = n }hI:↑I ≠ 0⊢ ↑n ^ (-s) = ↑n ^ (-s)]nega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0ht:∀ (I : { I // absNorm I = n }), CubicEisenstein.fullIdealWeight s ↑I = ↑n ^ (-s)⊢ ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s n simp_rw [nega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0ht:∀ (I : { I // absNorm I = n }), CubicEisenstein.fullIdealWeight s ↑I = ↑n ^ (-s)⊢ ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I = LSeries.term (normFiberCoeff a) s nhtnega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0ht:∀ (I : { I // absNorm I = n }), CubicEisenstein.fullIdealWeight s ↑I = ↑n ^ (-s)⊢ ∑' (I : { I // absNorm I = n }), a ↑I * ↑n ^ (-s) = LSeries.term (normFiberCoeff a) s n] rw [tsum_mul_right,nega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0ht:∀ (I : { I // absNorm I = n }), CubicEisenstein.fullIdealWeight s ↑I = ↑n ^ (-s)⊢ (∑' (x : { I // absNorm I = n }), a ↑x) * ↑n ^ (-s) = LSeries.term (normFiberCoeff a) s nnormFiber_tsum,nega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0ht:∀ (I : { I // absNorm I = n }), CubicEisenstein.fullIdealWeight s ↑I = ↑n ^ (-s)⊢ normFiberCoeff a n * ↑n ^ (-s) = LSeries.term (normFiberCoeff a) s nLSeries.term_of_ne_zero hn,nega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0ht:∀ (I : { I // absNorm I = n }), CubicEisenstein.fullIdealWeight s ↑I = ↑n ^ (-s)⊢ normFiberCoeff a n * ↑n ^ (-s) = normFiberCoeff a n / ↑n ^ sComplex.cpow_neg,nega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0ht:∀ (I : { I // absNorm I = n }), CubicEisenstein.fullIdealWeight s ↑I = ↑n ^ (-s)⊢ normFiberCoeff a n * (↑n ^ s)⁻¹ = normFiberCoeff a n / ↑n ^ sdiv_eq_mul_invnega:Ideal ActualEisensteinCubic.O → ℂs:ℂn:ℕhn:¬n = 0ht:∀ (I : { I // absNorm I = n }), CubicEisenstein.fullIdealWeight s ↑I = ↑n ^ (-s)⊢ normFiberCoeff a n * (↑n ^ s)⁻¹ = normFiberCoeff a n * (↑n ^ s)⁻¹]All goals completed! 🐙lemma idealDirichlet_summable (a : Ideal ActualEisensteinCubic.O→ℂ) (ha : ∀I,‖a I‖≤1) (s : ℂ) (hs : 1<s.re) : Summable (fun I : Ideal ActualEisensteinCubic.O => a I*CubicEisenstein.fullIdealWeight s I) := bya:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.re⊢ Summable fun I => a I * CubicEisenstein.fullIdealWeight s I apply Summable.of_norma:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.re⊢ Summable fun a_1 => ‖a a_1 * CubicEisenstein.fullIdealWeight s a_1‖ apply Summable.of_nonneg_of_le (fun _ => norm_nonneg _) (fun I => ?_) (CubicEisenstein.fullIdealWeight_summable_norm s hs)a:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.reI:Ideal CubicEisenstein.O⊢ ‖a I * CubicEisenstein.fullIdealWeight s I‖ ≤ ‖CubicEisenstein.fullIdealWeight s I‖ rw [norm_mula:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.reI:Ideal CubicEisenstein.O⊢ ‖a I‖ * ‖CubicEisenstein.fullIdealWeight s I‖ ≤ ‖CubicEisenstein.fullIdealWeight s I‖]a:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.reI:Ideal CubicEisenstein.O⊢ ‖a I‖ * ‖CubicEisenstein.fullIdealWeight s I‖ ≤ ‖CubicEisenstein.fullIdealWeight s I‖ exact mul_le_of_le_one_left (norm_nonneg _) (ha I)All goals completed! 🐙theorem idealDirichlet_eq_LSeries (a : Ideal ActualEisensteinCubic.O→ℂ) (ha : ∀I,‖a I‖≤1) (s : ℂ) (hs : 1<s.re) : (∑'I : Ideal ActualEisensteinCubic.O,a I*CubicEisenstein.fullIdealWeight s I)=LSeries (normFiberCoeff a) s := bya:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), a I * CubicEisenstein.fullIdealWeight s I = L (normFiberCoeff a) s have hh := (idealDirichlet_summable a ha s hs).hasSum.tsum_fiberwise Ideal.absNorma:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.rehh:HasSum (fun c => ∑' (b : ↑(⇑absNorm ⁻¹' {c})), a ↑b * CubicEisenstein.fullIdealWeight s ↑b) (∑' (b : Ideal ActualEisensteinCubic.O), a b * CubicEisenstein.fullIdealWeight s b)⊢ ∑' (I : Ideal ActualEisensteinCubic.O), a I * CubicEisenstein.fullIdealWeight s I = L (normFiberCoeff a) s change HasSum (fun n : ℕ => ∑'I : {I : Ideal ActualEisensteinCubic.O // Ideal.absNorm I=n}, a I.val*CubicEisenstein.fullIdealWeight s I.val) _ at hha:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.rehh:HasSum (fun n => ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I) (∑' (b : Ideal ActualEisensteinCubic.O), a b * CubicEisenstein.fullIdealWeight s b)⊢ ∑' (I : Ideal ActualEisensteinCubic.O), a I * CubicEisenstein.fullIdealWeight s I = L (normFiberCoeff a) s simp_rw [a:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.rehh:HasSum (fun n => ∑' (I : { I // absNorm I = n }), a ↑I * CubicEisenstein.fullIdealWeight s ↑I) (∑' (b : Ideal ActualEisensteinCubic.O), a b * CubicEisenstein.fullIdealWeight s b)⊢ ∑' (I : Ideal ActualEisensteinCubic.O), a I * CubicEisenstein.fullIdealWeight s I = L (normFiberCoeff a) sidealDirichlet_fibera:Ideal ActualEisensteinCubic.O → ℂha:∀ (I : Ideal ActualEisensteinCubic.O), ‖a I‖ ≤ 1s:ℂhs:1 < s.rehh:HasSum (fun n => LSeries.term (normFiberCoeff a) s n) (∑' (b : Ideal ActualEisensteinCubic.O), a b * CubicEisenstein.fullIdealWeight s b)⊢ ∑' (I : Ideal ActualEisensteinCubic.O), a I * CubicEisenstein.fullIdealWeight s I = L (normFiberCoeff a) s] at hh exact hh.tsum_eq.symmAll goals completed! 🐙lemma ordinarySeriesTerm_outside {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (I : Ideal ActualEisensteinCubic.O) : ordinarySeriesTerm χ S s I= FiniteSFactor.outsideWeight S (baseChangeWeight χ) I*CubicEisenstein.fullIdealWeight s I := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.O⊢ ordinarySeriesTerm χ S s I = FiniteSFactor.outsideWeight S (baseChangeWeight χ) I * CubicEisenstein.fullIdealWeight s I unfold ordinarySeriesTerm outsideMask FiniteSFactor.outsideWeightq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.O⊢ (if ∀ P ∈ S, ¬P ∣ I then 1 else 0) * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I = (if ∀ P ∈ S, ¬P ∣ I then baseChangeWeight χ I else 0) * CubicEisenstein.fullIdealWeight s I split_ifsposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.Oh✝:∀ P ∈ S, ¬P ∣ I⊢ 1 * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I = baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s Inegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.Oh✝:¬∀ P ∈ S, ¬P ∣ I⊢ 0 * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I = 0 * CubicEisenstein.fullIdealWeight s I <;>posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.Oh✝:∀ P ∈ S, ¬P ∣ I⊢ 1 * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I = baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s Inegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.Oh✝:¬∀ P ∈ S, ¬P ∣ I⊢ 0 * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I = 0 * CubicEisenstein.fullIdealWeight s I simpAll goals completed! 🐙lemma dampedSeriesTerm_outside {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (I : Ideal ActualEisensteinCubic.O) : dampedSeriesTerm χ S s I= SixthPowerAverage.outsideWeight χ S I*CubicEisenstein.fullIdealWeight s I := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.O⊢ dampedSeriesTerm χ S s I = SixthPowerAverage.outsideWeight χ S I * CubicEisenstein.fullIdealWeight s I unfold dampedSeriesTerm ordinarySeriesTerm outsideMask SixthPowerAverage.outsideWeight FiniteSFactor.outsideWeight SixthPowerAverage.weightedMoebiusq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.O⊢ (if ∀ P ∈ S, ¬P ∣ I then 1 else 0) * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I * SixthPowerAverage.totientDensity I = (if ∀ P ∈ S, ¬P ∣ I then baseChangeWeight χ I * SixthPowerAverage.totientDensity I else 0) * CubicEisenstein.fullIdealWeight s I split_ifsposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.Oh✝:∀ P ∈ S, ¬P ∣ I⊢ 1 * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I * SixthPowerAverage.totientDensity I = baseChangeWeight χ I * SixthPowerAverage.totientDensity I * CubicEisenstein.fullIdealWeight s Inegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.Oh✝:¬∀ P ∈ S, ¬P ∣ I⊢ 0 * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I * SixthPowerAverage.totientDensity I = 0 * CubicEisenstein.fullIdealWeight s I <;>posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.Oh✝:∀ P ∈ S, ¬P ∣ I⊢ 1 * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I * SixthPowerAverage.totientDensity I = baseChangeWeight χ I * SixthPowerAverage.totientDensity I * CubicEisenstein.fullIdealWeight s Inegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂI:Ideal ActualEisensteinCubic.Oh✝:¬∀ P ∈ S, ¬P ∣ I⊢ 0 * baseChangeWeight χ I * CubicEisenstein.fullIdealWeight s I * SixthPowerAverage.totientDensity I = 0 * CubicEisenstein.fullIdealWeight s I ringAll goals completed! 🐙lemma ordinarySeries_eq_LSeries {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (hs : 1<s.re) : (∑'I : Ideal ActualEisensteinCubic.O,ordinarySeriesTerm χ S s I)= LSeries (FiniteSFactor.outsideCoeff S (baseChangeWeight χ)) s := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = L (FiniteSFactor.outsideCoeff S (baseChangeWeight χ)) s simp_rw [q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = L (FiniteSFactor.outsideCoeff S (baseChangeWeight χ)) sordinarySeriesTerm_outsideq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), FiniteSFactor.outsideWeight S (baseChangeWeight χ) I * CubicEisenstein.fullIdealWeight s I = L (FiniteSFactor.outsideCoeff S (baseChangeWeight χ)) s] apply idealDirichlet_eq_LSerieshaq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ ∀ (I : Ideal ActualEisensteinCubic.O), ‖FiniteSFactor.outsideWeight S (baseChangeWeight χ) I‖ ≤ 1hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ 1 < s.re intro Ihaq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.reI:Ideal ActualEisensteinCubic.O⊢ ‖FiniteSFactor.outsideWeight S (baseChangeWeight χ) I‖ ≤ 1hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ 1 < s.re unfold FiniteSFactor.outsideWeighthaq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.reI:Ideal ActualEisensteinCubic.O⊢ ‖if ∀ P ∈ S, ¬P ∣ I then baseChangeWeight χ I else 0‖ ≤ 1hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ 1 < s.re split_ifsposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.reI:Ideal ActualEisensteinCubic.Oh✝:∀ P ∈ S, ¬P ∣ I⊢ ‖baseChangeWeight χ I‖ ≤ 1negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.reI:Ideal ActualEisensteinCubic.Oh✝:¬∀ P ∈ S, ¬P ∣ I⊢ ‖0‖ ≤ 1hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ 1 < s.re ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.reI:Ideal ActualEisensteinCubic.Oh✝:∀ P ∈ S, ¬P ∣ I⊢ ‖baseChangeWeight χ I‖ ≤ 1 exact ConcretePrimeRowBridge.baseChangeWeight_norm_le_one χ IAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.reI:Ideal ActualEisensteinCubic.Oh✝:¬∀ P ∈ S, ¬P ∣ I⊢ ‖0‖ ≤ 1 simpAll goals completed! 🐙 exact hsAll goals completed! 🐙lemma dampedSeries_eq_LSeries {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (hs : 1<s.re) : (∑'I : Ideal ActualEisensteinCubic.O,dampedSeriesTerm χ S s I)= LSeries (SixthPowerAverage.weightedCoeff χ S) s := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s I = L (SixthPowerAverage.weightedCoeff χ S) s simp_rw [q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s I = L (SixthPowerAverage.weightedCoeff χ S) sdampedSeriesTerm_outsideq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), SixthPowerAverage.outsideWeight χ S I * CubicEisenstein.fullIdealWeight s I = L (SixthPowerAverage.weightedCoeff χ S) s] exact idealDirichlet_eq_LSeries _ (SixthPowerAverage.outsideWeight_norm_le_one χ S) s hsAll goals completed! 🐙theorem actual_LSeries_correction {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : ∀P∈S,Prime P) (s : ℂ) (hs : 1<s.re) : LSeries (FiniteSFactor.outsideCoeff S (baseChangeWeight χ)) s= eulerCorrection χ S s*LSeries (SixthPowerAverage.weightedCoeff χ S) s := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ L (FiniteSFactor.outsideCoeff S (baseChangeWeight χ)) s = eulerCorrection χ S s * L (SixthPowerAverage.weightedCoeff χ S) s rw [←ordinarySeries_eq_LSeries χ S s hs,q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = eulerCorrection χ S s * L (SixthPowerAverage.weightedCoeff χ S) s←dampedSeries_eq_LSeries χ S s hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = eulerCorrection χ S s * ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s I]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:1 < s.re⊢ ∑' (I : Ideal ActualEisensteinCubic.O), ordinarySeriesTerm χ S s I = eulerCorrection χ S s * ∑' (I : Ideal ActualEisensteinCubic.O), dampedSeriesTerm χ S s I exact actual_dirichlet_correction χ S hS s hsAll goals completed! 🐙theorem full_LSeries_correction {q : ℕ} [NeZero q] (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : ∀P∈S,Prime P) (s : ℂ) (hs : 2<s.re) : LSeries (normFiberCoeff (baseChangeWeight χ)) s= (CompactMellinBridge.finiteEulerFactor χ S s*eulerCorrection χ S s)* LSeries (SixthPowerAverage.weightedCoeff χ S) s := byq:ℕinst✝:NeZero qχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:2 < s.re⊢ L (normFiberCoeff (baseChangeWeight χ)) s = CompactMellinBridge.finiteEulerFactor χ S s * eulerCorrection χ S s * L (SixthPowerAverage.weightedCoeff χ S) s rw [FiniteSFactor.normFiberLSeries_finiteEuler_baseChange χ S hS s hs,q:ℕinst✝:NeZero qχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:2 < s.re⊢ (∏ P ∈ S, (1 - χ ↑(absNorm P) * ↑(absNorm P) ^ (-s))) * L (FiniteSFactor.outsideCoeff S (baseChangeWeight χ)) s = CompactMellinBridge.finiteEulerFactor χ S s * eulerCorrection χ S s * L (SixthPowerAverage.weightedCoeff χ S) s actual_LSeries_correction χ S hS s (byq:ℕinst✝:NeZero qχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:2 < s.re⊢ 1 < s.re linarithAll goals completed! 🐙)]q:ℕinst✝:NeZero qχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)hS:∀ P ∈ S, Prime Ps:ℂhs:2 < s.re⊢ (∏ P ∈ S, (1 - χ ↑(absNorm P) * ↑(absNorm P) ^ (-s))) * (eulerCorrection χ S s * L (SixthPowerAverage.weightedCoeff χ S) s) = CompactMellinBridge.finiteEulerFactor χ S s * eulerCorrection χ S s * L (SixthPowerAverage.weightedCoeff χ S) s exact (mul_assoc _ _ _).symmAll goals completed! 🐙theorem eulerCorrection_analytic {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) : AnalyticOnNhd ℂ (eulerCorrection χ S) {s : ℂ | 0<s.re} := (Complex.analyticOnNhd_iff_differentiableOn (Complex.isOpen_re_gt 0)).mpr (eulerCorrection_differentiableOn χ S)end SmoothMobiusCorrectionendend OAI