1. OAI
  2. NumberTheory
  3. DirichletL
  4. GaussSum
  5. MixedConversion
import OAI.NumberTheory.DirichletL.GaussSum.ActiveConductor import OAI.NumberTheory.DirichletL.GaussSum.CubicTracenamespace OAInoncomputable sectionopen scoped BigOperatorsopen MulChar AddCharopen scoped BigOperatorsopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen MeasureTheory Realopen scoped FourierTransform SchwartzMapopen Finset Complexopen scoped Classicalopen scoped Classicalopen Filter Real Asymptoticsopen ActualEisensteinCubicopen Filteropen ActualEisensteinCubic RationalPrimeExtraction ShortDraftLatticeCountopen ActualEisensteinCubic ShortDraftLatticeCountopen Filteropen scoped Topologyopen EisensteinEmbedding ConcreteTraceCRT ActualEisensteinCubicopen MulChar AddCharopen Filter Asymptoticsopen scoped LSeries.notation ArithmeticFunction.Moebiusopen Filteropen MulChar AddCharopen MulChar AddCharopen scoped LSeries.notation ArithmeticFunction.Moebiusopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptoticsopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Filter Asymptoticsopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptotics Ideal NumberFieldopen Filteropen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen MeasureTheory Realopen scoped ContDiff FourierTransform SchwartzMapopen scoped BigOperators Classicalopen scoped BigOperators Classicalopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classicalopen scoped BigOperators Classicalnamespace MixedGaussConversionabbrev O := ActualEisensteinCubic.Oopen ActualEisensteinCubic ConcreteTraceCRT FiniteGaussPhasedef localGauss (p : O) (hp : p ≠ 0) [ (Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) (j : ℕ) : ℂ := ConcreteBreveE.normalizedTraceGauss p hp (canonicalSextic (Ideal.span {p}) hg ^ j)def localCoefficient (p : O) (hp : p ≠ 0) [ (Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) : ℂ := star (angularFactor p) * localGauss p hp hg 2def localG (p : O) (hp : p ≠ 0) [ (Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) : ℂ := breveLocalG (Ideal.span {p}) hg p rfl hptheorem norm_localGauss (p : O) (hp : p ≠ 0) [ (Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) (hchar : ringChar (O ⧸ Ideal.span {p}) ≠ 2) (j : ℕ) (hj0 : j ≠ 0) (hj6 : j < 6) : ‖localGauss p hp hg j‖ = 1 := p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2j:ℕhj0:j ≠ 0hj6:j < 6⊢ ‖localGauss p hp hg j‖ = 1 p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2j:ℕhj0:j ≠ 0hj6:j < 6q:Unit → O := fun x => p⊢ ‖localGauss p hp hg j‖ = 1 p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2j:ℕhj0:j ≠ 0hj6:j < 6q:Unit → O := fun x => phcop:Pairwise (Function.onFun IsCoprime fun i => span {q i})⊢ ‖localGauss p hp hg j‖ = 1 p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2j:ℕhj0:j ≠ 0hj6:j < 6q:Unit → O := fun x => phcop:Pairwise (Function.onFun IsCoprime fun i => span {q i})h:‖canonicalProductGauss q ⋯ hcop ⋯ fun x => j‖ = 1⊢ ‖localGauss p hp hg j‖ = 1 p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2j:ℕhj0:j ≠ 0hj6:j < 6q:Unit → O := fun x => phcop:Pairwise (Function.onFun IsCoprime fun i => span {q i})h:‖(∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {q i}) hg) ((Ideal.Quotient.mk (span {q i})) (q k))) ^ j * ∏ i, ConcreteBreveE.normalizedTraceGauss (q i) hp (canonicalSextic (span {q i}) hg ^ j)‖ = 1⊢ ‖localGauss p hp hg j‖ = 1 All goals completed! 🐙theorem canonicalSextic_fifth_eq_inverse (p : O) [(Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) : canonicalSextic (Ideal.span {p}) hg ^ 5 = (canonicalSextic (Ideal.span {p}) hg)⁻¹ := p:Oinst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}⊢ canonicalSextic (span {p}) hg ^ 5 = (canonicalSextic (span {p}) hg)⁻¹ p:Oinst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}⊢ ∀ (x : ActualEisensteinCubic.O ⧸ span {p}), (canonicalSextic (span {p}) hg ^ 5) x = (canonicalSextic (span {p}) hg)⁻¹ x p:Oinst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}x:ActualEisensteinCubic.O ⧸ span {p}⊢ (canonicalSextic (span {p}) hg ^ 5) x = (canonicalSextic (span {p}) hg)⁻¹ x p:Oinst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}a:ActualEisensteinCubic.O⊢ (canonicalSextic (span {p}) hg ^ 5) ((Ideal.Quotient.mk (span {p})) a) = (canonicalSextic (span {p}) hg)⁻¹ ((Ideal.Quotient.mk (span {p})) a) p:Oinst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}a:ActualEisensteinCubic.O⊢ (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) a) ^ 5 = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) a) * (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) a) ^ 4 All goals completed! 🐙theorem localGauss_five_eq (p : O) (hp : p ≠ 0) [(Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) : localGauss p hp hg 5 = breveGammaMinus1 (Ideal.span {p}) hg p rfl hp := p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}⊢ localGauss p hp hg 5 = breveGammaMinus1 (span {p}) hg p ⋯ hp p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}⊢ ConcreteBreveE.normalizedTraceGauss p hp (canonicalSextic (span {p}) hg)⁻¹ = breveGammaMinus1 (span {p}) hg p ⋯ hp All goals completed! 🐙theorem local_sign_conversion (p : O) (hp : p ≠ 0) [(Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) (hchar : ringChar (O ⧸ Ideal.span {p}) ≠ 2) (hprimary : lambda ^ 2 ∣ p - 1) : (-localGauss p hp hg 1) * star (localG p hp hg) = star (localCoefficient p hp hg) ∧ (-localGauss p hp hg 5) * localG p hp hg = canonicalSextic (Ideal.span {p}) hg (Ideal.Quotient.mk (Ideal.span {p}) (-1 : O)) * localCoefficient p hp hg := p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1⊢ -localGauss p hp hg 1 * star (localG p hp hg) = star (localCoefficient p hp hg) ∧ -localGauss p hp hg 5 * localG p hp hg = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * localCoefficient p hp hg p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:have alpha := eisEmbedding p / ↑‖eisEmbedding p‖; have g1 := breveGamma1 (span {p}) hg p ⋯ hp; have g2 := breveGamma2 (span {p}) hg p ⋯ hp; have gm := breveGammaMinus1 (span {p}) hg p ⋯ hp; have G := breveLocalG (span {p}) hg p ⋯ hp; have t := (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) 1); have eps := (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)); -star g1 * G * t = star alpha * g2 * t ∧ -gm * G * t = eps * (star alpha * g2) * t ∧ -g1 * star G * t⁻¹ = alpha * star g2 * t⁻¹ ∧ -star gm * star G * t⁻¹ = star eps * (alpha * star g2) * t⁻¹⊢ -localGauss p hp hg 1 * star (localG p hp hg) = star (localCoefficient p hp hg) ∧ -localGauss p hp hg 5 * localG p hp hg = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * localCoefficient p hp hg p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:-star (breveGamma1 (span {p}) hg p ⋯ hp) * breveLocalG (span {p}) hg p ⋯ hp * (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) 1) = star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp * (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) 1) ∧ -breveGammaMinus1 (span {p}) hg p ⋯ hp * breveLocalG (span {p}) hg p ⋯ hp * (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) 1) = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * (star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp) * (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) 1) ∧ -breveGamma1 (span {p}) hg p ⋯ hp * star (breveLocalG (span {p}) hg p ⋯ hp) * ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) 1))⁻¹ = eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp) * ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) 1))⁻¹ ∧ -star (breveGammaMinus1 (span {p}) hg p ⋯ hp) * star (breveLocalG (span {p}) hg p ⋯ hp) * ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) 1))⁻¹ = star ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1))) * (eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp)) * ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) 1))⁻¹⊢ -localGauss p hp hg 1 * star (localG p hp hg) = star (localCoefficient p hp hg) ∧ -localGauss p hp hg 5 * localG p hp hg = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * localCoefficient p hp hg p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:-star (breveGamma1 (span {p}) hg p ⋯ hp) * breveLocalG (span {p}) hg p ⋯ hp = star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp ∧ -breveGammaMinus1 (span {p}) hg p ⋯ hp * breveLocalG (span {p}) hg p ⋯ hp = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * (star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp) ∧ -breveGamma1 (span {p}) hg p ⋯ hp * star (breveLocalG (span {p}) hg p ⋯ hp) = eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp) ∧ -star (breveGammaMinus1 (span {p}) hg p ⋯ hp) * star (breveLocalG (span {p}) hg p ⋯ hp) = star ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1))) * (eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp))⊢ -localGauss p hp hg 1 * star (localG p hp hg) = star (localCoefficient p hp hg) ∧ -localGauss p hp hg 5 * localG p hp hg = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * localCoefficient p hp hg p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:-star (breveGamma1 (span {p}) hg p ⋯ hp) * breveLocalG (span {p}) hg p ⋯ hp = star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp ∧ -breveGammaMinus1 (span {p}) hg p ⋯ hp * breveLocalG (span {p}) hg p ⋯ hp = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * (star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp) ∧ -breveGamma1 (span {p}) hg p ⋯ hp * star (breveLocalG (span {p}) hg p ⋯ hp) = eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp) ∧ -star (breveGammaMinus1 (span {p}) hg p ⋯ hp) * star (breveLocalG (span {p}) hg p ⋯ hp) = star ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1))) * (eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp))⊢ -localGauss p hp hg 1 * star (localG p hp hg) = star (localCoefficient p hp hg)p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:-star (breveGamma1 (span {p}) hg p ⋯ hp) * breveLocalG (span {p}) hg p ⋯ hp = star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp ∧ -breveGammaMinus1 (span {p}) hg p ⋯ hp * breveLocalG (span {p}) hg p ⋯ hp = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * (star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp) ∧ -breveGamma1 (span {p}) hg p ⋯ hp * star (breveLocalG (span {p}) hg p ⋯ hp) = eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp) ∧ -star (breveGammaMinus1 (span {p}) hg p ⋯ hp) * star (breveLocalG (span {p}) hg p ⋯ hp) = star ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1))) * (eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp))⊢ -localGauss p hp hg 5 * localG p hp hg = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * localCoefficient p hp hg p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:-star (breveGamma1 (span {p}) hg p ⋯ hp) * breveLocalG (span {p}) hg p ⋯ hp = star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp ∧ -breveGammaMinus1 (span {p}) hg p ⋯ hp * breveLocalG (span {p}) hg p ⋯ hp = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * (star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp) ∧ -breveGamma1 (span {p}) hg p ⋯ hp * star (breveLocalG (span {p}) hg p ⋯ hp) = eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp) ∧ -star (breveGammaMinus1 (span {p}) hg p ⋯ hp) * star (breveLocalG (span {p}) hg p ⋯ hp) = star ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1))) * (eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp))⊢ -localGauss p hp hg 1 * star (localG p hp hg) = star (localCoefficient p hp hg) All goals completed! 🐙 p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:-star (breveGamma1 (span {p}) hg p ⋯ hp) * breveLocalG (span {p}) hg p ⋯ hp = star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp ∧ -breveGammaMinus1 (span {p}) hg p ⋯ hp * breveLocalG (span {p}) hg p ⋯ hp = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * (star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp) ∧ -breveGamma1 (span {p}) hg p ⋯ hp * star (breveLocalG (span {p}) hg p ⋯ hp) = eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp) ∧ -star (breveGammaMinus1 (span {p}) hg p ⋯ hp) * star (breveLocalG (span {p}) hg p ⋯ hp) = star ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1))) * (eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp))⊢ -localGauss p hp hg 5 * localG p hp hg = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * localCoefficient p hp hg p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:-star (breveGamma1 (span {p}) hg p ⋯ hp) * breveLocalG (span {p}) hg p ⋯ hp = star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp ∧ -breveGammaMinus1 (span {p}) hg p ⋯ hp * breveLocalG (span {p}) hg p ⋯ hp = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * (star (eisEmbedding p / ↑‖eisEmbedding p‖) * breveGamma2 (span {p}) hg p ⋯ hp) ∧ -breveGamma1 (span {p}) hg p ⋯ hp * star (breveLocalG (span {p}) hg p ⋯ hp) = eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp) ∧ -star (breveGammaMinus1 (span {p}) hg p ⋯ hp) * star (breveLocalG (span {p}) hg p ⋯ hp) = star ((canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1))) * (eisEmbedding p / ↑‖eisEmbedding p‖ * star (breveGamma2 (span {p}) hg p ⋯ hp))⊢ -breveGammaMinus1 (span {p}) hg p ⋯ hp * localG p hp hg = (canonicalSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) (-1)) * localCoefficient p hp hg All goals completed! 🐙theorem norm_localG (p : O) (hp : p ≠ 0) [(Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) (hchar : ringChar (O ⧸ Ideal.span {p}) ≠ 2) (hprimary : lambda ^ 2 ∣ p - 1) : ‖localG p hp hg‖ = 1 := p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1⊢ ‖localG p hp hg‖ = 1 p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:‖-localGauss p hp hg 1 * star (localG p hp hg)‖ = ‖star (localCoefficient p hp hg)‖⊢ ‖localG p hp hg‖ = 1 p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:‖localGauss p hp hg 1‖ * ‖localG p hp hg‖ = ‖angularFactor p‖ * ‖localGauss p hp hg 2‖⊢ ‖localG p hp hg‖ = 1 p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1h:‖localG p hp hg‖ = 1⊢ ‖localG p hp hg‖ = 1 All goals completed! 🐙def convertedLocal (p : O) (hp : p ≠ 0) [(Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) (inverse : Bool) : ℂ := if inverse then (canonicalSextic (Ideal.span {p}) hg (Ideal.Quotient.mk (Ideal.span {p}) (-1 : O)) * localCoefficient p hp hg) / localG p hp hg else star (localCoefficient p hp hg) / star (localG p hp hg)theorem neg_localGauss_eq_converted (p : O) (hp : p ≠ 0) [(Ideal.span {p}).IsMaximal] (hg : lambda ∉ Ideal.span {p}) (hchar : ringChar (O ⧸ Ideal.span {p}) ≠ 2) (hprimary : lambda ^ 2 ∣ p - 1) (inverse : Bool) : -localGauss p hp hg (if inverse then 5 else 1) = convertedLocal p hp hg inverse := p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1inverse:Bool⊢ -localGauss p hp hg (if inverse = true then 5 else 1) = convertedLocal p hp hg inverse p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1inverse:BoolhG:localG p hp hg ≠ 0⊢ -localGauss p hp hg (if inverse = true then 5 else 1) = convertedLocal p hp hg inverse p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1hG:localG p hp hg ≠ 0⊢ -localGauss p hp hg (if false = true then 5 else 1) = convertedLocal p hp hg falsep:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1hG:localG p hp hg ≠ 0⊢ -localGauss p hp hg (if true = true then 5 else 1) = convertedLocal p hp hg true p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1hG:localG p hp hg ≠ 0⊢ -localGauss p hp hg (if false = true then 5 else 1) = convertedLocal p hp hg false All goals completed! 🐙 p:Ohp:p ≠ 0inst✝:(span {p}).IsMaximalhg:lambda ∉ span {p}hchar:ringChar (O ⧸ span {p}) ≠ 2hprimary:lambda ^ 2 ∣ p - 1hG:localG p hp hg ≠ 0⊢ -localGauss p hp hg (if true = true then 5 else 1) = convertedLocal p hp hg true All goals completed! 🐙theorem moebius_mixed_gauss_conversion {ι : Type*} [Fintype ι] (p : ι → O) (hp : ∀ i, p i ≠ 0) [∀ i, (Ideal.span {p i}).IsMaximal] (hcop : Pairwise (Function.onFun IsCoprime (fun i => Ideal.span {p i}))) (hgood : ∀ i, lambda ∉ Ideal.span {p i}) (hchar : ∀ i, ringChar (O ⧸ Ideal.span {p i}) ≠ 2) (hprimary : ∀ i, lambda ^ 2 ∣ p i - 1) (inverse : ι → Bool) : (UniqueFactorizationMonoid.moebius (Ideal.span {∏ i, p i}) : ℂ) * canonicalProductGauss p hp hcop hgood (fun i => if inverse i then 5 else 1) = (∏ i, ∏ k ∈ Finset.univ.erase i, (canonicalSextic (Ideal.span {p i}) (hgood i) ^ (if inverse i then 5 else 1)) (Ideal.Quotient.mk (Ideal.span {p i}) (p k))) * ∏ i, convertedLocal (p i) (hp i) (hgood i) (inverse i) := ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1inverse:ι → Bool⊢ (↑(moebius (span {∏ i, p i})) * canonicalProductGauss p hp hcop hgood fun i => if inverse i = true then 5 else 1) = (∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ∏ i, convertedLocal (p i) ⋯ ⋯ (inverse i) ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1inverse:ι → Bool⊢ (-1) ^ Fintype.card ι * ((∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ∏ i, ConcreteBreveE.normalizedTraceGauss (p i) ⋯ (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1)) = (∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ∏ i, convertedLocal (p i) ⋯ ⋯ (inverse i) ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1inverse:ι → Boolhprod:(-1) ^ Fintype.card ι * ∏ i, localGauss (p i) ⋯ ⋯ (if inverse i = true then 5 else 1) = ∏ i, convertedLocal (p i) ⋯ ⋯ (inverse i)⊢ (-1) ^ Fintype.card ι * ((∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ∏ i, ConcreteBreveE.normalizedTraceGauss (p i) ⋯ (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1)) = (∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ∏ i, convertedLocal (p i) ⋯ ⋯ (inverse i) calc _ = (∏ i, ∏ k ∈ Finset.univ.erase i, (canonicalSextic (Ideal.span {p i}) (hgood i) ^ (if inverse i then 5 else 1)) (Ideal.Quotient.mk (Ideal.span {p i}) (p k))) * ((-1 : ℂ) ^ Fintype.card ι * ∏ i, localGauss (p i) (hp i) (hgood i) (if inverse i then 5 else 1)) := ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1inverse:ι → Boolhprod:(-1) ^ Fintype.card ι * ∏ i, localGauss (p i) ⋯ ⋯ (if inverse i = true then 5 else 1) = ∏ i, convertedLocal (p i) ⋯ ⋯ (inverse i)⊢ (-1) ^ Fintype.card ι * ((∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ∏ i, ConcreteBreveE.normalizedTraceGauss (p i) ⋯ (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1)) = (∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ((-1) ^ Fintype.card ι * ∏ i, localGauss (p i) ⋯ ⋯ (if inverse i = true then 5 else 1)) ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1inverse:ι → Boolhprod:(-1) ^ Fintype.card ι * ∏ i, localGauss (p i) ⋯ ⋯ (if inverse i = true then 5 else 1) = ∏ i, convertedLocal (p i) ⋯ ⋯ (inverse i)⊢ (-1) ^ Fintype.card ι * ((∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ∏ i, ConcreteBreveE.normalizedTraceGauss (p i) ⋯ (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1)) = (∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ((-1) ^ Fintype.card ι * ∏ i, ConcreteBreveE.normalizedTraceGauss (p i) ⋯ (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1)) All goals completed! 🐙 _ = _ := ι:Type u_1inst✝¹:Fintype ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhcop:Pairwise (Function.onFun IsCoprime fun i => span {p i})hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1inverse:ι → Boolhprod:(-1) ^ Fintype.card ι * ∏ i, localGauss (p i) ⋯ ⋯ (if inverse i = true then 5 else 1) = ∏ i, convertedLocal (p i) ⋯ ⋯ (inverse i)⊢ (∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ((-1) ^ Fintype.card ι * ∏ i, localGauss (p i) ⋯ ⋯ (if inverse i = true then 5 else 1)) = (∏ i, ∏ k ∈ univ.erase i, (canonicalSextic (span {p i}) ⋯ ^ if inverse i = true then 5 else 1) ((Ideal.Quotient.mk (span {p i})) (p k))) * ∏ i, convertedLocal (p i) ⋯ ⋯ (inverse i) All goals completed! 🐙end MixedGaussConversionopen scoped BigOperators Classical SchwartzMap ContDiffnamespace GaussGeneratorTransportopen ActualEisensteinCubic ConcreteTraceCRT EisensteinSchwartzPoisson FiniteGaussPhaseopen MixedGaussConversiontheorem pair_moebius_eq_active {ι : Type*} [DecidableEq ι] (p : ι → O) [∀ i, (Ideal.span {p i}).IsMaximal] (hinj : Function.Injective (fun i => Ideal.span {p i})) (S T : Finset ι) : (UniqueFactorizationMonoid.moebius (∏ i ∈ S, Ideal.span {p i}) : ℂ) * (UniqueFactorizationMonoid.moebius (∏ i ∈ T, Ideal.span {p i}) : ℂ) = (UniqueFactorizationMonoid.moebius (Ideal.span {∏ i : activeSupport S T, p i.val}) : ℂ) := ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ι⊢ ↑(moebius (∏ i ∈ S, span {p i})) * ↑(moebius (∏ i ∈ T, span {p i})) = ↑(moebius (span {∏ i, p ↑i})) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})⊢ ↑(moebius (∏ i ∈ S, span {p i})) * ↑(moebius (∏ i ∈ T, span {p i})) = ↑(moebius (span {∏ i, p ↑i})) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})hcop:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T))⊢ ↑(moebius (∏ i ∈ S, span {p i})) * ↑(moebius (∏ i ∈ T, span {p i})) = ↑(moebius (span {∏ i, p ↑i})) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})hcop:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T))⊢ (-1) ^ (#S + #T) = (-1) ^ Fintype.card ↥(activeSupport S T) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})hcop:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T))hd:Disjoint (S \ T) (T \ S)⊢ (-1) ^ (#S + #T) = (-1) ^ Fintype.card ↥(activeSupport S T) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})hcop:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T))hd:Disjoint (S \ T) (T \ S)ha:Fintype.card ↥(activeSupport S T) = #(S \ T) + #(T \ S)⊢ (-1) ^ (#S + #T) = (-1) ^ Fintype.card ↥(activeSupport S T) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})hcop:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T))hd:Disjoint (S \ T) (T \ S)ha:Fintype.card ↥(activeSupport S T) = #(S \ T) + #(T \ S)hs:#(S \ T) + #(S ∩ T) = #S⊢ (-1) ^ (#S + #T) = (-1) ^ Fintype.card ↥(activeSupport S T) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})hcop:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T))hd:Disjoint (S \ T) (T \ S)ha:Fintype.card ↥(activeSupport S T) = #(S \ T) + #(T \ S)hs:#(S \ T) + #(S ∩ T) = #Sht:#(T \ S) + #(T ∩ S) = #T⊢ (-1) ^ (#S + #T) = (-1) ^ Fintype.card ↥(activeSupport S T) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})hcop:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T))hd:Disjoint (S \ T) (T \ S)ha:Fintype.card ↥(activeSupport S T) = #(S \ T) + #(T \ S)hs:#(S \ T) + #(S ∩ T) = #Sht:#(T \ S) + #(S ∩ T) = #T⊢ (-1) ^ (#S + #T) = (-1) ^ Fintype.card ↥(activeSupport S T) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})hcop:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T))hd:Disjoint (S \ T) (T \ S)ha:Fintype.card ↥(activeSupport S T) = #(S \ T) + #(T \ S)hs:#(S \ T) + #(S ∩ T) = #Sht:#(T \ S) + #(S ∩ T) = #Thcard:#S + #T = Fintype.card ↥(activeSupport S T) + 2 * #(S ∩ T)⊢ (-1) ^ (#S + #T) = (-1) ^ Fintype.card ↥(activeSupport S T) ι:Type u_1inst✝¹:DecidableEq ιp:ι → Oinst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}S:Finset ιT:Finset ιhprime:∀ (i : ι), Prime (span {p i})hcop:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T))hd:Disjoint (S \ T) (T \ S)ha:Fintype.card ↥(activeSupport S T) = #(S \ T) + #(T \ S)hs:#(S \ T) + #(S ∩ T) = #Sht:#(T \ S) + #(S ∩ T) = #Thcard:#S + #T = Fintype.card ↥(activeSupport S T) + 2 * #(S ∩ T)⊢ (-1) ^ Fintype.card ↥(activeSupport S T) * ((-1) ^ 2) ^ #(S ∩ T) = (-1) ^ Fintype.card ↥(activeSupport S T) All goals completed! 🐙def activeConvertedGauss {ι : Type*} [DecidableEq ι] (p : ι → O) (hp : ∀ i, p i ≠ 0) [∀ i, (Ideal.span {p i}).IsMaximal] (hgood : ∀ i, lambda ∉ Ideal.span {p i}) (S T : Finset ι) : ℂ := (∏ i : activeSupport S T, ∏ k ∈ @Finset.erase (activeSupport S T) (fun a b => Classical.propDecidable (a = b)) Finset.univ i, (canonicalSextic (Ideal.span {p i.val}) (hgood i.val) ^ activeExponent S T i) (Ideal.Quotient.mk (Ideal.span {p i.val}) (p k.val))) * ∏ i : activeSupport S T, convertedLocal (p i.val) (hp i.val) (hgood i.val) (decide (i.val ∈ S \ T))def activePairDualSeries {ι : Type*} [DecidableEq ι] (p : ι → O) [∀ i, (Ideal.span {p i}).IsMaximal] (hgood : ∀ i, lambda ∉ Ideal.span {p i}) (S T : Finset ι) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) : ℂ := let row := finiteSexticRow (activePrimes (fun i => Ideal.span {p i}) S T) (fun i => hgood i.val) (activeExponent S T) let n := ∏ i : activeSupport S T, p i.val ∑ E ∈ (S ∩ T).powerset, let d := primeSubsetGenerator (fun i => Ideal.span {p i}) E ((UniqueFactorizationMonoid.moebius (∏ i ∈ E, Ideal.span {p i}) : ℂ) * row d / (‖eisEmbedding d‖ ^ 2 : ℝ)) * ∑' h : O, star (row h) * paperRadialFourier W (scale * ‖eisEmbedding h‖ ^ 2 / (‖eisEmbedding d‖ ^ 2 * ‖eisEmbedding n‖ ^ 2))def convertedPairPoissonKernel {ι : Type*} [DecidableEq ι] (p : ι → O) (hp : ∀ i, p i ≠ 0) [∀ i, (Ideal.span {p i}).IsMaximal] (hgood : ∀ i, lambda ∉ Ideal.span {p i}) (S T : Finset ι) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) : ℂ := ((scale : ℂ) / (‖eisEmbedding (∏ i : activeSupport S T, p i.val)‖ : ℂ)) * activeConvertedGauss p hp hgood S T * activePairDualSeries p hgood S T W scaletheorem moebius_squarefreePairPoissonKernel_conversion {ι : Type*} [DecidableEq ι] (p : ι → O) (hp : ∀ i, p i ≠ 0) [∀ i, (Ideal.span {p i}).IsMaximal] (hinj : Function.Injective (fun i => Ideal.span {p i})) (hgood : ∀ i, lambda ∉ Ideal.span {p i}) (hchar : ∀ i, ringChar (O ⧸ Ideal.span {p i}) ≠ 2) (hprimary : ∀ i, lambda ^ 2 ∣ p i - 1) (S T : Finset ι) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) : ((UniqueFactorizationMonoid.moebius (∏ i ∈ S, Ideal.span {p i}) : ℂ) * (UniqueFactorizationMonoid.moebius (∏ i ∈ T, Ideal.span {p i}) : ℂ)) * squarefreePairPoissonKernel (fun i => Ideal.span {p i}) hinj hgood S T W scale = convertedPairPoissonKernel p hp hgood S T W scale := ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝ⊢ ↑(moebius (∏ i ∈ S, span {p i})) * ↑(moebius (∏ i ∈ T, span {p i})) * squarefreePairPoissonKernel (fun i => span {p i}) hinj hgood S T W scale = convertedPairPoissonKernel p hp hgood S T W scale ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝq:↥(activeSupport S T) → O := fun i => p ↑i⊢ ↑(moebius (∏ i ∈ S, span {p i})) * ↑(moebius (∏ i ∈ T, span {p i})) * squarefreePairPoissonKernel (fun i => span {p i}) hinj hgood S T W scale = convertedPairPoissonKernel p hp hgood S T W scale ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝq:↥(activeSupport S T) → O := fun i => p ↑ihQ:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T)) := ···⊢ ↑(moebius (∏ i ∈ S, span {p i})) * ↑(moebius (∏ i ∈ T, span {p i})) * squarefreePairPoissonKernel (fun i => span {p i}) hinj hgood S T W scale = convertedPairPoissonKernel p hp hgood S T W scale ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝq:↥(activeSupport S T) → O := fun i => p ↑ihQ:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T)) := ···hg:↑(moebius (span {∏ i, q i})) * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T) = activeConvertedGauss p hp hgood S T⊢ ↑(moebius (∏ i ∈ S, span {p i})) * ↑(moebius (∏ i ∈ T, span {p i})) * squarefreePairPoissonKernel (fun i => span {p i}) hinj hgood S T W scale = convertedPairPoissonKernel p hp hgood S T W scale ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝq:↥(activeSupport S T) → O := fun i => p ↑ihQ:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T)) := ···hg:↑(moebius (span {∏ i, q i})) * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T) = activeConvertedGauss p hp hgood S T⊢ ↑(moebius (span {∏ i, p ↑i})) * squarefreePairProductPoissonKernel p hp hinj hgood S T W scale = convertedPairPoissonKernel p hp hgood S T W scale ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝq:↥(activeSupport S T) → O := fun i => p ↑ihQ:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T)) := ···hg:↑(moebius (span {∏ i, q i})) * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T) = activeConvertedGauss p hp hgood S T⊢ ↑(moebius (span {∏ i, q i})) * (↑scale * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T) / ↑‖eisEmbedding (∏ i, q i)‖ * activePairDualSeries p hgood S T W scale) = convertedPairPoissonKernel p hp hgood S T W scale calc _ = ((scale : ℂ) / (‖eisEmbedding (∏ i, q i)‖ : ℂ)) * ((UniqueFactorizationMonoid.moebius (Ideal.span {∏ i, q i}) : ℂ) * canonicalProductGauss q (fun i => hp i.val) hQ (fun i => hgood i.val) (activeExponent S T)) * activePairDualSeries p hgood S T W scale := ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝq:↥(activeSupport S T) → O := fun i => p ↑ihQ:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T)) := ···hg:↑(moebius (span {∏ i, q i})) * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T) = activeConvertedGauss p hp hgood S T⊢ ↑(moebius (span {∏ i, q i})) * (↑scale * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T) / ↑‖eisEmbedding (∏ i, q i)‖ * activePairDualSeries p hgood S T W scale) = ↑scale / ↑‖eisEmbedding (∏ i, q i)‖ * (↑(moebius (span {∏ i, q i})) * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T)) * activePairDualSeries p hgood S T W scale All goals completed! 🐙 _ = _ := ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝq:↥(activeSupport S T) → O := fun i => p ↑ihQ:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T)) := ···hg:↑(moebius (span {∏ i, q i})) * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T) = activeConvertedGauss p hp hgood S T⊢ ↑scale / ↑‖eisEmbedding (∏ i, q i)‖ * (↑(moebius (span {∏ i, q i})) * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T)) * activePairDualSeries p hgood S T W scale = convertedPairPoissonKernel p hp hgood S T W scale ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝq:↥(activeSupport S T) → O := fun i => p ↑ihQ:Pairwise (Function.onFun IsCoprime (activePrimes (fun i => span {p i}) S T)) := ···hg:↑(moebius (span {∏ i, q i})) * canonicalProductGauss q ⋯ hQ ⋯ (activeExponent S T) = activeConvertedGauss p hp hgood S T⊢ ↑scale / ↑‖eisEmbedding (∏ i, q i)‖ * activeConvertedGauss p hp hgood S T * activePairDualSeries p hgood S T W scale = convertedPairPoissonKernel p hp hgood S T W scale; All goals completed! 🐙theorem moebius_pair_radial_poisson_converted {ι : Type*} [DecidableEq ι] (p : ι → O) (hp : ∀ i, p i ≠ 0) [∀ i, (Ideal.span {p i}).IsMaximal] (hinj : Function.Injective (fun i => Ideal.span {p i})) (hgood : ∀ i, lambda ∉ Ideal.span {p i}) (hchar : ∀ i, ringChar (O ⧸ Ideal.span {p i}) ≠ 2) (hprimary : ∀ i, lambda ^ 2 ∣ p i - 1) (S T : Finset ι) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) (hscale : 0 < scale) : ((UniqueFactorizationMonoid.moebius (∏ i ∈ S, Ideal.span {p i}) : ℂ) * (UniqueFactorizationMonoid.moebius (∏ i ∈ T, Ideal.span {p i}) : ℂ)) * (∑' z : O, (star (finiteSquarefreeRow (fun i => Ideal.span {p i}) hgood S z) * finiteSquarefreeRow (fun i => Ideal.span {p i}) hgood T z) * W (‖eisEmbedding z‖ ^ 2 / scale)) = convertedPairPoissonKernel p hp hgood S T W scale := ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ↑(moebius (∏ i ∈ S, span {p i})) * ↑(moebius (∏ i ∈ T, span {p i})) * ∑' (z : O), star (finiteSquarefreeRow (fun i => span {p i}) hgood S z) * finiteSquarefreeRow (fun i => span {p i}) hgood T z * W (‖eisEmbedding z‖ ^ 2 / scale) = convertedPairPoissonKernel p hp hgood S T W scale ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0inst✝:∀ (i : ι), (span {p i}).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ span {p i}hchar:∀ (i : ι), ringChar (O ⧸ span {p i}) ≠ 2hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ↑(moebius (∏ i ∈ S, span {p i})) * ↑(moebius (∏ i ∈ T, span {p i})) * squarefreePairPoissonKernel (fun i => span {p i}) hinj hgood S T W scale = convertedPairPoissonKernel p hp hgood S T W scale All goals completed! 🐙theorem moebius_pair_kernel_conversion_of_generators {ι : Type*} [DecidableEq ι] (P : ι → Ideal O) [∀ i, (P i).IsMaximal] (hinj : Function.Injective P) (hgood : ∀ i, lambda ∉ P i) (hchar : ∀ i, ringChar (O ⧸ P i) ≠ 2) (p : ι → O) (hP : ∀ i, P i = Ideal.span {p i}) (hp : ∀ i, p i ≠ 0) (hprimary : ∀ i, lambda ^ 2 ∣ p i - 1) (S T : Finset ι) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) : letI : ∀ i, (Ideal.span {p i}).IsMaximal := fun i => (hP i) ▸ (inferInstance : (P i).IsMaximal) let hg : ∀ i, lambda ∉ Ideal.span {p i} := fun i => (hP i) ▸ hgood i ((UniqueFactorizationMonoid.moebius (∏ i ∈ S, P i) : ℂ) * (UniqueFactorizationMonoid.moebius (∏ i ∈ T, P i) : ℂ)) * squarefreePairPoissonKernel P hinj hgood S T W scale = convertedPairPoissonKernel p hp hg S T W scale := ι:Type u_1inst✝¹:DecidableEq ιP:ι → Ideal Oinst✝:∀ (i : ι), (P i).IsMaximalhinj:Function.Injective Phgood:∀ (i : ι), lambda ∉ P ihchar:∀ (i : ι), ringChar (O ⧸ P i) ≠ 2p:ι → OhP:∀ (i : ι), P i = span {p i}hp:∀ (i : ι), p i ≠ 0hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝ⊢ let hg := ⋯; ↑(moebius (∏ i ∈ S, P i)) * ↑(moebius (∏ i ∈ T, P i)) * squarefreePairPoissonKernel P hinj hgood S T W scale = convertedPairPoissonKernel p hp hg S T W scale ι:Type u_1inst✝¹:DecidableEq ιP:ι → Ideal Oinst✝:∀ (i : ι), (P i).IsMaximalhinj:Function.Injective Phgood:∀ (i : ι), lambda ∉ P ihchar:∀ (i : ι), ringChar (O ⧸ P i) ≠ 2p:ι → OhP:∀ (i : ι), P i = span {p i}hp:∀ (i : ι), p i ≠ 0hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝhPeq:P = fun i => span {p i}⊢ let hg := ⋯; ↑(moebius (∏ i ∈ S, P i)) * ↑(moebius (∏ i ∈ T, P i)) * squarefreePairPoissonKernel P hinj hgood S T W scale = convertedPairPoissonKernel p hp hg S T W scale ι:Type u_1inst✝¹:DecidableEq ιp:ι → Ohp:∀ (i : ι), p i ≠ 0hprimary:∀ (i : ι), lambda ^ 2 ∣ p i - 1S:Finset ιT:Finset ιW:𝓢(ℝ, ℂ)scale:ℝinst✝:∀ (i : ι), ((fun i => span {p i}) i).IsMaximalhinj:Function.Injective fun i => span {p i}hgood:∀ (i : ι), lambda ∉ (fun i => span {p i}) ihchar:∀ (i : ι), ringChar (O ⧸ (fun i => span {p i}) i) ≠ 2hP:∀ (i : ι), (fun i => span {p i}) i = span {p i}⊢ let hg := ⋯; ↑(moebius (∏ i ∈ S, (fun i => span {p i}) i)) * ↑(moebius (∏ i ∈ T, (fun i => span {p i}) i)) * squarefreePairPoissonKernel (fun i => span {p i}) hinj hgood S T W scale = convertedPairPoissonKernel p hp hg S T W scale All goals completed! 🐙end GaussGeneratorTransportopen scoped BigOperators Classical SchwartzMap ContDiffnamespace ConcretePrimeRowBridgeopen ActualEisensteinCubic ShortDraftHeckeBridge ConcreteTraceCRT EisensteinSchwartzPoissonnoncomputable def mobiusIdealColumn (C : Ideal O → ℂ) (I : Ideal O) : ℂ := (UniqueFactorizationMonoid.moebius I : ℂ) * C Inoncomputable def conjugateIdealRowSum (F : Finset (Ideal O)) (hFpos : ∀ I ∈ F, I ≠ ⊥) (hFgood : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (C : Ideal O → ℂ) (y : O) : ℂ := ∑ I ∈ F, mobiusIdealColumn C I * star (idealSexticRow F hFpos hFgood I y)theorem conjugateIdealRowSum_eq_star (F : Finset (Ideal O)) (hFpos : ∀ I ∈ F, I ≠ ⊥) (hFgood : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (C : Ideal O → ℂ) (y : O) : conjugateIdealRowSum F hFpos hFgood C y = star (∑ I ∈ F, star (mobiusIdealColumn C I) * idealSexticRow F hFpos hFgood I y) := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂy:O⊢ conjugateIdealRowSum F hFpos hFgood C y = star (∑ I ∈ F, star (mobiusIdealColumn C I) * idealSexticRow F hFpos hFgood I y) All goals completed! 🐙theorem conjugateIdealRowSum_smoothed_summable (F : Finset (Ideal O)) (hFpos : ∀ I ∈ F, I ≠ ⊥) (hFgood : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (C : Ideal O → ℂ) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) (hscale : 0 < scale) : Summable (fun y : O => W (‖eisEmbedding y‖ ^ 2 / scale) * (↑(‖conjugateIdealRowSum F hFpos hFgood C y‖ ^ 2) : ℂ)) := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ Summable fun y => W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖conjugateIdealRowSum F hFpos hFgood C y‖ ^ 2) simp_rw F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ Summable fun y => W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖conjugateIdealRowSum F hFpos hFgood C y‖ ^ 2)F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ Summable fun y => W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖star (∑ I ∈ F, star (mobiusIdealColumn C I) * idealSexticRow F hFpos hFgood I y)‖ ^ 2) F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ Summable fun y => W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖∑ I ∈ F, star (mobiusIdealColumn C I) * idealSexticRow F hFpos hFgood I y‖ ^ 2)] F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···⊢ Summable fun y => W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖∑ I ∈ F, star (mobiusIdealColumn C I) * idealSexticRow F hFpos hFgood I y‖ ^ 2) All goals completed! 🐙theorem conjugateIdealRowSum_smoothed_poisson (F : Finset (Ideal O)) (hFpos : ∀ I ∈ F, I ≠ ⊥) (hFgood : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (hchar : ∀ i : primePool F, ringChar (O ⧸ i.val) ≠ 2) (C : Ideal O → ℂ) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) (hscale : 0 < scale) : (∑' y : O, W (‖eisEmbedding y‖ ^ 2 / scale) * (↑(‖conjugateIdealRowSum F hFpos hFgood C y‖ ^ 2) : ℂ)) = ∑ I ∈ F, ∑ J ∈ F, (star (mobiusIdealColumn C I) * mobiusIdealColumn C J) * idealPairPoissonKernel F hFpos hFgood J I W scale := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑' (y : O), W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖conjugateIdealRowSum F hFpos hFgood C y‖ ^ 2) = ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale simp_rw F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑' (y : O), W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖conjugateIdealRowSum F hFpos hFgood C y‖ ^ 2) = ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scaleF:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑' (y : O), W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖star (∑ I ∈ F, star (mobiusIdealColumn C I) * idealSexticRow F hFpos hFgood I y)‖ ^ 2) = ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑' (y : O), W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖∑ I ∈ F, star (mobiusIdealColumn C I) * idealSexticRow F hFpos hFgood I y‖ ^ 2) = ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale] F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···⊢ ∑' (y : O), W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖∑ I ∈ F, star (mobiusIdealColumn C I) * idealSexticRow F hFpos hFgood I y‖ ^ 2) = ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···⊢ ∑' (y : O), W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖∑ I ∈ F, star (mobiusIdealColumn C I) * finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F I) y‖ ^ 2) = ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···⊢ ∑ y ∈ F, ∑ x ∈ F, star (star (mobiusIdealColumn C x)) * star (mobiusIdealColumn C y) * ∑' (u : ActualEisensteinCubic.O), star (finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F x) u) * finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F y) u * W (‖eisEmbedding u‖ ^ 2 / scale) = ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···⊢ ∀ x ∈ F, ∑ x_1 ∈ F, star (star (mobiusIdealColumn C x_1)) * star (mobiusIdealColumn C x) * ∑' (u : ActualEisensteinCubic.O), star (finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F x_1) u) * finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F x) u * W (‖eisEmbedding u‖ ^ 2 / scale) = ∑ J ∈ F, star (mobiusIdealColumn C x) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J x W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···I:Ideal OhI:I ∈ F⊢ ∑ x ∈ F, star (star (mobiusIdealColumn C x)) * star (mobiusIdealColumn C I) * ∑' (u : ActualEisensteinCubic.O), star (finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F x) u) * finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F I) u * W (‖eisEmbedding u‖ ^ 2 / scale) = ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···I:Ideal OhI:I ∈ F⊢ ∀ x ∈ F, star (star (mobiusIdealColumn C x)) * star (mobiusIdealColumn C I) * ∑' (u : ActualEisensteinCubic.O), star (finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F x) u) * finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F I) u * W (‖eisEmbedding u‖ ^ 2 / scale) = star (mobiusIdealColumn C I) * mobiusIdealColumn C x * idealPairPoissonKernel F hFpos hFgood x I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···I:Ideal OhI:I ∈ FJ:Ideal OhJ:J ∈ F⊢ star (star (mobiusIdealColumn C J)) * star (mobiusIdealColumn C I) * ∑' (u : ActualEisensteinCubic.O), star (finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F J) u) * finiteSquarefreeRow (fun i => ↑i) ⋯ (idealSupport F I) u * W (‖eisEmbedding u‖ ^ 2 / scale) = star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···I:Ideal OhI:I ∈ FJ:Ideal OhJ:J ∈ F⊢ mobiusIdealColumn C J * star (mobiusIdealColumn C I) * squarefreePairPoissonKernel (fun i => ↑i) ⋯ ⋯ (idealSupport F J) (idealSupport F I) W scale = star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scalethis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···I:Ideal OhI:I ∈ FJ:Ideal OhJ:J ∈ F⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * squarefreePairPoissonKernel (fun i => ↑i) ⋯ ⋯ (idealSupport F J) (idealSupport F I) W scale = star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale All goals completed! 🐙theorem mobiusIdealColumn_eq_zero_of_not_squarefree (C : Ideal O → ℂ) {I : Ideal O} (hI : ¬ Squarefree I) : mobiusIdealColumn C I = 0 := C:Ideal O → ℂI:Ideal OhI:¬Squarefree I⊢ mobiusIdealColumn C I = 0 All goals completed! 🐙theorem conjugateIdealRowSum_zeroMode_offDiagonal (F : Finset (Ideal O)) (hFpos : ∀ I ∈ F, I ≠ ⊥) (hFgood : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (C : Ideal O → ℂ) {I J : Ideal O} (hI : I ∈ F) (hJ : J ∈ F) (hIJ : I ≠ J) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) : (star (mobiusIdealColumn C I) * mobiusIdealColumn C J) * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝ⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:Squarefree I⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:¬Squarefree I⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:Squarefree I⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:Squarefree IhsJ:Squarefree J⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:Squarefree IhsJ:¬Squarefree J⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:Squarefree IhsJ:Squarefree J⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:Squarefree IhsJ:Squarefree Jhsupport:idealSupport F J ≠ idealSupport F I⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:Squarefree IhsJ:Squarefree Jhsupport:idealSupport F J ≠ idealSupport F Ithis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:Squarefree IhsJ:Squarefree Jhsupport:idealSupport F J ≠ idealSupport F Ithis:∀ (i : ↥(primePool F)), (↑i).IsMaximal := ···hz:idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 All goals completed! 🐙 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:Squarefree IhsJ:¬Squarefree J⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 All goals completed! 🐙 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂI:Ideal OJ:Ideal OhI:I ∈ FhJ:J ∈ FhIJ:I ≠ JW:𝓢(ℝ, ℂ)scale:ℝhsI:¬Squarefree I⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 All goals completed! 🐙theorem conjugateIdealRowSum_zeroMode_formula (F : Finset (Ideal O)) (hFpos : ∀ I ∈ F, I ≠ ⊥) (hFgood : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (C : Ideal O → ℂ) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) : (∑ I ∈ F, ∑ J ∈ F, (star (mobiusIdealColumn C I) * mobiusIdealColumn C J) * idealPairPoissonZeroMode F hFpos hFgood J I W scale) = (scale : ℂ) * paperRadialFourier W 0 * ∑ I ∈ F, (↑(‖mobiusIdealColumn C I‖ ^ 2) : ℂ) * idealPrimeDensity F I := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝ⊢ ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = ↑scale * paperRadialFourier (⇑W) 0 * ∑ I ∈ F, ↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I) F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝ⊢ ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = ∑ i ∈ F, ↑scale * paperRadialFourier (⇑W) 0 * (↑(‖mobiusIdealColumn C i‖ ^ 2) * ↑(idealPrimeDensity F i)) F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝ⊢ ∀ x ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C x) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J x W scale = ↑scale * paperRadialFourier (⇑W) 0 * (↑(‖mobiusIdealColumn C x‖ ^ 2) * ↑(idealPrimeDensity F x)) F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = ↑scale * paperRadialFourier (⇑W) 0 * (↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I)) F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C I * idealPairPoissonZeroMode F hFpos hFgood I I W scale = ↑scale * paperRadialFourier (⇑W) 0 * (↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I))F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ∀ b ∈ F, b ≠ I → star (mobiusIdealColumn C I) * mobiusIdealColumn C b * idealPairPoissonZeroMode F hFpos hFgood b I W scale = 0F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ I ∉ F → star (mobiusIdealColumn C I) * mobiusIdealColumn C I * idealPairPoissonZeroMode F hFpos hFgood I I W scale = 0 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C I * idealPairPoissonZeroMode F hFpos hFgood I I W scale = ↑scale * paperRadialFourier (⇑W) 0 * (↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I)) F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C I * (↑scale * paperRadialFourier (⇑W) 0 * ↑(idealPrimeDensity F I)) = ↑scale * paperRadialFourier (⇑W) 0 * ((starRingEnd ℂ) (mobiusIdealColumn C I) * mobiusIdealColumn C I * ↑(idealPrimeDensity F I)) F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C I * (↑scale * paperRadialFourier (⇑W) 0 * ↑(idealPrimeDensity F I)) = ↑scale * paperRadialFourier (⇑W) 0 * (star (mobiusIdealColumn C I) * mobiusIdealColumn C I * ↑(idealPrimeDensity F I)) All goals completed! 🐙 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ∀ b ∈ F, b ≠ I → star (mobiusIdealColumn C I) * mobiusIdealColumn C b * idealPairPoissonZeroMode F hFpos hFgood b I W scale = 0 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ FJ:Ideal OhJ:J ∈ FhJI:J ≠ I⊢ star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale = 0 All goals completed! 🐙 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ I ∉ F → star (mobiusIdealColumn C I) * mobiusIdealColumn C I * idealPairPoissonZeroMode F hFpos hFgood I I W scale = 0 All goals completed! 🐙theorem conjugateIdealRowSum_smoothed_poisson_zero_split (F : Finset (Ideal O)) (hFpos : ∀ I ∈ F, I ≠ ⊥) (hFgood : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (hchar : ∀ i : primePool F, ringChar (O ⧸ i.val) ≠ 2) (C : Ideal O → ℂ) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) (hscale : 0 < scale) : (∑' y : O, W (‖eisEmbedding y‖ ^ 2 / scale) * (↑(‖conjugateIdealRowSum F hFpos hFgood C y‖ ^ 2) : ℂ)) = (scale : ℂ) * paperRadialFourier W 0 * (∑ I ∈ F, (↑(‖mobiusIdealColumn C I‖ ^ 2) : ℂ) * idealPrimeDensity F I) + ∑ I ∈ F, ∑ J ∈ F, (star (mobiusIdealColumn C I) * mobiusIdealColumn C J) * idealPairPoissonNonzeroMode F hFpos hFgood J I W scale := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑' (y : O), W (‖eisEmbedding y‖ ^ 2 / scale) * ↑(‖conjugateIdealRowSum F hFpos hFgood C y‖ ^ 2) = ↑scale * paperRadialFourier (⇑W) 0 * ∑ I ∈ F, ↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I) + ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonNonzeroMode F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale = ↑scale * paperRadialFourier (⇑W) 0 * ∑ I ∈ F, ↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I) + ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonNonzeroMode F hFpos hFgood J I W scale simp_rw F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonKernel F hFpos hFgood J I W scale = ↑scale * paperRadialFourier (⇑W) 0 * ∑ I ∈ F, ↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I) + ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonNonzeroMode F hFpos hFgood J I W scaleF:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑ x ∈ F, ∑ x_1 ∈ F, star (mobiusIdealColumn C x) * mobiusIdealColumn C x_1 * (idealPairPoissonZeroMode F hFpos hFgood x_1 x W scale + idealPairPoissonNonzeroMode F hFpos hFgood x_1 x W scale) = ↑scale * paperRadialFourier (⇑W) 0 * ∑ I ∈ F, ↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I) + ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonNonzeroMode F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑ x ∈ F, ∑ x_1 ∈ F, (star (mobiusIdealColumn C x) * mobiusIdealColumn C x_1 * idealPairPoissonZeroMode F hFpos hFgood x_1 x W scale + star (mobiusIdealColumn C x) * mobiusIdealColumn C x_1 * idealPairPoissonNonzeroMode F hFpos hFgood x_1 x W scale) = ↑scale * paperRadialFourier (⇑W) 0 * ∑ I ∈ F, ↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I) + ∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonNonzeroMode F hFpos hFgood J I W scale F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Phchar:∀ (i : ↥(primePool F)), ringChar (O ⧸ ↑i) ≠ 2C:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝhscale:0 < scale⊢ ∑ x ∈ F, ∑ x_1 ∈ F, star (mobiusIdealColumn C x) * mobiusIdealColumn C x_1 * idealPairPoissonZeroMode F hFpos hFgood x_1 x W scale + ∑ x ∈ F, ∑ x_1 ∈ F, star (mobiusIdealColumn C x) * mobiusIdealColumn C x_1 * idealPairPoissonNonzeroMode F hFpos hFgood x_1 x W scale = ↑scale * paperRadialFourier (⇑W) 0 * ∑ I ∈ F, ↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I) + ∑ x ∈ F, ∑ x_1 ∈ F, star (mobiusIdealColumn C x) * mobiusIdealColumn C x_1 * idealPairPoissonNonzeroMode F hFpos hFgood x_1 x W scale] All goals completed! 🐙theorem norm_mobiusIdealColumn_le (C : Ideal O → ℂ) (I : Ideal O) : ‖mobiusIdealColumn C I‖ ≤ ‖C I‖ := C:Ideal O → ℂI:Ideal O⊢ ‖mobiusIdealColumn C I‖ ≤ ‖C I‖ C:Ideal O → ℂI:Ideal OhI:Squarefree I⊢ ‖mobiusIdealColumn C I‖ ≤ ‖C I‖C:Ideal O → ℂI:Ideal OhI:¬Squarefree I⊢ ‖mobiusIdealColumn C I‖ ≤ ‖C I‖ C:Ideal O → ℂI:Ideal OhI:Squarefree I⊢ ‖mobiusIdealColumn C I‖ ≤ ‖C I‖ All goals completed! 🐙 C:Ideal O → ℂI:Ideal OhI:¬Squarefree I⊢ ‖mobiusIdealColumn C I‖ ≤ ‖C I‖ C:Ideal O → ℂI:Ideal OhI:¬Squarefree I⊢ 0 ≤ ‖C I‖ All goals completed! 🐙theorem norm_conjugateIdealRowSum_zeroMode_le (F : Finset (Ideal O)) (hFpos : ∀ I ∈ F, I ≠ ⊥) (hFgood : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (C : Ideal O → ℂ) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) : ‖∑ I ∈ F, ∑ J ∈ F, (star (mobiusIdealColumn C I) * mobiusIdealColumn C J) * idealPairPoissonZeroMode F hFpos hFgood J I W scale‖ ≤ (|scale| * ‖paperRadialFourier W 0‖) * ∑ I ∈ F, ‖C I‖ ^ 2 := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝ⊢ ‖∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale‖ ≤ |scale| * ‖paperRadialFourier (⇑W) 0‖ * ∑ I ∈ F, ‖C I‖ ^ 2 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝ⊢ |scale| * ‖paperRadialFourier (⇑W) 0‖ * ‖∑ I ∈ F, ↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I)‖ ≤ |scale| * ‖paperRadialFourier (⇑W) 0‖ * ∑ I ∈ F, ‖C I‖ ^ 2 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝ⊢ ‖∑ I ∈ F, ↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I)‖ ≤ ∑ I ∈ F, ‖C I‖ ^ 2 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖↑(‖mobiusIdealColumn C I‖ ^ 2) * ↑(idealPrimeDensity F I)‖ ≤ ‖C I‖ ^ 2 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖mobiusIdealColumn C I‖ ^ 2 * idealPrimeDensity F I ≤ ‖C I‖ ^ 2 calc _ ≤ ‖mobiusIdealColumn C I‖ ^ 2 := mul_le_of_le_one_right (sq_nonneg _) (idealPrimeDensity_mem_Icc F hFpos I).2 _ ≤ ‖C I‖ ^ 2 := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖mobiusIdealColumn C I‖ ^ 2 ≤ ‖C I‖ ^ 2 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PC:Ideal O → ℂW:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖mobiusIdealColumn C I‖ ≤ ‖C I‖; All goals completed! 🐙theorem norm_secondPoisson_zeroMode_fixed_factors (F : Finset (Ideal O)) (hFpos : ∀ I ∈ F, I ≠ ⊥) (hFgood : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (ξ ρ : Ideal O → ℂ) (A : ℕ → ℂ) (hξ : ∀ I ∈ F, ‖ξ I‖ ≤ 1) (hρ : ∀ I ∈ F, ‖ρ I‖ ≤ 1) (W : 𝓢(ℝ, ℂ)) (scale : ℝ) : let C : Ideal O → ℂ := fun I => ξ I * ρ I * A (Ideal.absNorm I) ‖∑ I ∈ F, ∑ J ∈ F, (star (mobiusIdealColumn C I) * mobiusIdealColumn C J) * idealPairPoissonZeroMode F hFpos hFgood J I W scale‖ ≤ (|scale| * ‖paperRadialFourier W 0‖) * ∑ I ∈ F, ‖A (Ideal.absNorm I)‖ ^ 2 := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝ⊢ let C := fun I => ξ I * ρ I * A (absNorm I); ‖∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn C I) * mobiusIdealColumn C J * idealPairPoissonZeroMode F hFpos hFgood J I W scale‖ ≤ |scale| * ‖paperRadialFourier (⇑W) 0‖ * ∑ I ∈ F, ‖A (absNorm I)‖ ^ 2 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝ⊢ ‖∑ I ∈ F, ∑ J ∈ F, star (mobiusIdealColumn (fun I => ξ I * ρ I * A (absNorm I)) I) * mobiusIdealColumn (fun I => ξ I * ρ I * A (absNorm I)) J * idealPairPoissonZeroMode F hFpos hFgood J I W scale‖ ≤ |scale| * ‖paperRadialFourier (⇑W) 0‖ * ∑ I ∈ F, ‖A (absNorm I)‖ ^ 2 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝ⊢ |scale| * ‖paperRadialFourier (⇑W) 0‖ * ∑ I ∈ F, ‖ξ I * ρ I * A (absNorm I)‖ ^ 2 ≤ |scale| * ‖paperRadialFourier (⇑W) 0‖ * ∑ I ∈ F, ‖A (absNorm I)‖ ^ 2 F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖ξ I * ρ I * A (absNorm I)‖ ≤ ‖A (absNorm I)‖ F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖ξ I‖ * ‖ρ I‖ * ‖A (absNorm I)‖ ≤ ‖A (absNorm I)‖ calc ‖ξ I‖ * ‖ρ I‖ * ‖A (Ideal.absNorm I)‖ ≤ 1 * 1 * ‖A (Ideal.absNorm I)‖ := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖ξ I‖ * ‖ρ I‖ * ‖A (absNorm I)‖ ≤ 1 * 1 * ‖A (absNorm I)‖ F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖ξ I‖ ≤ 1F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖ρ I‖ ≤ 1; F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ ‖ρ I‖ ≤ 1; All goals completed! 🐙 _ = _ := F:Finset (Ideal O)hFpos:∀ I ∈ F, I ≠ ⊥hFgood:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ Pξ:Ideal O → ℂρ:Ideal O → ℂA:ℕ → ℂhξ:∀ I ∈ F, ‖ξ I‖ ≤ 1hρ:∀ I ∈ F, ‖ρ I‖ ≤ 1W:𝓢(ℝ, ℂ)scale:ℝI:Ideal OhI:I ∈ F⊢ 1 * 1 * ‖A (absNorm I)‖ = ‖A (absNorm I)‖ All goals completed! 🐙end ConcretePrimeRowBridgeopen MeasureTheory Setopen scoped BigOperatorsnamespace EisensteinSchwartzPoissontheorem scaled_cauchy_antitone (b : ℝ) : AntitoneOn (fun x : ℝ => (1 + (b * x) ^ 2)⁻¹) (Ici 0) := b:ℝ⊢ AntitoneOn (fun x => (1 + (b * x) ^ 2)⁻¹) (Set.Ici 0) b:ℝx:ℝhx:x ∈ Set.Ici 0y:ℝhy:y ∈ Set.Ici 0hxy:x ≤ y⊢ (fun x => (1 + (b * x) ^ 2)⁻¹) y ≤ (fun x => (1 + (b * x) ^ 2)⁻¹) x b:ℝx:ℝy:ℝhy:y ∈ Set.Ici 0hxy:x ≤ yhx:0 ≤ x⊢ (fun x => (1 + (b * x) ^ 2)⁻¹) y ≤ (fun x => (1 + (b * x) ^ 2)⁻¹) x b:ℝx:ℝy:ℝhxy:x ≤ yhx:0 ≤ xhy:0 ≤ y⊢ (fun x => (1 + (b * x) ^ 2)⁻¹) y ≤ (fun x => (1 + (b * x) ^ 2)⁻¹) x apply inv_anti₀ (b:ℝx:ℝy:ℝhxy:x ≤ yhx:0 ≤ xhy:0 ≤ y⊢ 0 < 1 + (b * x) ^ 2 All goals completed! 🐙) nlinarith [sq_nonneg b, sq_nonneg (y - x), mul_nonneg (sq_nonneg b) (show 0 ≤ y ^ 2 - x ^ 2 b:ℝ⊢ AntitoneOn (fun x => (1 + (b * x) ^ 2)⁻¹) (Set.Ici 0) All goals completed! 🐙)]theorem scaled_cauchy_nat_bound (b : ℝ) (hb : 0 < b) : (∑' n : ℕ, (1 + (b * (n : ℝ)) ^ 2)⁻¹) ≤ 1 + Real.pi / (2 * b) := b:ℝhb:0 < b⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / (2 * b) b:ℝhb:0 < bhi:IntegrableOn (fun x => (1 + (b * x) ^ 2)⁻¹) (Set.Ioi 0) volume⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / (2 * b) b:ℝhb:0 < bhi:IntegrableOn (fun x => (1 + (b * x) ^ 2)⁻¹) (Set.Ioi 0) volumeht:∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ (1 + (b * 0) ^ 2)⁻¹ + ∫ (x : ℝ) in Set.Ioi 0, (1 + (b * x) ^ 2)⁻¹⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / (2 * b) b:ℝhb:0 < bhi:IntegrableOn (fun x => (1 + (b * x) ^ 2)⁻¹) (Set.Ioi 0) volumeht:∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ (1 + (b * 0) ^ 2)⁻¹ + ∫ (x : ℝ) in Set.Ioi 0, (1 + (b * x) ^ 2)⁻¹he:∫ (x : ℝ) in Set.Ioi 0, (1 + (b * x) ^ 2)⁻¹ = π / (2 * b)⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / (2 * b) All goals completed! 🐙theorem summable_scaled_cauchy_nat (b : ℝ) (hb : 0 < b) : Summable (fun n : ℕ => (1 + (b * (n : ℝ)) ^ 2)⁻¹) := b:ℝhb:0 < b⊢ Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹ exact (scaled_cauchy_antitone b).summable_of_integrableOn_Ioi_zero (integrable_inv_one_add_mul_sq hb.ne').integrableOn (fun _ _ => b:ℝhb:0 < bx✝¹:ℝx✝:x✝¹ ∈ Set.Ioi 0⊢ 0 ≤ (1 + (b * x✝¹) ^ 2)⁻¹ All goals completed! 🐙)theorem summable_scaled_cauchy_int (b : ℝ) (hb : 0 < b) : Summable (fun n : ℤ => (1 + (b * (n : ℝ)) ^ 2)⁻¹) := b:ℝhb:0 < b⊢ Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹ b:ℝhb:0 < b⊢ (Summable fun n => (1 + (b * ↑↑n) ^ 2)⁻¹) ∧ Summable fun n => (1 + (b * ↑(-↑n)) ^ 2)⁻¹ b:ℝhb:0 < b⊢ Summable fun n => (1 + (b * ↑↑n) ^ 2)⁻¹b:ℝhb:0 < b⊢ Summable fun n => (1 + (b * ↑(-↑n)) ^ 2)⁻¹ b:ℝhb:0 < b⊢ Summable fun n => (1 + (b * ↑↑n) ^ 2)⁻¹ All goals completed! 🐙 b:ℝhb:0 < b⊢ Summable fun n => (1 + (b * ↑(-↑n)) ^ 2)⁻¹ All goals completed! 🐙theorem scaled_cauchy_int_bound (b : ℝ) (hb : 0 < b) : (∑' n : ℤ, (1 + (b * (n : ℝ)) ^ 2)⁻¹) ≤ 1 + Real.pi / b := b:ℝhb:0 < b⊢ ∑' (n : ℤ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹⊢ ∑' (n : ℤ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹⊢ ∑' (n : ℤ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹hneg:Summable fun n => (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹⊢ ∑' (n : ℤ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹hneg:Summable fun n => (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹⊢ ∑' (n : ℕ), (1 + (b * ↑↑n) ^ 2)⁻¹ + ∑' (n : ℕ), (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹ ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹hneg:Summable fun n => (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ + ∑' (n : ℕ), (1 + (b * (↑n + 1)) ^ 2)⁻¹ ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹hneg:Summable fun n => (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹hz:∑' (b_1 : ℕ), (1 + (b * ↑b_1) ^ 2)⁻¹ = (1 + (b * ↑0) ^ 2)⁻¹ + ∑' (b_1 : ℕ), (1 + (b * ↑(b_1 + 1)) ^ 2)⁻¹⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ + ∑' (n : ℕ), (1 + (b * (↑n + 1)) ^ 2)⁻¹ ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹hneg:Summable fun n => (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹hz:∑' (b_1 : ℕ), (1 + (b * ↑b_1) ^ 2)⁻¹ = (1 + (b * ↑0) ^ 2)⁻¹ + ∑' (b_1 : ℕ), (1 + (b * ↑(b_1 + 1)) ^ 2)⁻¹he:∑' (n : ℕ), (1 + (b * (↑n + 1)) ^ 2)⁻¹ = ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ - 1⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ + ∑' (n : ℕ), (1 + (b * (↑n + 1)) ^ 2)⁻¹ ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹hneg:Summable fun n => (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹hz:∑' (b_1 : ℕ), (1 + (b * ↑b_1) ^ 2)⁻¹ = (1 + (b * ↑0) ^ 2)⁻¹ + ∑' (b_1 : ℕ), (1 + (b * ↑(b_1 + 1)) ^ 2)⁻¹he:∑' (n : ℕ), (1 + (b * (↑n + 1)) ^ 2)⁻¹ = ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ - 1⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ + (∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ - 1) ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹hneg:Summable fun n => (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹hz:∑' (b_1 : ℕ), (1 + (b * ↑b_1) ^ 2)⁻¹ = (1 + (b * ↑0) ^ 2)⁻¹ + ∑' (b_1 : ℕ), (1 + (b * ↑(b_1 + 1)) ^ 2)⁻¹he:∑' (n : ℕ), (1 + (b * (↑n + 1)) ^ 2)⁻¹ = ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ - 1this:∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / (2 * b)⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ + (∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ - 1) ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹hneg:Summable fun n => (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹hz:∑' (b_1 : ℕ), (1 + (b * ↑b_1) ^ 2)⁻¹ = (1 + (b * ↑0) ^ 2)⁻¹ + ∑' (b_1 : ℕ), (1 + (b * ↑(b_1 + 1)) ^ 2)⁻¹he:∑' (n : ℕ), (1 + (b * (↑n + 1)) ^ 2)⁻¹ = ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ - 1this:∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / (2 * b)hh:π / (2 * b) = π / b / 2⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ + (∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ - 1) ≤ 1 + π / b b:ℝhb:0 < bhs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hs1:Summable fun n => (1 + (b * ↑(n + 1)) ^ 2)⁻¹hneg:Summable fun n => (1 + (b * ↑(-(↑n + 1))) ^ 2)⁻¹hz:∑' (b_1 : ℕ), (1 + (b * ↑b_1) ^ 2)⁻¹ = (1 + (b * ↑0) ^ 2)⁻¹ + ∑' (b_1 : ℕ), (1 + (b * ↑(b_1 + 1)) ^ 2)⁻¹he:∑' (n : ℕ), (1 + (b * (↑n + 1)) ^ 2)⁻¹ = ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ - 1this:∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / b / 2hh:π / (2 * b) = π / b / 2⊢ ∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ + (∑' (n : ℕ), (1 + (b * ↑n) ^ 2)⁻¹ - 1) ≤ 1 + π / b All goals completed! 🐙open ConcreteTraceCRT ActualEisensteinCubictheorem scaled_eisenstein_cauchy_summable (K : ℝ) (hK : 0 < K) : Summable (fun h : O => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) := K:ℝhK:0 < K⊢ Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ K:ℝhK:0 < Kb:ℝ := √K⊢ Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ K:ℝhK:0 < Kb:ℝ := √Khb:0 < b⊢ Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = K⊢ Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹⊢ Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹⊢ Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹⊢ Summable ((fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ ⇑latticeCoordEquiv.symm) K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹⊢ Summable fun p => ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹ apply Summable.of_nonneg_of_le (fun _ => K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹x✝:ℤ × ℤ⊢ 0 ≤ ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm x✝)‖ ^ 2) ^ 2)⁻¹ All goals completed! 🐙) _ (hp.mul_left 4) K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹p:ℤ × ℤ⊢ ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹ ≤ 4 * ((1 + (b * ↑p.1) ^ 2)⁻¹ * (1 + (b * ↑p.2) ^ 2)⁻¹) apply inverse_square_le_cauchy_product (b * (p.1 : ℝ)) (b * (p.2 : ℝ)) (K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) (K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹p:ℤ × ℤ⊢ 0 ≤ K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2 All goals completed! 🐙) K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹p:ℤ × ℤ⊢ ((b * ↑p.1) ^ 2 + (b * ↑p.2) ^ 2) / 2 ≤ K * ‖eisEmbedding (ActualEisensteinCoordinates.eval p.1 p.2)‖ ^ 2 K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹p:ℤ × ℤ⊢ ((b * ↑p.1) ^ 2 + (b * ↑p.2) ^ 2) / 2 ≤ K * ↑(p.1 * p.1 - p.1 * p.2 + p.2 * p.2) K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹p:ℤ × ℤ⊢ ((b * ↑p.1) ^ 2 + (b * ↑p.2) ^ 2) / 2 ≤ K * (↑p.1 * ↑p.1 - ↑p.1 * ↑p.2 + ↑p.2 * ↑p.2) All goals completed! 🐙theorem scaled_eisenstein_cauchy_bound (K : ℝ) (hK : 0 < K) : (∑' h : O, ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ≤ 4 * (1 + Real.pi / Real.sqrt K) ^ 2 := K:ℝhK:0 < K⊢ ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2 K:ℝhK:0 < Kb:ℝ := √K⊢ ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2 K:ℝhK:0 < Kb:ℝ := √Khb:0 < b⊢ ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2 K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = K⊢ ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2 K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹⊢ ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2 K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹⊢ ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2 K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹⊢ ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2 K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹⊢ ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2 calc _ ≤ ∑' p : ℤ × ℤ, 4 * ((1 + (b * (p.1 : ℝ)) ^ 2)⁻¹ * (1 + (b * (p.2 : ℝ)) ^ 2)⁻¹) := K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹⊢ ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹ ≤ ∑' (p : ℤ × ℤ), 4 * ((1 + (b * ↑p.1) ^ 2)⁻¹ * (1 + (b * ↑p.2) ^ 2)⁻¹) K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹⊢ ∀ (i : ℤ × ℤ), ((fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ ⇑latticeCoordEquiv.symm) i ≤ 4 * ((1 + (b * ↑i.1) ^ 2)⁻¹ * (1 + (b * ↑i.2) ^ 2)⁻¹) K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹p:ℤ × ℤ⊢ ((fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ ⇑latticeCoordEquiv.symm) p ≤ 4 * ((1 + (b * ↑p.1) ^ 2)⁻¹ * (1 + (b * ↑p.2) ^ 2)⁻¹) apply inverse_square_le_cauchy_product _ _ _ (K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹p:ℤ × ℤ⊢ 0 ≤ K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2 All goals completed! 🐙) K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹p:ℤ × ℤ⊢ ((b * ↑p.1) ^ 2 + (b * ↑p.2) ^ 2) / 2 ≤ K * ‖eisEmbedding (ActualEisensteinCoordinates.eval p.1 p.2)‖ ^ 2 K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹p:ℤ × ℤ⊢ ((b * ↑p.1) ^ 2 + (b * ↑p.2) ^ 2) / 2 ≤ K * ↑(p.1 * p.1 - p.1 * p.2 + p.2 * p.2) K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹p:ℤ × ℤ⊢ ((b * ↑p.1) ^ 2 + (b * ↑p.2) ^ 2) / 2 ≤ K * (↑p.1 * ↑p.1 - ↑p.1 * ↑p.2 + ↑p.2 * ↑p.2) All goals completed! 🐙 _ = 4 * (∑' n : ℤ, (1 + (b * (n : ℝ)) ^ 2)⁻¹) ^ 2 := K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹⊢ ∑' (p : ℤ × ℤ), 4 * ((1 + (b * ↑p.1) ^ 2)⁻¹ * (1 + (b * ↑p.2) ^ 2)⁻¹) = 4 * (∑' (n : ℤ), (1 + (b * ↑n) ^ 2)⁻¹) ^ 2 All goals completed! 🐙 _ ≤ 4 * (1 + Real.pi / b) ^ 2 := K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹⊢ 4 * (∑' (n : ℤ), (1 + (b * ↑n) ^ 2)⁻¹) ^ 2 ≤ 4 * (1 + π / b) ^ 2 K:ℝhK:0 < Kb:ℝ := √Khb:0 < bhbsq:b ^ 2 = Khs:Summable fun n => (1 + (b * ↑n) ^ 2)⁻¹hp:Summable fun x => (1 + (b * ↑x.1) ^ 2)⁻¹ * (1 + (b * ↑x.2) ^ 2)⁻¹he:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ = ∑' (p : ℤ × ℤ), ((1 + K * ‖eisEmbedding (latticeCoordEquiv.symm p)‖ ^ 2) ^ 2)⁻¹⊢ ∑' (n : ℤ), (1 + (b * ↑n) ^ 2)⁻¹ ≤ 1 + π / b All goals completed! 🐙theorem scaled_eisenstein_cauchy_small (K : ℝ) (hK : 0 < K) (hK1 : K ≤ 1) : K * (∑' h : O, ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ≤ 4 * (1 + Real.pi) ^ 2 := K:ℝhK:0 < KhK1:K ≤ 1⊢ K * ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π) ^ 2 K:ℝhK:0 < KhK1:K ≤ 1hs:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2⊢ K * ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π) ^ 2 K:ℝhK:0 < KhK1:K ≤ 1hs:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2hb:0 < √K⊢ K * ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π) ^ 2 K:ℝhK:0 < KhK1:K ≤ 1hs:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2hb:0 < √Khb1:√K ≤ 1⊢ K * ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π) ^ 2 K:ℝhK:0 < KhK1:K ≤ 1hs:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2hb:0 < √Khb1:√K ≤ 1hsq:√K ^ 2 = K⊢ K * ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π) ^ 2 calc _ ≤ K * (4 * (1 + Real.pi / Real.sqrt K) ^ 2) := mul_le_mul_of_nonneg_left hs hK.le _ = 4 * (Real.sqrt K + Real.pi) ^ 2 := K:ℝhK:0 < KhK1:K ≤ 1hs:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2hb:0 < √Khb1:√K ≤ 1hsq:√K ^ 2 = K⊢ K * (4 * (1 + π / √K) ^ 2) = 4 * (√K + π) ^ 2 nth_rw 1 [K:ℝhK:0 < KhK1:K ≤ 1hs:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2hb:0 < √Khb1:√K ≤ 1hsq:√K ^ 2 = K⊢ √K ^ 2 * (4 * (1 + π / √K) ^ 2) = 4 * (√K + π) ^ 2K:ℝhK:0 < KhK1:K ≤ 1hs:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2hb:0 < √Khb1:√K ≤ 1hsq:√K ^ 2 = K⊢ √K ^ 2 * (4 * (1 + π / √K) ^ 2) = 4 * (√K + π) ^ 2 All goals completed! 🐙 _ ≤ _ := K:ℝhK:0 < KhK1:K ≤ 1hs:∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹ ≤ 4 * (1 + π / √K) ^ 2hb:0 < √Khb1:√K ≤ 1hsq:√K ^ 2 = K⊢ 4 * (√K + π) ^ 2 ≤ 4 * (1 + π) ^ 2 All goals completed! 🐙theorem one_le_eisenstein_norm_sq (h : O) (hh : h ≠ 0) : 1 ≤ ‖eisEmbedding h‖ ^ 2 := h:Ohh:h ≠ 0⊢ 1 ≤ ‖eisEmbedding h‖ ^ 2 h:Ohh:h ≠ 0⊢ 1 ≤ ↑(absNorm (span {h})) exact_mod_cast Nat.one_le_iff_ne_zero.mpr (show Ideal.absNorm (Ideal.span {h}) ≠ 0 h:Ohh:h ≠ 0⊢ 1 ≤ ‖eisEmbedding h‖ ^ 2 h:Ohh:h ≠ 0⊢ ¬h = 0 All goals completed! 🐙)theorem cauchy_large_scale_pointwise (K q : ℝ) (hK : 1 ≤ K) (hq : 1 ≤ q) : K * ((1 + K * q) ^ 2)⁻¹ ≤ 4 * ((1 + q) ^ 2)⁻¹ := K:ℝq:ℝhK:1 ≤ Khq:1 ≤ q⊢ K * ((1 + K * q) ^ 2)⁻¹ ≤ 4 * ((1 + q) ^ 2)⁻¹ K:ℝq:ℝhK:1 ≤ Khq:1 ≤ qhKp:0 < K⊢ K * ((1 + K * q) ^ 2)⁻¹ ≤ 4 * ((1 + q) ^ 2)⁻¹ K:ℝq:ℝhK:1 ≤ Khq:1 ≤ qhKp:0 < Khqp:0 < q⊢ K * ((1 + K * q) ^ 2)⁻¹ ≤ 4 * ((1 + q) ^ 2)⁻¹ K:ℝq:ℝhK:1 ≤ Khq:1 ≤ qhKp:0 < Khqp:0 < qh1:K * (1 + q) ≤ 2 * (1 + K * q)⊢ K * ((1 + K * q) ^ 2)⁻¹ ≤ 4 * ((1 + q) ^ 2)⁻¹ K:ℝq:ℝhK:1 ≤ Khq:1 ≤ qhKp:0 < Khqp:0 < qh1:K * (1 + q) ≤ 2 * (1 + K * q)h2:(K * (1 + q)) ^ 2 ≤ (2 * (1 + K * q)) ^ 2⊢ K * ((1 + K * q) ^ 2)⁻¹ ≤ 4 * ((1 + q) ^ 2)⁻¹ K:ℝq:ℝhK:1 ≤ Khq:1 ≤ qhKp:0 < Khqp:0 < qh1:K * (1 + q) ≤ 2 * (1 + K * q)h2:(K * (1 + q)) ^ 2 ≤ (2 * (1 + K * q)) ^ 2h3:K * (1 + q) ^ 2 ≤ K ^ 2 * (1 + q) ^ 2⊢ K * ((1 + K * q) ^ 2)⁻¹ ≤ 4 * ((1 + q) ^ 2)⁻¹ apply (div_le_div_iff₀ (K:ℝq:ℝhK:1 ≤ Khq:1 ≤ qhKp:0 < Khqp:0 < qh1:K * (1 + q) ≤ 2 * (1 + K * q)h2:(K * (1 + q)) ^ 2 ≤ (2 * (1 + K * q)) ^ 2h3:K * (1 + q) ^ 2 ≤ K ^ 2 * (1 + q) ^ 2⊢ 0 < (1 + K * q) ^ 2 All goals completed! 🐙 : 0 < (1 + K * q) ^ 2) (K:ℝq:ℝhK:1 ≤ Khq:1 ≤ qhKp:0 < Khqp:0 < qh1:K * (1 + q) ≤ 2 * (1 + K * q)h2:(K * (1 + q)) ^ 2 ≤ (2 * (1 + K * q)) ^ 2h3:K * (1 + q) ^ 2 ≤ K ^ 2 * (1 + q) ^ 2⊢ 0 < (1 + q) ^ 2 All goals completed! 🐙 : 0 < (1 + q) ^ 2)).mpr All goals completed! 🐙theorem lattice_profile_nonzero_scaled_bound (F : ℝ → ℂ) (B : ℝ) (hB : 0 ≤ B) (hF : ∀ t : ℝ, 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ B) (K : ℝ) (hK : 0 < K) : K * (∑' h : {h : O // h ≠ 0}, ‖F (K * ‖eisEmbedding h.val‖ ^ 2)‖) ≤ (4 * (1 + Real.pi) ^ 2 + 4 * eisensteinCauchyMass) * B := F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < K⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:K ≤ 1⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * BF:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:¬K ≤ 1⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:K ≤ 1⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:K ≤ 1htotal:∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ ∑' (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:K ≤ 1htotal:∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ ∑' (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hbound:∑' (i : O), ‖F (K * ‖eisEmbedding i‖ ^ 2)‖ ≤ ∑' (i : O), B * ((1 + K * ‖eisEmbedding i‖ ^ 2) ^ 2)⁻¹⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:K ≤ 1htotal:∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ ∑' (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hbound:∑' (i : O), ‖F (K * ‖eisEmbedding i‖ ^ 2)‖ ≤ B * ∑' (x : O), ((1 + K * ‖eisEmbedding x‖ ^ 2) ^ 2)⁻¹⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B calc _ ≤ K * (B * ∑' h : O, ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) := mul_le_mul_of_nonneg_left (htotal.trans hbound) hK.le _ = B * (K * ∑' h : O, ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) := F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:K ≤ 1htotal:∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ ∑' (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hbound:∑' (i : O), ‖F (K * ‖eisEmbedding i‖ ^ 2)‖ ≤ B * ∑' (x : O), ((1 + K * ‖eisEmbedding x‖ ^ 2) ^ 2)⁻¹⊢ K * (B * ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) = B * (K * ∑' (h : O), ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) All goals completed! 🐙 _ ≤ B * (4 * (1 + Real.pi) ^ 2) := mul_le_mul_of_nonneg_left (scaled_eisenstein_cauchy_small K hK hK1) hB _ ≤ _ := F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:K ≤ 1htotal:∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ ∑' (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hbound:∑' (i : O), ‖F (K * ‖eisEmbedding i‖ ^ 2)‖ ≤ B * ∑' (x : O), ((1 + K * ‖eisEmbedding x‖ ^ 2) ^ 2)⁻¹⊢ B * (4 * (1 + π) ^ 2) ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B All goals completed! 🐙 F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:¬K ≤ 1⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:¬K ≤ 1hp:∀ (h : { h // h ≠ 0 }), K * ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ 4 * B * ((1 + ‖eisEmbedding ↑h‖ ^ 2) ^ 2)⁻¹⊢ K * ∑' (h : { h // h ≠ 0 }), ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B calc _ = ∑' h : {h : O // h ≠ 0}, K * ‖F (K * ‖eisEmbedding h.val‖ ^ 2)‖ := tsum_mul_left.symm _ ≤ ∑' h : {h : O // h ≠ 0}, (4 * B) * ((1 + ‖eisEmbedding h.val‖ ^ 2) ^ 2)⁻¹ := (hsub.mul_left K).tsum_le_tsum hp (hc.mul_left (4 * B)) _ = (4 * B) * ∑' h : {h : O // h ≠ 0}, ((1 + ‖eisEmbedding h.val‖ ^ 2) ^ 2)⁻¹ := tsum_mul_left _ ≤ (4 * B) * eisensteinCauchyMass := mul_le_mul_of_nonneg_left (eisensteinCauchyMass_subtype (fun h : O => h ≠ 0)) (F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:¬K ≤ 1hp:∀ (h : { h // h ≠ 0 }), K * ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ 4 * B * ((1 + ‖eisEmbedding ↑h‖ ^ 2) ^ 2)⁻¹⊢ 0 ≤ 4 * B All goals completed! 🐙) _ ≤ _ := F:ℝ → ℂB:ℝhB:0 ≤ BhF:∀ (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖F t‖ ≤ BK:ℝhK:0 < Khm:∀ (h : O), ‖F (K * ‖eisEmbedding h‖ ^ 2)‖ ≤ B * ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hs:Summable fun h => ((1 + K * ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹hf:Summable fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖hsub:Summable ((fun h => ‖F (K * ‖eisEmbedding h‖ ^ 2)‖) ∘ Subtype.val)hc:Summable ((fun h => ((1 + ‖eisEmbedding h‖ ^ 2) ^ 2)⁻¹) ∘ Subtype.val)hK1:¬K ≤ 1hp:∀ (h : { h // h ≠ 0 }), K * ‖F (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ 4 * B * ((1 + ‖eisEmbedding ↑h‖ ^ 2) ^ 2)⁻¹⊢ 4 * B * eisensteinCauchyMass ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * B All goals completed! 🐙theorem paperRadialFourier_nonzero_lattice_uniform : ∃ (s : Finset (ℕ × ℕ)) (C : ℝ), 0 < C ∧ ∀ (W : SchwartzMap ℝ ℂ) (K : ℝ), 0 < K → K * (∑' h : {h : O // h ≠ 0}, ‖paperRadialFourier W (K * ‖eisEmbedding h.val‖ ^ 2)‖) ≤ C * s.sup (schwartzSeminormFamily ℝ ℝ ℂ) W := ⊢ ∃ s C, 0 < C ∧ ∀ (W : 𝓢(ℝ, ℂ)) (K : ℝ), 0 < K → K * ∑' (h : { h // h ≠ 0 }), ‖paperRadialFourier (⇑W) (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W s:Finset (ℕ × ℕ)C:ℝhC:0 < Chb:∀ (W : 𝓢(ℝ, ℂ)) (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖paperRadialFourier (⇑W) t‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W⊢ ∃ s C, 0 < C ∧ ∀ (W : 𝓢(ℝ, ℂ)) (K : ℝ), 0 < K → K * ∑' (h : { h // h ≠ 0 }), ‖paperRadialFourier (⇑W) (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W s:Finset (ℕ × ℕ)C:ℝhC:0 < Chb:∀ (W : 𝓢(ℝ, ℂ)) (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖paperRadialFourier (⇑W) t‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W⊢ 0 < (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * Cs:Finset (ℕ × ℕ)C:ℝhC:0 < Chb:∀ (W : 𝓢(ℝ, ℂ)) (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖paperRadialFourier (⇑W) t‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W⊢ ∀ (W : 𝓢(ℝ, ℂ)) (K : ℝ), 0 < K → K * ∑' (h : { h // h ≠ 0 }), ‖paperRadialFourier (⇑W) (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W s:Finset (ℕ × ℕ)C:ℝhC:0 < Chb:∀ (W : 𝓢(ℝ, ℂ)) (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖paperRadialFourier (⇑W) t‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W⊢ 0 < (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * C s:Finset (ℕ × ℕ)C:ℝhC:0 < Chb:∀ (W : 𝓢(ℝ, ℂ)) (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖paperRadialFourier (⇑W) t‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) Wthis:0 ≤ eisensteinCauchyMass⊢ 0 < (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * C s:Finset (ℕ × ℕ)C:ℝhC:0 < Chb:∀ (W : 𝓢(ℝ, ℂ)) (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖paperRadialFourier (⇑W) t‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) Wthis✝:0 ≤ eisensteinCauchyMassthis:0 < π⊢ 0 < (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * C All goals completed! 🐙 s:Finset (ℕ × ℕ)C:ℝhC:0 < Chb:∀ (W : 𝓢(ℝ, ℂ)) (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖paperRadialFourier (⇑W) t‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W⊢ ∀ (W : 𝓢(ℝ, ℂ)) (K : ℝ), 0 < K → K * ∑' (h : { h // h ≠ 0 }), ‖paperRadialFourier (⇑W) (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W s:Finset (ℕ × ℕ)C:ℝhC:0 < Chb:∀ (W : 𝓢(ℝ, ℂ)) (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖paperRadialFourier (⇑W) t‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) WW:𝓢(ℝ, ℂ)K:ℝhK:0 < K⊢ K * ∑' (h : { h // h ≠ 0 }), ‖paperRadialFourier (⇑W) (K * ‖eisEmbedding ↑h‖ ^ 2)‖ ≤ (4 * (1 + π) ^ 2 + 4 * eisensteinCauchyMass) * C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W simpa only [mul_assoc] using lattice_profile_nonzero_scaled_bound (paperRadialFourier W) (C * s.sup (schwartzSeminormFamily ℝ ℝ ℂ) W) (s:Finset (ℕ × ℕ)C:ℝhC:0 < Chb:∀ (W : 𝓢(ℝ, ℂ)) (t : ℝ), 0 ≤ t → (1 + t) ^ 2 * ‖paperRadialFourier (⇑W) t‖ ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) WW:𝓢(ℝ, ℂ)K:ℝhK:0 < K⊢ 0 ≤ C * (s.sup (schwartzSeminormFamily ℝ ℝ ℂ)) W All goals completed! 🐙) (hb W) K hKend EisensteinSchwartzPoissonendend OAI