import OAI.NumberTheory.DirichletL.MeanSquare.ThetaDensitynamespace OAInoncomputable sectionnamespace SixthPowerAverageopen 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 Classicalsectionopen scoped BigOperators Classical SchwartzMap ContDiffopen MeasureTheory Metricopen EisensteinSchwartzPoissontheorem exists_averaging_test : ∃V : 𝓢(ℝ,ℂ), (∀x,‖V x‖≤1) ∧ (Function.support (V:ℝ→ℂ)⊆Set.Icc ((1:ℝ)/2) 1) ∧ V 0=0 ∧ paperRadialFourier V 0≠0 := by⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 let f : ContDiffBump ((3:ℝ)/4) := ⟨1/8,1/4,by⊢ 0 < 1 / 8 norm_numAll goals completed! 🐙,by⊢ 1 / 8 < 1 / 4 norm_numAll goals completed! 🐙⟩f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 let g : ℝ→ℂ := fun x=>(f x:ℂ)f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 have hgs : ContDiff ℝ ∞ g := Complex.ofRealCLM.contDiff.comp f.contDifff:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ g⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 have hsupport : Function.support g⊆Set.Icc ((1:ℝ)/2) 1 := by intro x hxf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ gx:ℝhx:x ∈ Function.support g⊢ x ∈ Set.Icc (1 / 2) 1 have hf : f x≠0 := by⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 simpa only [g,Function.mem_support,ne_eq,Complex.ofReal_eq_zero] using hxf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ gx:ℝhx:x ∈ Function.support ghf:↑f x ≠ 0⊢ x ∈ Set.Icc (1 / 2) 1 have hh : |x-(3:ℝ)/4|<1/4 := by⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 have hi : x∈Function.support (f:ℝ→ℝ) := hff:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ gx:ℝhx:x ∈ Function.support ghf:↑f x ≠ 0hi:x ∈ Function.support ↑f⊢ |x - 3 / 4| < 1 / 4 rw [f.support_eqf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ gx:ℝhx:x ∈ Function.support ghf:↑f x ≠ 0hi:x ∈ ball (3 / 4) f.rOut⊢ |x - 3 / 4| < 1 / 4] at hif:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ gx:ℝhx:x ∈ Function.support ghf:↑f x ≠ 0hi:x ∈ ball (3 / 4) f.rOut⊢ |x - 3 / 4| < 1 / 4 simpa only [Metric.mem_ball,Real.dist_eq,f] using hif:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ gx:ℝhx:x ∈ Function.support ghf:↑f x ≠ 0hh:|x - 3 / 4| < 1 / 4⊢ x ∈ Set.Icc (1 / 2) 1 exact ⟨byf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ gx:ℝhx:x ∈ Function.support ghf:↑f x ≠ 0hh:|x - 3 / 4| < 1 / 4⊢ 1 / 2 ≤ x linarith [(abs_lt.mp hh).1]All goals completed! 🐙,byf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ gx:ℝhx:x ∈ Function.support ghf:↑f x ≠ 0hh:|x - 3 / 4| < 1 / 4⊢ x ≤ 1 linarith [(abs_lt.mp hh).2]All goals completed! 🐙⟩f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 have hgc : HasCompactSupport g := HasCompactSupport.of_support_subset_isCompact isCompact_Icc hsupportf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport g⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 let V : 𝓢(ℝ,ℂ) := hgc.toSchwartzMap hgsf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgs⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 have hz : V 0=0 := by by_contra hf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgsh:¬V 0 = 0⊢ False have hh := (hsupport h).1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgsh:¬V 0 = 0hh:1 / 2 ≤ 0⊢ False norm_num at hhf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 refine ⟨V,?_,hsupport,hz,?_⟩refine_1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0⊢ ∀ (x : ℝ), ‖V x‖ ≤ 1refine_2f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0⊢ paperRadialFourier (⇑V) 0 ≠ 0 ·refine_1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0⊢ ∀ (x : ℝ), ‖V x‖ ≤ 1 intro xrefine_1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝ⊢ ‖V x‖ ≤ 1 change ‖(f x:ℂ)‖≤1refine_1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝ⊢ ‖↑(↑f x)‖ ≤ 1 rw [Complex.norm_real,refine_1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝ⊢ ‖↑f x‖ ≤ 1Real.norm_eq_abs,refine_1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝ⊢ |↑f x| ≤ 1abs_of_nonneg f.nonnegrefine_1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝ⊢ ↑f x ≤ 1]refine_1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝ⊢ ↑f x ≤ 1 exact f.le_oneAll goals completed! 🐙 ·refine_2f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0⊢ paperRadialFourier (⇑V) 0 ≠ 0 rw [paperRadialFourier_zero_eq_halflinerefine_2f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0⊢ 2 * ↑π / ↑√3 * ∫ (t : ℝ) in Set.Ioi 0, V t ≠ 0]refine_2f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0⊢ 2 * ↑π / ↑√3 * ∫ (t : ℝ) in Set.Ioi 0, V t ≠ 0 have he : (∫x : ℝ in Set.Ioi 0,(V x))=∫x : ℝ,(f x:ℂ) := by⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 apply setIntegral_eq_integral_of_forall_compl_eq_zerof:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0⊢ ∀ x ∉ Set.Ioi 0, V x = 0 intro x hxf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝhx:x ∉ Set.Ioi 0⊢ V x = 0 by_contra hnf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝhx:x ∉ Set.Ioi 0hn:¬V x = 0⊢ False have hp := (hsupport hn).1f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝhx:x ∉ Set.Ioi 0hn:¬V x = 0hp:1 / 2 ≤ x⊢ False simp only [Set.mem_Ioi,not_lt] at hxf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0x:ℝhn:¬V x = 0hp:1 / 2 ≤ xhx:x ≤ 0⊢ False linarithrefine_2f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 2 * ↑π / ↑√3 * ∫ (t : ℝ) in Set.Ioi 0, V t ≠ 0 rw [he,refine_2f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 2 * ↑π / ↑√3 * ∫ (x : ℝ), ↑(↑f x) ≠ 0integral_complex_ofRealrefine_2f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 2 * ↑π / ↑√3 * ↑(∫ (x : ℝ), ↑f x) ≠ 0]refine_2f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 2 * ↑π / ↑√3 * ↑(∫ (x : ℝ), ↑f x) ≠ 0 apply mul_ne_zerorefine_2.haf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 2 * ↑π / ↑√3 ≠ 0hbf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ ↑(∫ (x : ℝ), ↑f x) ≠ 0 ·refine_2.haf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 2 * ↑π / ↑√3 ≠ 0 apply div_ne_zerorefine_2.ha.haf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 2 * ↑π ≠ 0hbf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ ↑√3 ≠ 0 ·refine_2.ha.haf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 2 * ↑π ≠ 0 exact mul_ne_zero (byf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 2 ≠ 0 norm_numAll goals completed! 🐙) (byf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ ↑π ≠ 0 exact_mod_cast Real.pi_ne_zeroAll goals completed! 🐙) ·hbf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ ↑√3 ≠ 0 exact_mod_cast (Real.sqrt_ne_zero'.mpr (byf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ 0 < 3 norm_numAll goals completed! 🐙 : (0:ℝ)<3)) ·hbf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)⊢ ↑(∫ (x : ℝ), ↑f x) ≠ 0 have hfint : Integrable (f:ℝ→ℝ) := f.continuous.integrable_of_hasCompactSupport f.hasCompactSupporthbf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)hfint:Integrable (↑f) volume⊢ ↑(∫ (x : ℝ), ↑f x) ≠ 0 have hfpos : 0 < ∫x : ℝ,f x := by⊢ ∃ V, (∀ (x : ℝ), ‖V x‖ ≤ 1) ∧ Function.support ⇑V ⊆ Set.Icc (1 / 2) 1 ∧ V 0 = 0 ∧ paperRadialFourier (⇑V) 0 ≠ 0 apply (integral_pos_iff_support_of_nonneg f.nonneg' hfint).mprf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)hfint:Integrable (↑f) volume⊢ 0 < volume (Function.support ↑f) rw [f.support_eqf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)hfint:Integrable (↑f) volume⊢ 0 < volume (ball (3 / 4) f.rOut)]f:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)hfint:Integrable (↑f) volume⊢ 0 < volume (ball (3 / 4) f.rOut) exact measure_ball_pos volume _ f.rOut_poshbf:ContDiffBump (3 / 4) := { rIn := 1 / 8, rOut := 1 / 4, rIn_pos := ⋯, rIn_lt_rOut := ⋯ }g:ℝ → ℂ := fun x => ↑(↑f x)hgs:ContDiff ℝ ∞ ghsupport:Function.support g ⊆ Set.Icc (1 / 2) 1hgc:HasCompactSupport gV:𝓢(ℝ, ℂ) := hgc.toSchwartzMap hgshz:V 0 = 0he:∫ (x : ℝ) in Set.Ioi 0, V x = ∫ (x : ℝ), ↑(↑f x)hfint:Integrable (↑f) volumehfpos:0 < ∫ (x : ℝ), ↑f x⊢ ↑(∫ (x : ℝ), ↑f x) ≠ 0 exact_mod_cast hfpos.ne'All goals completed! 🐙endsectionopen scoped BigOperators Classicalopen ActualEisensteinCubicopen ConcretePrimeRowBridge hiding Oopen ShortDraftHeckeBridgelemma prime_coprime_span_iff (P : Ideal ActualEisensteinCubic.O) [P.IsMaximal] (b : ActualEisensteinCubic.O) : IsCoprime P (Ideal.span {b}) ↔ b∉P := byP:Ideal ActualEisensteinCubic.Oinst✝:P.IsMaximalb:ActualEisensteinCubic.O⊢ IsCoprime P (span {b}) ↔ b ∉ P rw [Ideal.isCoprime_iff_codisjoint,P:Ideal ActualEisensteinCubic.Oinst✝:P.IsMaximalb:ActualEisensteinCubic.O⊢ Codisjoint P (span {b}) ↔ b ∉ P ←(Ideal.isMaximal_def.mp (inferInstance : P.IsMaximal)).not_le_iff_codisjoint,P:Ideal ActualEisensteinCubic.Oinst✝:P.IsMaximalb:ActualEisensteinCubic.O⊢ ¬span {b} ≤ P ↔ b ∉ P Ideal.span_singleton_le_iff_memP:Ideal ActualEisensteinCubic.Oinst✝:P.IsMaximalb:ActualEisensteinCubic.O⊢ b ∉ P ↔ b ∉ P]All goals completed! 🐙lemma squarefree_sixth_row_coprime (F : Finset (Ideal ActualEisensteinCubic.O)) (hF : ∀I∈F,I≠⊥) (hg : ∀I∈F,∀P∈UniqueFactorizationMonoid.normalizedFactors I,goodLambda∉P) {I : Ideal ActualEisensteinCubic.O} (hI : I∈F) (hsq : Squarefree I) (b : ActualEisensteinCubic.O) : idealSexticRow F hF hg I (b^6)=if IsCoprime I (Ideal.span {b}) then 1 else 0 := byF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.O⊢ idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then 1 else 0 let : ∀i : primePool F,(i.val).IsMaximal:=primePool_maximal F hFF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···⊢ idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then 1 else 0 have hc : IsCoprime I (Ideal.span {b}) ↔ ¬∃i∈idealSupport F I,b∈i.val := by conv_lhs => rw [←idealSupport_product_eq F hI hsq]F:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···| IsCoprime (∏ i ∈ idealSupport F I, ↑i) (span {b}) rw [IsCoprime.prod_left_iffF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···⊢ (∀ i ∈ idealSupport F I, IsCoprime (↑i) (span {b})) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑i]F:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···⊢ (∀ i ∈ idealSupport F I, IsCoprime (↑i) (span {b})) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑i simp only [prime_coprime_span_iff,not_exists,not_and]F:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···hc:IsCoprime I (span {b}) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑i⊢ idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then 1 else 0 rw [idealSexticRow_sixth_mask,F:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···hc:IsCoprime I (span {b}) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑i⊢ rowCoprimeMask (fun i => ↑i) (idealSupport F I) b = if IsCoprime I (span {b}) then 1 else 0hcF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···hc:IsCoprime I (span {b}) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑i⊢ rowCoprimeMask (fun i => ↑i) (idealSupport F I) b = if ¬∃ i ∈ idealSupport F I, b ∈ ↑i then 1 else 0]F:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···hc:IsCoprime I (span {b}) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑i⊢ rowCoprimeMask (fun i => ↑i) (idealSupport F I) b = if ¬∃ i ∈ idealSupport F I, b ∈ ↑i then 1 else 0 by_cases hn : ∃i∈idealSupport F I,b∈i.valposF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···hc:IsCoprime I (span {b}) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑ihn:∃ i ∈ idealSupport F I, b ∈ ↑i⊢ rowCoprimeMask (fun i => ↑i) (idealSupport F I) b = if ¬∃ i ∈ idealSupport F I, b ∈ ↑i then 1 else 0negF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···hc:IsCoprime I (span {b}) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑ihn:¬∃ i ∈ idealSupport F I, b ∈ ↑i⊢ rowCoprimeMask (fun i => ↑i) (idealSupport F I) b = if ¬∃ i ∈ idealSupport F I, b ∈ ↑i then 1 else 0 <;>posF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···hc:IsCoprime I (span {b}) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑ihn:∃ i ∈ idealSupport F I, b ∈ ↑i⊢ rowCoprimeMask (fun i => ↑i) (idealSupport F I) b = if ¬∃ i ∈ idealSupport F I, b ∈ ↑i then 1 else 0negF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal ActualEisensteinCubic.OhI:I ∈ Fhsq:Squarefree Ib:ActualEisensteinCubic.Othis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···hc:IsCoprime I (span {b}) ↔ ¬∃ i ∈ idealSupport F I, b ∈ ↑ihn:¬∃ i ∈ idealSupport F I, b ∈ ↑i⊢ rowCoprimeMask (fun i => ↑i) (idealSupport F I) b = if ¬∃ i ∈ idealSupport F I, b ∈ ↑i then 1 else 0 simp [rowCoprimeMask,hn]All goals completed! 🐙theorem idealRowSum_sixth_eq_coprime_sum {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)) (hF : ∀I∈F,I≠⊥) (hg : ∀I∈F,∀P∈UniqueFactorizationMonoid.normalizedFactors I,goodLambda∉P) (χ : DirichletCharacter ℂ q) (W : ℕ→ℂ) (b : ActualEisensteinCubic.O) : idealRowSum F hF hg χ W (b^6)= ∑I∈F with IsCoprime I (Ideal.span {b}),baseChangeWeight χ I*W (Ideal.absNorm I) := byq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.O⊢ idealRowSum F hF hg χ W (b ^ 6) = ∑ I ∈ F with IsCoprime I (span {b}), baseChangeWeight χ I * W (absNorm I) rw [idealRowSum,q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.O⊢ ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = ∑ I ∈ F with IsCoprime I (span {b}), baseChangeWeight χ I * W (absNorm I)Finset.sum_filterq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.O⊢ ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = ∑ a ∈ F, if IsCoprime a (span {b}) then baseChangeWeight χ a * W (absNorm a) else 0]q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.O⊢ ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = ∑ a ∈ F, if IsCoprime a (span {b}) then baseChangeWeight χ a * W (absNorm a) else 0 apply Finset.sum_congr rflq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.O⊢ ∀ x ∈ F, baseChangeWeight χ x * W (absNorm x) * idealSexticRow F hF hg x (b ^ 6) = if IsCoprime x (span {b}) then baseChangeWeight χ x * W (absNorm x) else 0 intro I hIq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ F⊢ baseChangeWeight χ I * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then baseChangeWeight χ I * W (absNorm I) else 0 by_cases hsq : Squarefree Iposq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:Squarefree I⊢ baseChangeWeight χ I * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then baseChangeWeight χ I * W (absNorm I) else 0negq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:¬Squarefree I⊢ baseChangeWeight χ I * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then baseChangeWeight χ I * W (absNorm I) else 0 ·posq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:Squarefree I⊢ baseChangeWeight χ I * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then baseChangeWeight χ I * W (absNorm I) else 0 rw [squarefree_sixth_row_coprime F hF hg hI hsq bposq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:Squarefree I⊢ (baseChangeWeight χ I * W (absNorm I) * if IsCoprime I (span {b}) then 1 else 0) = if IsCoprime I (span {b}) then baseChangeWeight χ I * W (absNorm I) else 0]posq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:Squarefree I⊢ (baseChangeWeight χ I * W (absNorm I) * if IsCoprime I (span {b}) then 1 else 0) = if IsCoprime I (span {b}) then baseChangeWeight χ I * W (absNorm I) else 0 split_ifsposq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:Squarefree Ih✝:IsCoprime I (span {b})⊢ baseChangeWeight χ I * W (absNorm I) * 1 = baseChangeWeight χ I * W (absNorm I)negq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:Squarefree Ih✝:¬IsCoprime I (span {b})⊢ baseChangeWeight χ I * W (absNorm I) * 0 = 0 <;>posq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:Squarefree Ih✝:IsCoprime I (span {b})⊢ baseChangeWeight χ I * W (absNorm I) * 1 = baseChangeWeight χ I * W (absNorm I)negq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:Squarefree Ih✝:¬IsCoprime I (span {b})⊢ baseChangeWeight χ I * W (absNorm I) * 0 = 0 simpAll goals completed! 🐙 ·negq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:¬Squarefree I⊢ baseChangeWeight χ I * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then baseChangeWeight χ I * W (absNorm I) else 0 rw [ConcretePrimeRowBridge.baseChangeWeight_zero_of_not_squarefree χ I hsqnegq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:¬Squarefree I⊢ 0 * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then 0 * W (absNorm I) else 0]negq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂb:ActualEisensteinCubic.OI:Ideal ConcretePrimeRowBridge.OhI:I ∈ Fhsq:¬Squarefree I⊢ 0 * W (absNorm I) * idealSexticRow F hF hg I (b ^ 6) = if IsCoprime I (span {b}) then 0 * W (absNorm I) else 0 simpAll goals completed! 🐙endsectionopen scoped BigOperators Classical SchwartzMap ContDiffsectionopen ActualEisensteinCubicopen ConcretePrimeRowBridge hiding Oopen EisensteinSchwartzPoisson hiding Oopen IdealMobiusDivisorSum hiding Oopen ConcreteTraceCRT ShortDraftHeckeBridgeopen QuadraticInitialBound hiding Odef averagingRows (Y : ℝ) : Finset ActualEisensteinCubic.O := rowNormDisk ⌊Y⌋₊theorem mem_averagingRows {Y : ℝ} {b : ActualEisensteinCubic.O} (hY : 0≤Y) : b∈averagingRows Y ↔ b≠0 ∧ ‖eisEmbedding b‖^2≤Y := byY:ℝb:ActualEisensteinCubic.OhY:0 ≤ Y⊢ b ∈ averagingRows Y ↔ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y rw [averagingRows,Y:ℝb:ActualEisensteinCubic.OhY:0 ≤ Y⊢ b ∈ rowNormDisk ⌊Y⌋₊ ↔ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Ymem_rowNormDiskY:ℝb:ActualEisensteinCubic.OhY:0 ≤ Y⊢ 0 < absNorm (span {b}) ∧ absNorm (span {b}) ≤ ⌊Y⌋₊ ↔ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y]Y:ℝb:ActualEisensteinCubic.OhY:0 ≤ Y⊢ 0 < absNorm (span {b}) ∧ absNorm (span {b}) ≤ ⌊Y⌋₊ ↔ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y have hz : 0<Ideal.absNorm (Ideal.span {b}:Ideal ActualEisensteinCubic.O) ↔ b≠0 := byY:ℝb:ActualEisensteinCubic.OhY:0 ≤ Y⊢ b ∈ averagingRows Y ↔ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y rw [Nat.pos_iff_ne_zero,Y:ℝb:ActualEisensteinCubic.OhY:0 ≤ Y⊢ absNorm (span {b}) ≠ 0 ↔ b ≠ 0ne_eq,Y:ℝb:ActualEisensteinCubic.OhY:0 ≤ Y⊢ ¬absNorm (span {b}) = 0 ↔ b ≠ 0Ideal.absNorm_eq_zero_iff,Y:ℝb:ActualEisensteinCubic.OhY:0 ≤ Y⊢ ¬span {b} = ⊥ ↔ b ≠ 0Ideal.span_singleton_eq_botY:ℝb:ActualEisensteinCubic.OhY:0 ≤ Y⊢ ¬b = 0 ↔ b ≠ 0]Y:ℝb:ActualEisensteinCubic.OhY:0 ≤ Yhz:0 < absNorm (span {b}) ↔ b ≠ 0⊢ 0 < absNorm (span {b}) ∧ absNorm (span {b}) ≤ ⌊Y⌋₊ ↔ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y rw [hz,Y:ℝb:ActualEisensteinCubic.OhY:0 ≤ Yhz:0 < absNorm (span {b}) ↔ b ≠ 0⊢ b ≠ 0 ∧ absNorm (span {b}) ≤ ⌊Y⌋₊ ↔ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ YNat.le_floor_iff hY,Y:ℝb:ActualEisensteinCubic.OhY:0 ≤ Yhz:0 < absNorm (span {b}) ↔ b ≠ 0⊢ b ≠ 0 ∧ ↑(absNorm (span {b})) ≤ Y ↔ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y←eisEmbedding_norm_sq_eq_absNorm_spanY:ℝb:ActualEisensteinCubic.OhY:0 ≤ Yhz:0 < absNorm (span {b}) ↔ b ≠ 0⊢ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y ↔ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y]All goals completed! 🐙theorem averagingRows_card (Y : ℝ) (hY : 1≤Y) : ((averagingRows Y).card:ℝ)≤128*Y := DescentFiberCost.finite_element_count_real _ Y hY (fun b hb=>(mem_averagingRows (byY:ℝhY:1 ≤ Yb:DescentFiberCost.Ohb:b ∈ averagingRows Y⊢ 0 ≤ Y linarithAll goals completed! 🐙)).mp hb |>.2)theorem averagingRows_power_norm (Y : ℝ) (hY : 1≤Y) {z : ActualEisensteinCubic.O} (hz : z∈(averagingRows Y).image (fun b=>b^6)) : z≠0 ∧ (Ideal.absNorm (Ideal.span {z}):ℝ)≤Y^6 := byY:ℝhY:1 ≤ Yz:ActualEisensteinCubic.Ohz:z ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)⊢ z ≠ 0 ∧ ↑(absNorm (span {z})) ≤ Y ^ 6 obtain ⟨b,hb,rfl⟩:=Finset.mem_image.mp hzY:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)⊢ b ^ 6 ≠ 0 ∧ ↑(absNorm (span {b ^ 6})) ≤ Y ^ 6 have hh:=(mem_averagingRows (byY:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)⊢ 0 ≤ Y linarithAll goals completed! 🐙 : (0:ℝ)≤Y)).mp hbY:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)hh:b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y⊢ b ^ 6 ≠ 0 ∧ ↑(absNorm (span {b ^ 6})) ≤ Y ^ 6 refine ⟨pow_ne_zero _ hh.1,?_⟩Y:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)hh:b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y⊢ ↑(absNorm (span {b ^ 6})) ≤ Y ^ 6 rw [←eisEmbedding_norm_sq_eq_absNorm_span,Y:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)hh:b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y⊢ ‖eisEmbedding (b ^ 6)‖ ^ 2 ≤ Y ^ 6map_pow,Y:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)hh:b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y⊢ ‖eisEmbedding b ^ 6‖ ^ 2 ≤ Y ^ 6norm_pow,Y:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)hh:b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y⊢ (‖eisEmbedding b‖ ^ 6) ^ 2 ≤ Y ^ 6 ←pow_mul,Y:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)hh:b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y⊢ ‖eisEmbedding b‖ ^ (6 * 2) ≤ Y ^ 6show (6:ℕ)*2=2*6 byY:ℝhY:1 ≤ Yz:ActualEisensteinCubic.Ohz:z ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)⊢ z ≠ 0 ∧ ↑(absNorm (span {z})) ≤ Y ^ 6 omegaAll goals completed! 🐙,pow_mulY:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)hh:b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y⊢ (‖eisEmbedding b‖ ^ 2) ^ 6 ≤ Y ^ 6]Y:ℝhY:1 ≤ Yb:ActualEisensteinCubic.Ohb:b ∈ averagingRows Yhz:b ^ 6 ∈ Finset.image (fun b => b ^ 6) (averagingRows Y)hh:b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y⊢ (‖eisEmbedding b‖ ^ 2) ^ 6 ≤ Y ^ 6 exact pow_le_pow_left₀ (sq_nonneg _) hh.2 _All goals completed! 🐙theorem average_tsum_eq_finite (V : 𝓢(ℝ,ℂ)) (hV : Function.support (V:ℝ→ℂ)⊆Set.Icc ((1:ℝ)/2) 1) (hV0 : V 0=0) (Y : ℝ) (hY : 0<Y) (A : ActualEisensteinCubic.O→ℂ) : (∑'b : ActualEisensteinCubic.O,V (‖eisEmbedding b‖^2/Y)*A (b^6))= ∑b∈averagingRows Y,V (‖eisEmbedding b‖^2/Y)*A (b^6) := byV:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂ⊢ ∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * A (b ^ 6) = ∑ b ∈ averagingRows Y, V (‖eisEmbedding b‖ ^ 2 / Y) * A (b ^ 6) apply tsum_eq_sumV:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂ⊢ ∀ b ∉ averagingRows Y, V (‖eisEmbedding b‖ ^ 2 / Y) * A (b ^ 6) = 0 intro b hbV:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Y⊢ V (‖eisEmbedding b‖ ^ 2 / Y) * A (b ^ 6) = 0 have hz : V (‖eisEmbedding b‖^2/Y)=0 := byV:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂ⊢ ∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * A (b ^ 6) = ∑ b ∈ averagingRows Y, V (‖eisEmbedding b‖ ^ 2 / Y) * A (b ^ 6) by_contra hvV:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhv:¬V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ False apply hbV:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhv:¬V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ b ∈ averagingRows Y apply (mem_averagingRows hY.le).mprV:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhv:¬V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ b ≠ 0 ∧ ‖eisEmbedding b‖ ^ 2 ≤ Y refine ⟨?_,?_⟩refine_1V:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhv:¬V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ b ≠ 0refine_2V:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhv:¬V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ ‖eisEmbedding b‖ ^ 2 ≤ Y ·refine_1V:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhv:¬V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ b ≠ 0 intro herefine_1V:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhv:¬V (‖eisEmbedding b‖ ^ 2 / Y) = 0he:b = 0⊢ False simp only [he,map_zero,norm_zero,zero_pow (by decide : (2:ℕ)≠0),zero_div,hV0] at hvrefine_1V:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhe:b = 0hv:¬True⊢ False exact hv trivialAll goals completed! 🐙 ·refine_2V:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhv:¬V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ ‖eisEmbedding b‖ ^ 2 ≤ Y exact (div_le_one hY).mp (hV hv).2V:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhz:V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ V (‖eisEmbedding b‖ ^ 2 / Y) * A (b ^ 6) = 0 rw [hz,V:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhz:V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ 0 * A (b ^ 6) = 0zero_mulV:𝓢(ℝ, ℂ)hV:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:0 < YA:ActualEisensteinCubic.O → ℂb:ActualEisensteinCubic.Ohb:b ∉ averagingRows Yhz:V (‖eisEmbedding b‖ ^ 2 / Y) = 0⊢ 0 = 0]All goals completed! 🐙theorem average_tsum_cauchy (V : 𝓢(ℝ,ℂ)) (hV : ∀x,‖V x‖≤1) (hs : Function.support (V:ℝ→ℂ)⊆Set.Icc ((1:ℝ)/2) 1) (hV0 : V 0=0) (Y : ℝ) (hY : 1≤Y) (A : ActualEisensteinCubic.O→ℂ) : ‖∑'b : ActualEisensteinCubic.O,V (‖eisEmbedding b‖^2/Y)*A (b^6)‖^2≤ 768*Y*∑z∈(averagingRows Y).image (fun b=>b^6),‖A z‖^2 := byV:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:1 ≤ YA:ActualEisensteinCubic.O → ℂ⊢ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * A (b ^ 6)‖ ^ 2 ≤ 768 * Y * ∑ z ∈ Finset.image (fun b => b ^ 6) (averagingRows Y), ‖A z‖ ^ 2 rw [average_tsum_eq_finite V hs hV0 Y (byV:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:1 ≤ YA:ActualEisensteinCubic.O → ℂ⊢ 0 < Y linarithAll goals completed! 🐙) A]V:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:1 ≤ YA:ActualEisensteinCubic.O → ℂ⊢ ‖∑ b ∈ averagingRows Y, V (‖eisEmbedding b‖ ^ 2 / Y) * A (b ^ 6)‖ ^ 2 ≤ 768 * Y * ∑ z ∈ Finset.image (fun b => b ^ 6) (averagingRows Y), ‖A z‖ ^ 2 apply (sixth_power_average_cauchy _ _ _ (fun b hb=>hV _)).transV:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:1 ≤ YA:ActualEisensteinCubic.O → ℂ⊢ 6 * ↑(#(averagingRows Y)) * ∑ z ∈ Finset.image (fun b => b ^ 6) (averagingRows Y), ‖A z‖ ^ 2 ≤ 768 * Y * ∑ z ∈ Finset.image (fun b => b ^ 6) (averagingRows Y), ‖A z‖ ^ 2 have hc:=averagingRows_card Y hYV:𝓢(ℝ, ℂ)hV:∀ (x : ℝ), ‖V x‖ ≤ 1hs:Function.support ⇑V ⊆ Set.Icc (1 / 2) 1hV0:V 0 = 0Y:ℝhY:1 ≤ YA:ActualEisensteinCubic.O → ℂhc:↑(#(averagingRows Y)) ≤ 128 * Y⊢ 6 * ↑(#(averagingRows Y)) * ∑ z ∈ Finset.image (fun b => b ^ 6) (averagingRows Y), ‖A z‖ ^ 2 ≤ 768 * Y * ∑ z ∈ Finset.image (fun b => b ^ 6) (averagingRows Y), ‖A z‖ ^ 2 nlinarith [Finset.sum_nonneg (s:=(averagingRows Y).image (fun b=>b^6)) (fun z _=>sq_nonneg ‖A z‖)]All goals completed! 🐙theorem average_remainder_small_power (ε : ℝ) (hε : 0<ε) : ∃C : ℝ,0<C ∧ ∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)) (_hF : ∀I∈F,I≠⊥) (χ : DirichletCharacter ℂ q) (W : ℕ→ℂ) (V : 𝓢(ℝ,ℂ)) (Y lengthScale G : ℝ),0<Y → 1≤lengthScale → 0≤G → (∀n,‖W n‖≤G) → (∀I∈F,W (Ideal.absNorm I)≠0→(Ideal.absNorm I:ℝ)≤lengthScale) → ‖∑I∈F,baseChangeWeight χ I*W (Ideal.absNorm I)* maskedPrincipalRemainder (fun i : primePool F=>i.val) (idealSupport F I) V Y‖≤ C*G*pvControl V*lengthScale^(1+ε) := byε:ℝhε:0 < ε⊢ ∃ C, 0 < C ∧ ∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ C * G * pvControl V * lengthScale ^ (1 + ε) obtain ⟨C,hC,hp⟩:=SquarefreeDivisorBound.prime_support_subsets_bound ε hεε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ ε⊢ ∃ C, 0 < C ∧ ∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ C * G * pvControl V * lengthScale ^ (1 + ε) refine ⟨128*C,byε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ ε⊢ 0 < 128 * C positivityAll goals completed! 🐙,?_⟩ intro q F hF χ W V Y lengthScale G hY hL hG hW hnormε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScale⊢ ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ 128 * C * G * pvControl V * lengthScale ^ (1 + ε) apply (sixth_average_remainder_bound F hF χ W V Y hY).transε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScale⊢ ∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ 128 * C * G * pvControl V * lengthScale ^ (1 + ε) let T:=F.filter (fun I=>W (Ideal.absNorm I)≠0)ε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}⊢ ∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ 128 * C * G * pvControl V * lengthScale ^ (1 + ε) have he : (∑I∈F,‖W (Ideal.absNorm I)‖*(2:ℝ)^(primeSupport I).card*pvControl V)= ∑I∈T,‖W (Ideal.absNorm I)‖*(2:ℝ)^(primeSupport I).card*pvControl V := byε:ℝhε:0 < ε⊢ ∃ C, 0 < C ∧ ∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ C * G * pvControl V * lengthScale ^ (1 + ε) symmε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}⊢ ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V apply Finset.sum_subset (Finset.filter_subset _ _)ε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}⊢ ∀ x ∈ F, x ∉ {I ∈ F | W (absNorm I) ≠ 0} → ‖W (absNorm x)‖ * 2 ^ #(primeSupport x) * pvControl V = 0 intro I hI hnε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}I:Ideal ActualEisensteinCubic.OhI:I ∈ Fhn:I ∉ {I ∈ F | W (absNorm I) ≠ 0}⊢ ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = 0 have hz : W (Ideal.absNorm I)=0 := byε:ℝhε:0 < ε⊢ ∃ C, 0 < C ∧ ∀ {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)), (∀ I ∈ F, I ≠ ⊥) → ∀ (χ : DirichletCharacter ℂ q) (W : ℕ → ℂ) (V : 𝓢(ℝ, ℂ)) (Y lengthScale G : ℝ), 0 < Y → 1 ≤ lengthScale → 0 ≤ G → (∀ (n : ℕ), ‖W n‖ ≤ G) → (∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScale) → ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ C * G * pvControl V * lengthScale ^ (1 + ε) by_contra hhε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}I:Ideal ActualEisensteinCubic.OhI:I ∈ Fhn:I ∉ {I ∈ F | W (absNorm I) ≠ 0}hh:¬W (absNorm I) = 0⊢ False exact hn (Finset.mem_filter.mpr ⟨hI,hh⟩)ε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}I:Ideal ActualEisensteinCubic.OhI:I ∈ Fhn:I ∉ {I ∈ F | W (absNorm I) ≠ 0}hz:W (absNorm I) = 0⊢ ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = 0 simp only [hz,norm_zero,zero_mul]ε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V⊢ ∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ 128 * C * G * pvControl V * lengthScale ^ (1 + ε) have hc : (T.card:ℝ)≤128*lengthScale := DescentFiberCost.finite_ideal_count_real T lengthScale hL (fun I hI=>hF I (Finset.mem_filter.mp hI).1) (fun I hI=>hnorm I (Finset.mem_filter.mp hI).1 (Finset.mem_filter.mp hI).2)ε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ ∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ 128 * C * G * pvControl V * lengthScale ^ (1 + ε) rw [heε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ 128 * C * G * pvControl V * lengthScale ^ (1 + ε)]ε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ 128 * C * G * pvControl V * lengthScale ^ (1 + ε) calc _≤∑I∈T,G*(C*lengthScale^ε)*pvControl V := byε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ ∑ I ∈ T, G * (C * lengthScale ^ ε) * pvControl V apply Finset.sum_le_sumε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ ∀ i ∈ T, ‖W (absNorm i)‖ * 2 ^ #(primeSupport i) * pvControl V ≤ G * (C * lengthScale ^ ε) * pvControl V intro I hIε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScaleI:Ideal ActualEisensteinCubic.OhI:I ∈ T⊢ ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ G * (C * lengthScale ^ ε) * pvControl V have hh:=Finset.mem_filter.mp hIε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScaleI:Ideal ActualEisensteinCubic.OhI:I ∈ Thh:I ∈ F ∧ W (absNorm I) ≠ 0⊢ ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ G * (C * lengthScale ^ ε) * pvControl V have hb:=(hp I (hF I hh.1)).trans (mul_le_mul_of_nonneg_left (Real.rpow_le_rpow (Nat.cast_nonneg _) (hnorm I hh.1 hh.2) hε.le) hC.le)ε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScaleI:Ideal ActualEisensteinCubic.OhI:I ∈ Thh:I ∈ F ∧ W (absNorm I) ≠ 0hb:2 ^ #(primeSupport I) ≤ C * lengthScale ^ ε⊢ ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V ≤ G * (C * lengthScale ^ ε) * pvControl V exact mul_le_mul_of_nonneg_right (mul_le_mul (hW _) hb (byε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScaleI:Ideal ActualEisensteinCubic.OhI:I ∈ Thh:I ∈ F ∧ W (absNorm I) ≠ 0hb:2 ^ #(primeSupport I) ≤ C * lengthScale ^ ε⊢ 0 ≤ 2 ^ #(primeSupport I) positivityAll goals completed! 🐙) hG) (pvControl_nonneg V) _=(T.card:ℝ)*(G*(C*lengthScale^ε)*pvControl V) := byε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ ∑ I ∈ T, G * (C * lengthScale ^ ε) * pvControl V = ↑(#T) * (G * (C * lengthScale ^ ε) * pvControl V) simpAll goals completed! 🐙 _≤128*lengthScale*(G*(C*lengthScale^ε)*pvControl V) := mul_le_mul_of_nonneg_right hc (mul_nonneg (byε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ 0 ≤ G * (C * lengthScale ^ ε) positivityAll goals completed! 🐙) (pvControl_nonneg V)) _=(128*C)*G*pvControl V*lengthScale^(1+ε) := byε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ 128 * lengthScale * (G * (C * lengthScale ^ ε) * pvControl V) = 128 * C * G * pvControl V * lengthScale ^ (1 + ε) rw [Real.rpow_add (byε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ 0 < lengthScale linarithAll goals completed! 🐙 : (0:ℝ)<lengthScale),Real.rpow_oneε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ 128 * lengthScale * (G * (C * lengthScale ^ ε) * pvControl V) = 128 * C * G * pvControl V * (lengthScale * lengthScale ^ ε)]ε:ℝhε:0 < εC:ℝhC:0 < Chp:∀ (I : Ideal SquarefreeDivisorBound.O), I ≠ ⊥ → 2 ^ #(primeSupport I) ≤ C * ↑(absNorm I) ^ εq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥χ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝlengthScale:ℝG:ℝhY:0 < YhL:1 ≤ lengthScalehG:0 ≤ GhW:∀ (n : ℕ), ‖W n‖ ≤ Ghnorm:∀ I ∈ F, W (absNorm I) ≠ 0 → ↑(absNorm I) ≤ lengthScaleT:Finset (Ideal ActualEisensteinCubic.O) := {I ∈ F | W (absNorm I) ≠ 0}he:∑ I ∈ F, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl V = ∑ I ∈ T, ‖W (absNorm I)‖ * 2 ^ #(primeSupport I) * pvControl Vhc:↑(#T) ≤ 128 * lengthScale⊢ 128 * lengthScale * (G * (C * lengthScale ^ ε) * pvControl V) = 128 * C * G * pvControl V * (lengthScale * lengthScale ^ ε) ringAll goals completed! 🐙theorem totient_sum_normalized_bound {q : ℕ} (F : Finset (Ideal ActualEisensteinCubic.O)) (hF : ∀I∈F,I≠⊥) (hg : ∀I∈F,∀P∈UniqueFactorizationMonoid.normalizedFactors I,goodLambda∉P) (χ : DirichletCharacter ℂ q) (W : ℕ→ℂ) (V : 𝓢(ℝ,ℂ)) (Y : ℝ) (hY : 0<Y) : Y*‖paperRadialFourier V 0‖* ‖∑I∈F,baseChangeWeight χ I*W (Ideal.absNorm I)*totientDensity I‖≤ ‖∑'b : ActualEisensteinCubic.O,V (‖eisEmbedding b‖^2/Y)*idealRowSum F hF hg χ W (b^6)‖+ ‖∑I∈F,baseChangeWeight χ I*W (Ideal.absNorm I)* maskedPrincipalRemainder (fun i : primePool F=>i.val) (idealSupport F I) V Y‖ := byq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Y⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ have he:=idealRowSum_sixth_average F hF hg χ W V Y hYq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ have hh:=norm_sub_le (∑'b : ActualEisensteinCubic.O,V (‖eisEmbedding b‖^2/Y)*idealRowSum F hF hg χ W (b^6)) (∑I∈F,baseChangeWeight χ I*W (Ideal.absNorm I)* maskedPrincipalRemainder (fun i : primePool F=>i.val) (idealSupport F I) V Y)q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) - ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ rw [he,q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y - ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ ≤ ‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖add_sub_cancel_right,q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖norm_mul,q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:‖↑Y * paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖norm_mul,q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:‖↑Y‖ * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖Complex.norm_real,q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:‖Y‖ * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖Real.norm_eq_abs,q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:|Y| * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖abs_of_pos hYq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖] at hhq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ rwa [←heq:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖]q:ℕF:Finset (Ideal ActualEisensteinCubic.O)hF:∀ I ∈ F, I ≠ ⊥hg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pχ:DirichletCharacter ℂ qW:ℕ → ℂV:𝓢(ℝ, ℂ)Y:ℝhY:0 < Yhe:∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6) = ↑Y * paperRadialFourier (⇑V) 0 * ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I + ∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Yhh:Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖⊢ Y * ‖paperRadialFourier (⇑V) 0‖ * ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * totientDensity I‖ ≤ ‖∑' (b : ActualEisensteinCubic.O), V (‖eisEmbedding b‖ ^ 2 / Y) * idealRowSum F hF hg χ W (b ^ 6)‖ + ‖∑ I ∈ F, baseChangeWeight χ I * W (absNorm I) * maskedPrincipalRemainder (fun i => ↑i) (idealSupport F I) (⇑V) Y‖ at hhendopen ActualEisensteinCubicopen ConcretePrimeRowBridge hiding Oopen EisensteinSchwartzPoisson hiding Oopen ConcreteTraceCRT ShortDraftHeckeBridgeopen QuadraticInitialBound hiding Oopen InitialMeanSquareopen CanonicalQuadraticSieve hiding Oopen SecondPassArithmetic hiding Oopen CanonicalRowCompletionendsectionopen scoped BigOperators Classical SchwartzMap ContDiff Topologyopen Filter Asymptotics MeasureTheoryopen ActualEisensteinCubicopen ConcretePrimeRowBridge hiding Oopen ShortDraftHeckeBridgeopen IdealMobiusDivisorSum hiding Oopen CanonicalQuadraticSieve hiding Oopen SecondPassArithmetic hiding Oopen CanonicalRowCompletionopen InitialMeanSquaredef weightedMoebius {q : ℕ} (χ : DirichletCharacter ℂ q) (I : Ideal ActualEisensteinCubic.O) : ℂ := baseChangeWeight χ I*totientDensity Idef outsideWeight {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) : Ideal ActualEisensteinCubic.O→ℂ := FiniteSFactor.outsideWeight S (weightedMoebius χ)def weightedCoeff {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) : ℕ→ℂ := FiniteSFactor.outsideCoeff S (weightedMoebius χ)theorem totientDensity_norm_le_one (I : Ideal ActualEisensteinCubic.O) : ‖totientDensity I‖≤1 := byI:Ideal ActualEisensteinCubic.O⊢ ‖totientDensity I‖ ≤ 1 rw [totientDensity,I:Ideal ActualEisensteinCubic.O⊢ ‖∏ P ∈ primeSupport I, (1 - 1 / ↑(absNorm P))‖ ≤ 1norm_prodI:Ideal ActualEisensteinCubic.O⊢ ∏ b ∈ primeSupport I, ‖1 - 1 / ↑(absNorm b)‖ ≤ 1]I:Ideal ActualEisensteinCubic.O⊢ ∏ b ∈ primeSupport I, ‖1 - 1 / ↑(absNorm b)‖ ≤ 1 apply Finset.prod_le_one₀h0I:Ideal ActualEisensteinCubic.O⊢ ∀ i ∈ primeSupport I, 0 ≤ ‖1 - 1 / ↑(absNorm i)‖h1I:Ideal ActualEisensteinCubic.O⊢ ∀ i ∈ primeSupport I, ‖1 - 1 / ↑(absNorm i)‖ ≤ 1 ·h0I:Ideal ActualEisensteinCubic.O⊢ ∀ i ∈ primeSupport I, 0 ≤ ‖1 - 1 / ↑(absNorm i)‖ intro P hPh0I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport I⊢ 0 ≤ ‖1 - 1 / ↑(absNorm P)‖ exact norm_nonneg _All goals completed! 🐙 ·h1I:Ideal ActualEisensteinCubic.O⊢ ∀ i ∈ primeSupport I, ‖1 - 1 / ↑(absNorm i)‖ ≤ 1 intro P hPh1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport I⊢ ‖1 - 1 / ↑(absNorm P)‖ ≤ 1 have hN : (2:ℝ)≤Ideal.absNorm P:=byI:Ideal ActualEisensteinCubic.O⊢ ‖totientDensity I‖ ≤ 1 exact_mod_cast IdealDivisorBound.support_norm_two_le hPh1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)⊢ ‖1 - 1 / ↑(absNorm P)‖ ≤ 1 have hNp : (0:ℝ)<Ideal.absNorm P:=byI:Ideal ActualEisensteinCubic.O⊢ ‖totientDensity I‖ ≤ 1 linarithh1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)⊢ ‖1 - 1 / ↑(absNorm P)‖ ≤ 1 have he : (1-(1:ℂ)/(Ideal.absNorm P:ℂ))=((1-1/(Ideal.absNorm P:ℝ):ℝ):ℂ) := byI:Ideal ActualEisensteinCubic.O⊢ ‖totientDensity I‖ ≤ 1 push_castI:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)⊢ 1 - 1 / ↑(absNorm P) = 1 - 1 / ↑(absNorm P);rflh1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ ‖1 - 1 / ↑(absNorm P)‖ ≤ 1 rw [he,h1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ ‖↑(1 - 1 / ↑(absNorm P))‖ ≤ 1Complex.norm_real,h1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ ‖1 - 1 / ↑(absNorm P)‖ ≤ 1Real.norm_eq_abs,h1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ |1 - 1 / ↑(absNorm P)| ≤ 1abs_of_nonnegh1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ 1 - 1 / ↑(absNorm P) ≤ 1h1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ 0 ≤ 1 - 1 / ↑(absNorm P)]h1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ 1 - 1 / ↑(absNorm P) ≤ 1h1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ 0 ≤ 1 - 1 / ↑(absNorm P) ·h1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ 1 - 1 / ↑(absNorm P) ≤ 1 exact sub_le_self _ (byI:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ 0 ≤ 1 / ↑(absNorm P) positivityAll goals completed! 🐙) ·h1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ 0 ≤ 1 - 1 / ↑(absNorm P) have hi : (1:ℝ)/(Ideal.absNorm P:ℝ)≤1 := (div_le_one hNp).mpr (byI:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))⊢ 1 ≤ ↑(absNorm P) linarithAll goals completed! 🐙)h1I:Ideal ActualEisensteinCubic.OP:Ideal IdealMobiusDivisorSum.OhP:P ∈ primeSupport IhN:2 ≤ ↑(absNorm P)hNp:0 < ↑(absNorm P)he:1 - 1 / ↑(absNorm P) = ↑(1 - 1 / ↑(absNorm P))hi:1 / ↑(absNorm P) ≤ 1⊢ 0 ≤ 1 - 1 / ↑(absNorm P) linarithAll goals completed! 🐙theorem weightedMoebius_norm_le_one {q : ℕ} (χ : DirichletCharacter ℂ q) (I : Ideal ActualEisensteinCubic.O) : ‖weightedMoebius χ I‖≤1 := byq:ℕχ:DirichletCharacter ℂ qI:Ideal ActualEisensteinCubic.O⊢ ‖weightedMoebius χ I‖ ≤ 1 rw [weightedMoebius,q:ℕχ:DirichletCharacter ℂ qI:Ideal ActualEisensteinCubic.O⊢ ‖baseChangeWeight χ I * totientDensity I‖ ≤ 1norm_mulq:ℕχ:DirichletCharacter ℂ qI:Ideal ActualEisensteinCubic.O⊢ ‖baseChangeWeight χ I‖ * ‖totientDensity I‖ ≤ 1]q:ℕχ:DirichletCharacter ℂ qI:Ideal ActualEisensteinCubic.O⊢ ‖baseChangeWeight χ I‖ * ‖totientDensity I‖ ≤ 1 exact (mul_le_mul (ConcretePrimeRowBridge.baseChangeWeight_norm_le_one χ I) (totientDensity_norm_le_one I) (norm_nonneg _) zero_le_one).trans_eq (mul_one _)All goals completed! 🐙@[simp] theorem weightedMoebius_zero {q : ℕ} (χ : DirichletCharacter ℂ q) : weightedMoebius χ (0:Ideal ActualEisensteinCubic.O)=0 := byq:ℕχ:DirichletCharacter ℂ q⊢ weightedMoebius χ 0 = 0 change ((UniqueFactorizationMonoid.moebius (0:Ideal ActualEisensteinCubic.O):ℂ)* χ (Ideal.absNorm (0:Ideal ActualEisensteinCubic.O)))*totientDensity 0=0q:ℕχ:DirichletCharacter ℂ q⊢ ↑(moebius 0) * χ ↑(absNorm 0) * totientDensity 0 = 0 rw [UniqueFactorizationMonoid.moebius_zero,q:ℕχ:DirichletCharacter ℂ q⊢ ↑0 * χ ↑(absNorm 0) * totientDensity 0 = 0Int.cast_zero,q:ℕχ:DirichletCharacter ℂ q⊢ 0 * χ ↑(absNorm 0) * totientDensity 0 = 0zero_mul,q:ℕχ:DirichletCharacter ℂ q⊢ 0 * totientDensity 0 = 0zero_mulq:ℕχ:DirichletCharacter ℂ q⊢ 0 = 0]All goals completed! 🐙theorem outsideWeight_norm_le_one {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (I : Ideal ActualEisensteinCubic.O) : ‖outsideWeight χ S I‖≤1 := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal ActualEisensteinCubic.O⊢ ‖outsideWeight χ S I‖ ≤ 1 unfold outsideWeight FiniteSFactor.outsideWeightq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal ActualEisensteinCubic.O⊢ ‖if ∀ P ∈ S, ¬P ∣ I then weightedMoebius χ I else 0‖ ≤ 1 split_ifsposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal ActualEisensteinCubic.Oh✝:∀ P ∈ S, ¬P ∣ I⊢ ‖weightedMoebius χ I‖ ≤ 1negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal ActualEisensteinCubic.Oh✝:¬∀ P ∈ S, ¬P ∣ I⊢ ‖0‖ ≤ 1 ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal ActualEisensteinCubic.Oh✝:∀ P ∈ S, ¬P ∣ I⊢ ‖weightedMoebius χ I‖ ≤ 1 exact weightedMoebius_norm_le_one χ IAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal ActualEisensteinCubic.Oh✝:¬∀ P ∈ S, ¬P ∣ I⊢ ‖0‖ ≤ 1 simpAll goals completed! 🐙@[simp] theorem outsideWeight_zero {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) : outsideWeight χ S (0:Ideal ActualEisensteinCubic.O)=0 := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)⊢ outsideWeight χ S 0 = 0 unfold outsideWeight FiniteSFactor.outsideWeightq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)⊢ (if ∀ P ∈ S, ¬P ∣ 0 then weightedMoebius χ 0 else 0) = 0 split_ifsposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)h✝:∀ P ∈ S, ¬P ∣ 0⊢ weightedMoebius χ 0 = 0negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)h✝:¬∀ P ∈ S, ¬P ∣ 0⊢ 0 = 0 ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)h✝:∀ P ∈ S, ¬P ∣ 0⊢ weightedMoebius χ 0 = 0 exact weightedMoebius_zero χAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)h✝:¬∀ P ∈ S, ¬P ∣ 0⊢ 0 = 0 rflAll goals completed! 🐙@[simp] theorem weightedCoeff_zero {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) : weightedCoeff χ S 0=0 := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)⊢ weightedCoeff χ S 0 = 0 unfold weightedCoeff FiniteSFactor.outsideCoeffq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)⊢ ∑ I ∈ FiniteSFactor.fiber 0, FiniteSFactor.outsideWeight S (weightedMoebius χ) I = 0 apply Finset.sum_eq_zeroq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)⊢ ∀ x ∈ FiniteSFactor.fiber 0, FiniteSFactor.outsideWeight S (weightedMoebius χ) x = 0 intro I hIq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal FiniteSFactor.OhI:I ∈ FiniteSFactor.fiber 0⊢ FiniteSFactor.outsideWeight S (weightedMoebius χ) I = 0 have hz:=Ideal.absNorm_eq_zero_iff.mp (FiniteSFactor.mem_fiber.mp hI)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal FiniteSFactor.OhI:I ∈ FiniteSFactor.fiber 0hz:I = ⊥⊢ FiniteSFactor.outsideWeight S (weightedMoebius χ) I = 0 change outsideWeight χ S I=0q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal FiniteSFactor.OhI:I ∈ FiniteSFactor.fiber 0hz:I = ⊥⊢ outsideWeight χ S I = 0 rw [hzq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal FiniteSFactor.OhI:I ∈ FiniteSFactor.fiber 0hz:I = ⊥⊢ outsideWeight χ S ⊥ = 0]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)I:Ideal FiniteSFactor.OhI:I ∈ FiniteSFactor.fiber 0hz:I = ⊥⊢ outsideWeight χ S ⊥ = 0 exact outsideWeight_zero χ SAll goals completed! 🐙theorem weightedCoeff_norm_bound {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (n : ℕ) : ‖weightedCoeff χ S n‖≤128*n := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕ⊢ ‖weightedCoeff χ S n‖ ≤ 128 * ↑n by_cases hn : n=0posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:n = 0⊢ ‖weightedCoeff χ S n‖ ≤ 128 * ↑nnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0⊢ ‖weightedCoeff χ S n‖ ≤ 128 * ↑n ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:n = 0⊢ ‖weightedCoeff χ S n‖ ≤ 128 * ↑n subst nposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)⊢ ‖weightedCoeff χ S 0‖ ≤ 128 * ↑0 simpAll goals completed! 🐙 have hn1 : (1:ℝ)≤n:=by exact_mod_cast Nat.one_le_iff_ne_zero.mpr hnnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑n⊢ ‖weightedCoeff χ S n‖ ≤ 128 * ↑n have hc:=DescentFiberCost.finite_ideal_count_real (FiniteSFactor.fiber n) n hn1 (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑n⊢ ∀ I ∈ FiniteSFactor.fiber n, I ≠ ⊥ intro I hI hzq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑nI:Ideal DescentFiberCost.OhI:I ∈ FiniteSFactor.fiber nhz:I = ⊥⊢ False have hh:=FiniteSFactor.mem_fiber.mp hIq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑nI:Ideal DescentFiberCost.OhI:I ∈ FiniteSFactor.fiber nhz:I = ⊥hh:absNorm I = n⊢ False rw [hzq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑nI:Ideal DescentFiberCost.OhI:I ∈ FiniteSFactor.fiber nhz:I = ⊥hh:absNorm ⊥ = n⊢ False] at hhq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑nI:Ideal DescentFiberCost.OhI:I ∈ FiniteSFactor.fiber nhz:I = ⊥hh:absNorm ⊥ = n⊢ False simp only [Ideal.absNorm_bot] at hhq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑nI:Ideal DescentFiberCost.OhI:I ∈ FiniteSFactor.fiber nhz:I = ⊥hh:0 = n⊢ False exact hn hh.symmAll goals completed! 🐙) (byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑n⊢ ∀ I ∈ FiniteSFactor.fiber n, ↑(absNorm I) ≤ ↑n intro I hIq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑nI:Ideal DescentFiberCost.OhI:I ∈ FiniteSFactor.fiber n⊢ ↑(absNorm I) ≤ ↑n exact_mod_cast (FiniteSFactor.mem_fiber.mp hI).leAll goals completed! 🐙)negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑nhc:↑(#(FiniteSFactor.fiber n)) ≤ 128 * ↑n⊢ ‖weightedCoeff χ S n‖ ≤ 128 * ↑n calc _≤∑I∈FiniteSFactor.fiber n,‖outsideWeight χ S I‖:=norm_sum_le _ _ _≤∑I∈FiniteSFactor.fiber n,(1:ℝ):=Finset.sum_le_sum (fun I hI=>outsideWeight_norm_le_one χ S I) _=(FiniteSFactor.fiber n).card:=byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)n:ℕhn:¬n = 0hn1:1 ≤ ↑nhc:↑(#(FiniteSFactor.fiber n)) ≤ 128 * ↑n⊢ ∑ I ∈ FiniteSFactor.fiber n, 1 = ↑(#(FiniteSFactor.fiber n)) simpAll goals completed! 🐙 _≤128*n:=hctheorem weightedCoeff_LSeriesSummable {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (s : ℂ) (hs : 2<s.re) : LSeriesSummable (weightedCoeff χ S) s := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:2 < s.re⊢ LSeriesSummable (weightedCoeff χ S) s apply LSeriesSummable_of_isBigO_rpow hsq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:2 < s.re⊢ weightedCoeff χ S =O[atTop] fun n => ↑n ^ (2 - 1) apply Asymptotics.IsBigO.of_bound 128q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:2 < s.re⊢ ∀ᶠ (x : ℕ) in atTop, ‖weightedCoeff χ S x‖ ≤ 128 * ‖↑x ^ (2 - 1)‖ filter_upwards [] with nq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:2 < s.ren:ℕ⊢ ‖weightedCoeff χ S n‖ ≤ 128 * ‖↑n ^ (2 - 1)‖ simpa only [show (2:ℝ)-1=1 byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)s:ℂhs:2 < s.re⊢ LSeriesSummable (weightedCoeff χ S) s norm_numAll goals completed! 🐙,Real.rpow_one,Real.norm_natCast] using weightedCoeff_norm_bound χ S ntheorem weightedCoeff_hasSum {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (W : ℝ→ℂ) (b Z : ℝ) (hZ : 0<Z) (hW : ∀x,W x≠0→x≤b) (D : ℕ) (hD : b*Z≤D) : HasSum (fun n : ℕ=>weightedCoeff χ S n*W ((n:ℝ)/Z)) (∑I∈outsideIdealsUpTo S D,baseChangeWeight χ I*W ((Ideal.absNorm I:ℝ)/Z)*totientDensity I) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑D⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) have ht (n : ℕ) (hn : n∉Finset.Icc 1 D) : weightedCoeff χ S n*W ((n:ℝ)/Z)=0 := by by_cases hn0 : n=0posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:n = 0⊢ weightedCoeff χ S n * W (↑n / Z) = 0negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:¬n = 0⊢ weightedCoeff χ S n * W (↑n / Z) = 0 ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:n = 0⊢ weightedCoeff χ S n * W (↑n / Z) = 0 subst nposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dhn:0 ∉ Finset.Icc 1 D⊢ weightedCoeff χ S 0 * W (↑0 / Z) = 0 simpAll goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:¬n = 0⊢ weightedCoeff χ S n * W (↑n / Z) = 0 have hnD : D<n := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑D⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) simp only [Finset.mem_Icc] at hnq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn0:¬n = 0hn:¬(1 ≤ n ∧ n ≤ D)⊢ D < n;omeganegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:¬n = 0hnD:D < n⊢ weightedCoeff χ S n * W (↑n / Z) = 0 have hz : W ((n:ℝ)/Z)=0 := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑D⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) by_contra hwq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:¬n = 0hnD:D < nhw:¬W (↑n / Z) = 0⊢ False have hh:=(div_le_iff₀ hZ).mp (hW _ hw)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:¬n = 0hnD:D < nhw:¬W (↑n / Z) = 0hh:↑n ≤ b * Z⊢ False have hl : (D:ℝ)<n:=byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑D⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) exact_mod_cast hnDq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:¬n = 0hnD:D < nhw:¬W (↑n / Z) = 0hh:↑n ≤ b * Zhl:↑D < ↑n⊢ False linarithnegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:¬n = 0hnD:D < nhz:W (↑n / Z) = 0⊢ weightedCoeff χ S n * W (↑n / Z) = 0 rw [hz,negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:¬n = 0hnD:D < nhz:W (↑n / Z) = 0⊢ weightedCoeff χ S n * 0 = 0mul_zeronegq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dn:ℕhn:n ∉ Finset.Icc 1 Dhn0:¬n = 0hnD:D < nhz:W (↑n / Z) = 0⊢ 0 = 0]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) have hh : HasSum (fun n : ℕ=>weightedCoeff χ S n*W ((n:ℝ)/Z)) (∑n∈Finset.Icc 1 D,weightedCoeff χ S n*W ((n:ℝ)/Z)) := hasSum_sum_of_ne_finset_zero htq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0hh:HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z))⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) have he:=outsideIdealSum_eq_outsideCoeff_sum S D (weightedMoebius χ) (fun n=>W ((n:ℝ)/Z))q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0hh:HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z))he:∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z) = ∑ n ∈ Finset.Icc 1 D, FiniteSFactor.outsideCoeff S (weightedMoebius χ) n * W (↑n / Z)⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) change _=(∑n∈Finset.Icc 1 D,weightedCoeff χ S n*W ((n:ℝ)/Z)) at heq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0hh:HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z))he:∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z) = ∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z)⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) rw [←heq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0hh:HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z))he:∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z) = ∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z)⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I)] at hhq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0hh:HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z))he:∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z) = ∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z)⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) convert hh using 1q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0hh:HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z))he:∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z) = ∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z)⊢ ∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I = ∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z) apply Finset.sum_congr rflq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0hh:HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z))he:∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z) = ∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z)⊢ ∀ x ∈ outsideIdealsUpTo S D, baseChangeWeight χ x * W (↑(absNorm x) / Z) * totientDensity x = weightedMoebius χ x * W (↑(absNorm x) / Z) intro I hIq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0hh:HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z))he:∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z) = ∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z)I:Ideal ConcretePrimeRowBridge.OhI:I ∈ outsideIdealsUpTo S D⊢ baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I = weightedMoebius χ I * W (↑(absNorm I) / Z) dsimp only [weightedMoebius]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ n ∉ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z) = 0hh:HasSum (fun n => weightedCoeff χ S n * W (↑n / Z)) (∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z))he:∑ I ∈ outsideIdealsUpTo S D, weightedMoebius χ I * W (↑(absNorm I) / Z) = ∑ n ∈ Finset.Icc 1 D, weightedCoeff χ S n * W (↑n / Z)I:Ideal ConcretePrimeRowBridge.OhI:I ∈ outsideIdealsUpTo S D⊢ baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I = baseChangeWeight χ I * totientDensity I * W (↑(absNorm I) / Z) ringAll goals completed! 🐙theorem ideal_weighted_hasSum {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (W : ℝ→ℂ) (b Z : ℝ) (hZ : 0<Z) (hW : ∀x,W x≠0→x≤b) (D : ℕ) (hD : b*Z≤D) : HasSum (fun I : Ideal ActualEisensteinCubic.O=>outsideWeight χ S I*W ((Ideal.absNorm I:ℝ)/Z)) (∑I∈outsideIdealsUpTo S D,baseChangeWeight χ I*W ((Ideal.absNorm I:ℝ)/Z)*totientDensity I) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑D⊢ HasSum (fun I => outsideWeight χ S I * W (↑(absNorm I) / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) have ht (I : Ideal ActualEisensteinCubic.O) (hI : I∉outsideIdealsUpTo S D) : outsideWeight χ S I*W ((Ideal.absNorm I:ℝ)/Z)=0 := by by_cases hI0 : I=0posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:I = 0⊢ outsideWeight χ S I * W (↑(absNorm I) / Z) = 0negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0⊢ outsideWeight χ S I * W (↑(absNorm I) / Z) = 0 ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:I = 0⊢ outsideWeight χ S I * W (↑(absNorm I) / Z) = 0 rw [hI0,posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:I = 0⊢ outsideWeight χ S 0 * W (↑(absNorm 0) / Z) = 0outsideWeight_zero,posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:I = 0⊢ 0 * W (↑(absNorm 0) / Z) = 0zero_mulposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:I = 0⊢ 0 = 0]All goals completed! 🐙 by_cases hg : ∀P∈S,¬P∣Iposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ I⊢ outsideWeight χ S I * W (↑(absNorm I) / Z) = 0negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:¬∀ P ∈ S, ¬P ∣ I⊢ outsideWeight χ S I * W (↑(absNorm I) / Z) = 0 ·posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ I⊢ outsideWeight χ S I * W (↑(absNorm I) / Z) = 0 have hz : W ((Ideal.absNorm I:ℝ)/Z)=0 := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑D⊢ HasSum (fun I => outsideWeight χ S I * W (↑(absNorm I) / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) by_contra hnq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ Ihn:¬W (↑(absNorm I) / Z) = 0⊢ False apply hIq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ Ihn:¬W (↑(absNorm I) / Z) = 0⊢ I ∈ outsideIdealsUpTo S D refine mem_outsideIdealsUpTo.mpr ⟨?_,?_,hg⟩refine_1q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ Ihn:¬W (↑(absNorm I) / Z) = 0⊢ 1 ≤ absNorm Irefine_2q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ Ihn:¬W (↑(absNorm I) / Z) = 0⊢ absNorm I ≤ D ·refine_1q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ Ihn:¬W (↑(absNorm I) / Z) = 0⊢ 1 ≤ absNorm I exact Nat.one_le_iff_ne_zero.mpr (fun hh=>hI0 (Ideal.absNorm_eq_zero_iff.mp hh))All goals completed! 🐙 ·refine_2q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ Ihn:¬W (↑(absNorm I) / Z) = 0⊢ absNorm I ≤ D exact_mod_cast ((div_le_iff₀ hZ).mp (hW _ hn)).trans hDposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ Ihz:W (↑(absNorm I) / Z) = 0⊢ outsideWeight χ S I * W (↑(absNorm I) / Z) = 0 rw [hz,posq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ Ihz:W (↑(absNorm I) / Z) = 0⊢ outsideWeight χ S I * 0 = 0mul_zeroposq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:∀ P ∈ S, ¬P ∣ Ihz:W (↑(absNorm I) / Z) = 0⊢ 0 = 0]All goals completed! 🐙 ·negq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑DI:Ideal ActualEisensteinCubic.OhI:I ∉ outsideIdealsUpTo S DhI0:¬I = 0hg:¬∀ P ∈ S, ¬P ∣ I⊢ outsideWeight χ S I * W (↑(absNorm I) / Z) = 0 simp [outsideWeight,FiniteSFactor.outsideWeight,hg]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ I ∉ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z) = 0⊢ HasSum (fun I => outsideWeight χ S I * W (↑(absNorm I) / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) have hh : HasSum (fun I : Ideal ActualEisensteinCubic.O=>outsideWeight χ S I*W ((Ideal.absNorm I:ℝ)/Z)) (∑I∈outsideIdealsUpTo S D,outsideWeight χ S I*W ((Ideal.absNorm I:ℝ)/Z)) := hasSum_sum_of_ne_finset_zero htq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ I ∉ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z) = 0hh:HasSum (fun I => outsideWeight χ S I * W (↑(absNorm I) / Z)) (∑ I ∈ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z))⊢ HasSum (fun I => outsideWeight χ S I * W (↑(absNorm I) / Z)) (∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I) convert hh using 1q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ I ∉ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z) = 0hh:HasSum (fun I => outsideWeight χ S I * W (↑(absNorm I) / Z)) (∑ I ∈ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z))⊢ ∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I = ∑ I ∈ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z) apply Finset.sum_congr rflq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ I ∉ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z) = 0hh:HasSum (fun I => outsideWeight χ S I * W (↑(absNorm I) / Z)) (∑ I ∈ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z))⊢ ∀ x ∈ outsideIdealsUpTo S D, baseChangeWeight χ x * W (↑(absNorm x) / Z) * totientDensity x = outsideWeight χ S x * W (↑(absNorm x) / Z) intro I hIq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ I ∉ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z) = 0hh:HasSum (fun I => outsideWeight χ S I * W (↑(absNorm I) / Z)) (∑ I ∈ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z))I:Ideal ConcretePrimeRowBridge.OhI:I ∈ outsideIdealsUpTo S D⊢ baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I = outsideWeight χ S I * W (↑(absNorm I) / Z) simp only [outsideWeight,FiniteSFactor.outsideWeight,ite_eq_left (mem_outsideIdealsUpTo.mp hI).2.2,weightedMoebius]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂb:ℝZ:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑Dht:∀ I ∉ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z) = 0hh:HasSum (fun I => outsideWeight χ S I * W (↑(absNorm I) / Z)) (∑ I ∈ outsideIdealsUpTo S D, outsideWeight χ S I * W (↑(absNorm I) / Z))I:Ideal ConcretePrimeRowBridge.OhI:I ∈ outsideIdealsUpTo S D⊢ baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I = baseChangeWeight χ I * totientDensity I * W (↑(absNorm I) / Z) ringAll goals completed! 🐙endopen scoped BigOperators Classical SchwartzMap ContDiff Topologyopen Filter Asymptotics MeasureTheoryopen ActualEisensteinCubicopen ConcretePrimeRowBridge hiding Oopen ShortDraftHeckeBridgeopen CanonicalQuadraticSieve hiding Oopen SecondPassArithmetic hiding Oopen CanonicalRowCompletionopen InitialMeanSquare CompactMellinBridgedef weightedCompactSum {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (W : ℝ→ℂ) (t : ℝ) : ℂ := ∑'n : ℕ,weightedCoeff χ S n*W ((n:ℝ)*t)theorem weightedCompactSum_hasSum {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (W : ℝ→ℂ) (hW : ∀x,2≤x→W x=0) (t : ℝ) (ht : 0<t) : HasSum (fun n : ℕ=>weightedCoeff χ S n*W ((n:ℝ)*t)) (weightedCompactSum χ S W t) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < t⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n * t)) (weightedCompactSum χ S W t) obtain ⟨N,hN⟩:=exists_nat_gt (2/t)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < tN:ℕhN:2 / t < ↑N⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n * t)) (weightedCompactSum χ S W t) have hz (n : ℕ) (hn : n∉Finset.range N) : weightedCoeff χ S n*W ((n:ℝ)*t)=0 := by have hNn : N≤n:=byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < t⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n * t)) (weightedCompactSum χ S W t) simpa only [Finset.mem_range,not_lt] using hnq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < tN:ℕhN:2 / t < ↑Nn:ℕhn:n ∉ Finset.range NhNn:N ≤ n⊢ weightedCoeff χ S n * W (↑n * t) = 0 have htwo : 2≤(n:ℝ)*t := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < t⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n * t)) (weightedCompactSum χ S W t) have hh:=(div_lt_iff₀ ht).mp hNq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < tN:ℕhN:2 / t < ↑Nn:ℕhn:n ∉ Finset.range NhNn:N ≤ nhh:2 < ↑N * t⊢ 2 ≤ ↑n * t exact hh.le.trans (mul_le_mul_of_nonneg_right (Nat.cast_le.mpr hNn) ht.le)q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < tN:ℕhN:2 / t < ↑Nn:ℕhn:n ∉ Finset.range NhNn:N ≤ nhtwo:2 ≤ ↑n * t⊢ weightedCoeff χ S n * W (↑n * t) = 0 rw [hW _ htwo,q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < tN:ℕhN:2 / t < ↑Nn:ℕhn:n ∉ Finset.range NhNn:N ≤ nhtwo:2 ≤ ↑n * t⊢ weightedCoeff χ S n * 0 = 0mul_zeroq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < tN:ℕhN:2 / t < ↑Nn:ℕhn:n ∉ Finset.range NhNn:N ≤ nhtwo:2 ≤ ↑n * t⊢ 0 = 0]q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:∀ (x : ℝ), 2 ≤ x → W x = 0t:ℝht:0 < tN:ℕhN:2 / t < ↑Nhz:∀ n ∉ Finset.range N, weightedCoeff χ S n * W (↑n * t) = 0⊢ HasSum (fun n => weightedCoeff χ S n * W (↑n * t)) (weightedCompactSum χ S W t) exact (summable_of_ne_finset_zero hz).hasSumAll goals completed! 🐙theorem weightedCompactSum_inv_eq {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (W : ℝ→ℂ) (Z b : ℝ) (hZ : 0<Z) (hW : ∀x,W x≠0→x≤b) (D : ℕ) (hD : b*Z≤D) : weightedCompactSum χ S W Z⁻¹= ∑I∈outsideIdealsUpTo S D,baseChangeWeight χ I*W ((Ideal.absNorm I:ℝ)/Z)*totientDensity I := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂZ:ℝb:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bD:ℕhD:b * Z ≤ ↑D⊢ weightedCompactSum χ S W Z⁻¹ = ∑ I ∈ outsideIdealsUpTo S D, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I simpa only [weightedCompactSum,div_eq_mul_inv] using (weightedCoeff_hasSum χ S W b Z hZ hW D hD).tsum_eqAll goals completed! 🐙theorem weightedCompactSum_eq_ideal_tsum {q : ℕ} (χ : DirichletCharacter ℂ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (W : ℝ→ℂ) (Z b : ℝ) (hZ : 0<Z) (hW : ∀x,W x≠0→x≤b) : weightedCompactSum χ S W Z⁻¹= ∑'I : Ideal ActualEisensteinCubic.O,outsideWeight χ S I*W ((Ideal.absNorm I:ℝ)/Z) := byq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂZ:ℝb:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ b⊢ weightedCompactSum χ S W Z⁻¹ = ∑' (I : Ideal ActualEisensteinCubic.O), outsideWeight χ S I * W (↑(absNorm I) / Z) have hD : b*Z≤(⌈b*Z⌉₊:ℝ):=Nat.le_ceil _q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂZ:ℝb:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bhD:b * Z ≤ ↑⌈b * Z⌉₊⊢ weightedCompactSum χ S W Z⁻¹ = ∑' (I : Ideal ActualEisensteinCubic.O), outsideWeight χ S I * W (↑(absNorm I) / Z) rw [weightedCompactSum_inv_eq χ S W Z b hZ hW _ hD,q:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂZ:ℝb:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bhD:b * Z ≤ ↑⌈b * Z⌉₊⊢ ∑ I ∈ outsideIdealsUpTo S ⌈b * Z⌉₊, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I = ∑' (I : Ideal ActualEisensteinCubic.O), outsideWeight χ S I * W (↑(absNorm I) / Z) (ideal_weighted_hasSum χ S W b Z hZ hW _ hD).tsum_eqq:ℕχ:DirichletCharacter ℂ qS:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂZ:ℝb:ℝhZ:0 < ZhW:∀ (x : ℝ), W x ≠ 0 → x ≤ bhD:b * Z ≤ ↑⌈b * Z⌉₊⊢ ∑ I ∈ outsideIdealsUpTo S ⌈b * Z⌉₊, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I = ∑ I ∈ outsideIdealsUpTo S ⌈b * Z⌉₊, baseChangeWeight χ I * W (↑(absNorm I) / Z) * totientDensity I]All goals completed! 🐙theorem weightedCompactMellin_eq_series {q₀ : ℕ} (χ : DirichletCharacter ℂ q₀) (S : Finset (Ideal ActualEisensteinCubic.O)) (W : ℝ→ℂ) (hW : ContDiff ℝ ∞ W) (hs : ∀x,x≤1 ∨ 2≤x→W x=0) (s : ℂ) (hRe : 2<s.re) : mellin (fun Z : ℝ=>weightedCompactSum χ S W Z⁻¹) (-s)= mellin W s*LSeries (weightedCoeff χ S) s := byq₀:ℕχ:DirichletCharacter ℂ q₀S:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:ContDiff ℝ ∞ Whs:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0s:ℂhRe:2 < s.re⊢ mellin (fun Z => weightedCompactSum χ S W Z⁻¹) (-s) = mellin W s * L (weightedCoeff χ S) s have hls:=weightedCoeff_LSeriesSummable χ S s hReq₀:ℕχ:DirichletCharacter ℂ q₀S:Finset (Ideal ActualEisensteinCubic.O)W:ℝ → ℂhW:ContDiff ℝ ∞ Whs:∀ (x : ℝ), x ≤ 1 ∨ 2 ≤ x → W x = 0s:ℂhRe:2 < s.rehls:LSeriesSummable (weightedCoeff χ S) s⊢ mellin (fun Z => weightedCompactSum χ S W Z⁻¹) (-s) = mellin W s * L (weightedCoeff χ S) s exact mellin_weighted_sum (weightedCoeff χ S) W (weightedCompactSum χ S W) s (weightedCoeff_zero χ S) (weightedCompactSum_hasSum χ S W (fun x hx=>hs x (Or.inr hx))) (weighted_term_integrable _ (weightedCoeff_zero χ S) W s (compact_weight_mellin_convergent W hW hs s)) (weighted_terms_fubini _ (weightedCoeff_zero χ S) W s hls) hlsAll goals completed! 🐙end SixthPowerAverageendend OAI