1. OAI
  2. NumberTheory
  3. DirichletL
  4. RowCompletion
  5. ThetaNonvanishing
import OAI.NumberTheory.DirichletL.Hecke.MobiusEulerCorrectionnamespace OAInoncomputable sectionopen scoped BigOperatorsopen MulChar AddCharopen scoped BigOperatorsopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen MeasureTheory Realopen scoped FourierTransform SchwartzMapopen Finset Complexopen scoped Classicalopen scoped Classicalopen Filter Real Asymptoticsopen ActualEisensteinCubicopen Filteropen ActualEisensteinCubic RationalPrimeExtraction ShortDraftLatticeCountopen ActualEisensteinCubic ShortDraftLatticeCountopen Filteropen scoped Topologyopen EisensteinEmbedding ConcreteTraceCRT ActualEisensteinCubicopen MulChar AddCharopen Filter Asymptoticsopen scoped LSeries.notation ArithmeticFunction.Moebiusopen Filteropen MulChar AddCharopen MulChar AddCharopen scoped LSeries.notation ArithmeticFunction.Moebiusopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptoticsopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Ideal NumberField RingOfIntegers UniqueFactorizationMonoidopen Filter Asymptoticsopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptotics Ideal NumberFieldopen Filteropen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen Filter Asymptotics MeasureTheoryopen scoped Topologyopen MeasureTheory Realopen scoped ContDiff FourierTransform SchwartzMapopen scoped BigOperators Classicalopen scoped BigOperators Classicalopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classical SchwartzMap ContDiffopen scoped BigOperators Classicalopen scoped BigOperators Classical SchwartzMap ContDiffopen MeasureTheory Setopen scoped BigOperatorsopen scoped BigOperators Classicalopen scoped BigOperators Classicalopen ActualEisensteinCubic UniqueFactorizationMonoidopen scoped BigOperatorsopen scoped BigOperatorsopen scoped BigOperators Classical SchwartzMapopen scoped BigOperators Classicalopen scoped BigOperators Classical ContDiff Topologynamespace CanonicalRowCompletionopen ActualEisensteinCubicopen ConcretePrimeRowBridge hiding Oopen ShortDraftHeckeBridgeopen CanonicalQuadraticSieve hiding Oopen SecondPassArithmetic hiding Oopen SixthPowerAverage CompactMellinBridge InitialMeanSquaretheorem corrected_weighted_mellin_identity {q : โ„•} [NeZero q] (ฯ‡ : DirichletCharacter โ„‚ q) (S : Finset (Ideal ActualEisensteinCubic.O)) (hS : โˆ€PโˆˆS,Prime P) (W : โ„โ†’โ„‚) (hW : ContDiff โ„ โˆž W) (hs : โˆ€x,xโ‰ค1 โˆจ 2โ‰คxโ†’W x=0) (s : โ„‚) (hRe : 2<s.re) : (ฯ‡.LFunction s*(baseChangeChar ฯ‡).LFunction s)* ((finiteEulerFactor ฯ‡ S s*SmoothMobiusCorrection.eulerCorrection ฯ‡ S s)* mellin (fun Z : โ„=>weightedCompactSum ฯ‡ S W Zโปยน) (-s))= mellin W s := q:โ„•instโœ:NeZero qฯ‡:DirichletCharacter โ„‚ qS:Finset (Ideal ActualEisensteinCubic.O)hS:โˆ€ P โˆˆ S, Prime PW:โ„ โ†’ โ„‚hW:ContDiff โ„ โˆž Whs:โˆ€ (x : โ„), x โ‰ค 1 โˆจ 2 โ‰ค x โ†’ W x = 0s:โ„‚hRe:2 < s.reโŠข DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * mellin (fun Z => weightedCompactSum ฯ‡ S W Zโปยน) (-s)) = mellin W s q:โ„•instโœ:NeZero qฯ‡:DirichletCharacter โ„‚ qS:Finset (Ideal ActualEisensteinCubic.O)hS:โˆ€ P โˆˆ S, Prime PW:โ„ โ†’ โ„‚hW:ContDiff โ„ โˆž Whs:โˆ€ (x : โ„), x โ‰ค 1 โˆจ 2 โ‰ค x โ†’ W x = 0s:โ„‚hRe:2 < s.reโŠข DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * (mellin W s * L (weightedCoeff ฯ‡ S) s)) = mellin W s q:โ„•instโœ:NeZero qฯ‡:DirichletCharacter โ„‚ qS:Finset (Ideal ActualEisensteinCubic.O)hS:โˆ€ P โˆˆ S, Prime PW:โ„ โ†’ โ„‚hW:ContDiff โ„ โˆž Whs:โˆ€ (x : โ„), x โ‰ค 1 โˆจ 2 โ‰ค x โ†’ W x = 0s:โ„‚hRe:2 < s.rehc:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) sโŠข DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * (mellin W s * L (weightedCoeff ฯ‡ S) s)) = mellin W s q:โ„•instโœ:NeZero qฯ‡:DirichletCharacter โ„‚ qS:Finset (Ideal ActualEisensteinCubic.O)hS:โˆ€ P โˆˆ S, Prime PW:โ„ โ†’ โ„‚hW:ContDiff โ„ โˆž Whs:โˆ€ (x : โ„), x โ‰ค 1 โˆจ 2 โ‰ค x โ†’ W x = 0s:โ„‚hRe:2 < s.rehc:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) shp:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = L (pairInverseCoeff ฯ‡ (baseChangeChar ฯ‡)) sโŠข DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * (mellin W s * L (weightedCoeff ฯ‡ S) s)) = mellin W s q:โ„•instโœ:NeZero qฯ‡:DirichletCharacter โ„‚ qS:Finset (Ideal ActualEisensteinCubic.O)hS:โˆ€ P โˆˆ S, Prime PW:โ„ โ†’ โ„‚hW:ContDiff โ„ โˆž Whs:โˆ€ (x : โ„), x โ‰ค 1 โˆจ 2 โ‰ค x โ†’ W x = 0s:โ„‚hRe:2 < s.rehc:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) shp:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = L (pairInverseCoeff ฯ‡ (baseChangeChar ฯ‡)) she:DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * L (pairInverseCoeff ฯ‡ (baseChangeChar ฯ‡)) s = 1โŠข DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * (mellin W s * L (weightedCoeff ฯ‡ S) s)) = mellin W s q:โ„•instโœ:NeZero qฯ‡:DirichletCharacter โ„‚ qS:Finset (Ideal ActualEisensteinCubic.O)hS:โˆ€ P โˆˆ S, Prime PW:โ„ โ†’ โ„‚hW:ContDiff โ„ โˆž Whs:โˆ€ (x : โ„), x โ‰ค 1 โˆจ 2 โ‰ค x โ†’ W x = 0s:โ„‚hRe:2 < s.rehc:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) shp:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = L (pairInverseCoeff ฯ‡ (baseChangeChar ฯ‡)) she:DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) s) = 1โŠข DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * (mellin W s * L (weightedCoeff ฯ‡ S) s)) = mellin W s calc _=((ฯ‡.LFunction s*(baseChangeChar ฯ‡).LFunction s)* ((finiteEulerFactor ฯ‡ S s*SmoothMobiusCorrection.eulerCorrection ฯ‡ S s)* LSeries (weightedCoeff ฯ‡ S) s))*mellin W s := q:โ„•instโœ:NeZero qฯ‡:DirichletCharacter โ„‚ qS:Finset (Ideal ActualEisensteinCubic.O)hS:โˆ€ P โˆˆ S, Prime PW:โ„ โ†’ โ„‚hW:ContDiff โ„ โˆž Whs:โˆ€ (x : โ„), x โ‰ค 1 โˆจ 2 โ‰ค x โ†’ W x = 0s:โ„‚hRe:2 < s.rehc:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) shp:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = L (pairInverseCoeff ฯ‡ (baseChangeChar ฯ‡)) she:DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) s) = 1โŠข DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * (mellin W s * L (weightedCoeff ฯ‡ S) s)) = DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) s) * mellin W s All goals completed! ๐Ÿ™ _=mellin W s := q:โ„•instโœ:NeZero qฯ‡:DirichletCharacter โ„‚ qS:Finset (Ideal ActualEisensteinCubic.O)hS:โˆ€ P โˆˆ S, Prime PW:โ„ โ†’ โ„‚hW:ContDiff โ„ โˆž Whs:โˆ€ (x : โ„), x โ‰ค 1 โˆจ 2 โ‰ค x โ†’ W x = 0s:โ„‚hRe:2 < s.rehc:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) shp:L (normFiberCoeff (baseChangeWeight ฯ‡)) s = L (pairInverseCoeff ฯ‡ (baseChangeChar ฯ‡)) she:DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) s) = 1โŠข DirichletCharacter.LFunction ฯ‡ s * DirichletCharacter.LFunction (baseChangeChar ฯ‡) s * (finiteEulerFactor ฯ‡ S s * SmoothMobiusCorrection.eulerCorrection ฯ‡ S s * L (weightedCoeff ฯ‡ S) s) * mellin W s = mellin W s All goals completed! ๐Ÿ™end CanonicalRowCompletionopen scoped BigOperators Classicalnamespace QuadraticAllOddCRTsectionopen ActualEisensteinCubicopen QuadraticGaussRay hiding Oopen ActualEisensteinCoordinates hiding O omegaopen CanonicalQuadraticSieve hiding Olocal instance : (Ideal.span {lambda} : Ideal ActualEisensteinCubic.O).IsMaximal:=lambdaIdeal_maximallemma lambda_odd : ringChar (ActualEisensteinCubic.OโงธIdeal.span {lambda})โ‰ 2:= ActualEisensteinSieve.lambda_residue_oddlemma lambda_residue : residue lambda=((3:ZMod 4),(1:ZMod 4)) := โŠข residue lambda = (3, 1) h:lambda = eval (-1) 1โŠข residue lambda = (3, 1) h:lambda = eval (-1) 1โŠข (โ†‘(-1), โ†‘1) = (3, 1) All goals completed! ๐Ÿ™lemma lambda_quadratic_ray_ne_zero : quadraticRayValue (residue lambda)โ‰ 0 := โŠข quadraticRayValue (residue lambda) โ‰  0 โŠข EisensteinEPrimaryPhase.odd (residue lambda) โŠข EisensteinEPrimaryPhase.odd (3, 1) All goals completed! ๐Ÿ™lemma character_lambda_primary (p : ActualEisensteinCubic.O) (hp : lambda^2โˆฃp-1) : character (Ideal.span {lambda}) (Ideal.Quotient.mk (Ideal.span {lambda}) p)=1 := p:ActualEisensteinCubic.Ohp:lambda ^ 2 โˆฃ p - 1โŠข (character (span {lambda})) ((Ideal.Quotient.mk (span {lambda})) p) = 1 p:ActualEisensteinCubic.Ohp:lambda ^ 2 โˆฃ p - 1hm:(Ideal.Quotient.mk (span {lambda})) p = (Ideal.Quotient.mk (span {lambda})) 1โŠข (character (span {lambda})) ((Ideal.Quotient.mk (span {lambda})) p) = 1 All goals completed! ๐Ÿ™def lambdaQuadraticRay (r : EisensteinEPrimaryPhase.Coord) : โ„‚:= quadraticRayValue (EisensteinEPrimaryPhase.mul (residue lambda) r)/ (quadraticRayValue (residue lambda)*quadraticRayValue r)theorem character_lambda_eq_ray (p : ActualEisensteinCubic.O) (hp : pโ‰ 0) [(Ideal.span {p}).IsMaximal] (hg : lambdaโˆ‰Ideal.span {p}) (hc : ringChar (ActualEisensteinCubic.OโงธIdeal.span {p})โ‰ 2) (hprimary : lambda^2โˆฃp-1) : character (Ideal.span {p}) (Ideal.Quotient.mk (Ideal.span {p}) lambda)= lambdaQuadraticRay (residue p) := p:ActualEisensteinCubic.Ohp:p โ‰  0instโœ:(span {p}).IsMaximalhg:lambda โˆ‰ span {p}hc:ringChar (ActualEisensteinCubic.O โงธ span {p}) โ‰  2hprimary:lambda ^ 2 โˆฃ p - 1โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (residue p) p:ActualEisensteinCubic.Ohp:p โ‰  0instโœ:(span {p}).IsMaximalhg:lambda โˆ‰ span {p}hc:ringChar (ActualEisensteinCubic.O โงธ span {p}) โ‰  2hprimary:lambda ^ 2 โˆฃ p - 1hcop:IsCoprime (span {lambda}) (span {p})โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (residue p) p:ActualEisensteinCubic.Ohp:p โ‰  0instโœ:(span {p}).IsMaximalhg:lambda โˆ‰ span {p}hc:ringChar (ActualEisensteinCubic.O โงธ span {p}) โ‰  2hprimary:lambda ^ 2 โˆฃ p - 1hcop:IsCoprime (span {lambda}) (span {p})h:quadraticRayValue (residue (lambda * p)) = (character (span {lambda})) ((Ideal.Quotient.mk (span {lambda})) p) * (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) * quadraticRayValue (residue lambda) * quadraticRayValue (residue p)โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (residue p) p:ActualEisensteinCubic.Ohp:p โ‰  0instโœ:(span {p}).IsMaximalhg:lambda โˆ‰ span {p}hc:ringChar (ActualEisensteinCubic.O โงธ span {p}) โ‰  2hprimary:lambda ^ 2 โˆฃ p - 1hcop:IsCoprime (span {lambda}) (span {p})h:quadraticRayValue (residue (lambda * p)) = (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) * quadraticRayValue (residue lambda) * quadraticRayValue (residue p)โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (residue p) p:ActualEisensteinCubic.Ohp:p โ‰  0instโœ:(span {p}).IsMaximalhg:lambda โˆ‰ span {p}hc:ringChar (ActualEisensteinCubic.O โงธ span {p}) โ‰  2hprimary:lambda ^ 2 โˆฃ p - 1hcop:IsCoprime (span {lambda}) (span {p})h:quadraticRayValue (residue (lambda * p)) = (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) * quadraticRayValue (residue lambda) * quadraticRayValue (residue p)hodd:EisensteinEPrimaryPhase.odd (residue p)โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (residue p) p:ActualEisensteinCubic.Ohp:p โ‰  0instโœ:(span {p}).IsMaximalhg:lambda โˆ‰ span {p}hc:ringChar (ActualEisensteinCubic.O โงธ span {p}) โ‰  2hprimary:lambda ^ 2 โˆฃ p - 1hcop:IsCoprime (span {lambda}) (span {p})h:quadraticRayValue (residue (lambda * p)) = (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) * quadraticRayValue (residue lambda) * quadraticRayValue (residue p)hodd:EisensteinEPrimaryPhase.odd (residue p)โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = quadraticRayValue (EisensteinEPrimaryPhase.mul (residue lambda) (residue p)) / (quadraticRayValue (residue lambda) * quadraticRayValue (residue p)) p:ActualEisensteinCubic.Ohp:p โ‰  0instโœ:(span {p}).IsMaximalhg:lambda โˆ‰ span {p}hc:ringChar (ActualEisensteinCubic.O โงธ span {p}) โ‰  2hprimary:lambda ^ 2 โˆฃ p - 1hcop:IsCoprime (span {lambda}) (span {p})h:quadraticRayValue (residue (lambda * p)) = (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) * quadraticRayValue (residue lambda) * quadraticRayValue (residue p)hodd:EisensteinEPrimaryPhase.odd (residue p)โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = quadraticRayValue (residue (lambda * p)) / (quadraticRayValue (residue lambda) * quadraticRayValue (residue p)) p:ActualEisensteinCubic.Ohp:p โ‰  0instโœ:(span {p}).IsMaximalhg:lambda โˆ‰ span {p}hc:ringChar (ActualEisensteinCubic.O โงธ span {p}) โ‰  2hprimary:lambda ^ 2 โˆฃ p - 1hcop:IsCoprime (span {lambda}) (span {p})h:quadraticRayValue (residue (lambda * p)) = (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) * quadraticRayValue (residue lambda) * quadraticRayValue (residue p)hodd:EisensteinEPrimaryPhase.odd (residue p)โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) * (quadraticRayValue (residue lambda) * quadraticRayValue (residue p)) = quadraticRayValue (residue (lambda * p)) All goals completed! ๐Ÿ™endopen ActualEisensteinCubicopen QuadraticGaussRay hiding Oopen ActualEisensteinCoordinates hiding O omegadef lambdaQuadraticTable (r : EisensteinEPrimaryPhase.Coord) : โ„ค := if ยฌEisensteinEPrimaryPhase.odd r then 0 else if rโˆˆ({(0,1),(1,0),(1,2),(1,3),(2,3),(3,3)} : Finset EisensteinEPrimaryPhase.Coord) then 1 else -1lemma lambdaQuadraticTable_mul (r s : EisensteinEPrimaryPhase.Coord) : lambdaQuadraticTable (EisensteinEPrimaryPhase.mul r s)= lambdaQuadraticTable r*lambdaQuadraticTable s := r:EisensteinEPrimaryPhase.Coords:EisensteinEPrimaryPhase.CoordโŠข lambdaQuadraticTable (EisensteinEPrimaryPhase.mul r s) = lambdaQuadraticTable r * lambdaQuadraticTable s r:EisensteinEPrimaryPhase.Coords:EisensteinEPrimaryPhase.Coordh:โˆ€ (r s : EisensteinEPrimaryPhase.Coord), lambdaQuadraticTable (EisensteinEPrimaryPhase.mul r s) = lambdaQuadraticTable r * lambdaQuadraticTable sโŠข lambdaQuadraticTable (EisensteinEPrimaryPhase.mul r s) = lambdaQuadraticTable r * lambdaQuadraticTable s All goals completed! ๐Ÿ™lemma lambdaQuadraticTable_eq_ray (r : EisensteinEPrimaryPhase.Coord) (hr : EisensteinEPrimaryPhase.odd r) : (lambdaQuadraticTable r:โ„‚)=lambdaQuadraticRay r := r:EisensteinEPrimaryPhase.Coordhr:EisensteinEPrimaryPhase.odd rโŠข โ†‘(lambdaQuadraticTable r) = lambdaQuadraticRay r r:EisensteinEPrimaryPhase.Coordhr:EisensteinEPrimaryPhase.odd rhcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valโŠข โ†‘(lambdaQuadraticTable r) = lambdaQuadraticRay r r:EisensteinEPrimaryPhase.Coordhr:EisensteinEPrimaryPhase.odd rhcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1โŠข โ†‘(lambdaQuadraticTable r) = lambdaQuadraticRay r hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1a:ZMod 4b:ZMod 4hr:EisensteinEPrimaryPhase.odd (a, b)โŠข โ†‘(lambdaQuadraticTable (a, b)) = lambdaQuadraticRay (a, b) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1a:ZMod 4b:ZMod 4hr:EisensteinEPrimaryPhase.odd (a, b)hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3โŠข โ†‘(lambdaQuadraticTable (a, b)) = lambdaQuadraticRay (a, b) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1b:ZMod 4hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (0, b)โŠข โ†‘(lambdaQuadraticTable (0, b)) = lambdaQuadraticRay (0, b)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1b:ZMod 4hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (1, b)โŠข โ†‘(lambdaQuadraticTable (1, b)) = lambdaQuadraticRay (1, b)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1b:ZMod 4hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (2, b)โŠข โ†‘(lambdaQuadraticTable (2, b)) = lambdaQuadraticRay (2, b)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1b:ZMod 4hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, b)โŠข โ†‘(lambdaQuadraticTable (3, b)) = lambdaQuadraticRay (3, b) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1b:ZMod 4hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (0, b)โŠข โ†‘(lambdaQuadraticTable (0, b)) = lambdaQuadraticRay (0, b)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1b:ZMod 4hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (1, b)โŠข โ†‘(lambdaQuadraticTable (1, b)) = lambdaQuadraticRay (1, b)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1b:ZMod 4hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (2, b)โŠข โ†‘(lambdaQuadraticTable (2, b)) = lambdaQuadraticRay (2, b)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1b:ZMod 4hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, b)โŠข โ†‘(lambdaQuadraticTable (3, b)) = lambdaQuadraticRay (3, b) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, 0)โŠข โ†‘(lambdaQuadraticTable (3, 0)) = lambdaQuadraticRay (3, 0)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, 1)โŠข โ†‘(lambdaQuadraticTable (3, 1)) = lambdaQuadraticRay (3, 1)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, 2)โŠข โ†‘(lambdaQuadraticTable (3, 2)) = lambdaQuadraticRay (3, 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, 3)โŠข โ†‘(lambdaQuadraticTable (3, 3)) = lambdaQuadraticRay (3, 3) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (0, 0)โŠข โ†‘(lambdaQuadraticTable (0, 0)) = lambdaQuadraticRay (0, 0)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (0, 1)โŠข โ†‘(lambdaQuadraticTable (0, 1)) = lambdaQuadraticRay (0, 1)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (0, 2)โŠข โ†‘(lambdaQuadraticTable (0, 2)) = lambdaQuadraticRay (0, 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (0, 3)โŠข โ†‘(lambdaQuadraticTable (0, 3)) = lambdaQuadraticRay (0, 3)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (1, 0)โŠข โ†‘(lambdaQuadraticTable (1, 0)) = lambdaQuadraticRay (1, 0)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (1, 1)โŠข โ†‘(lambdaQuadraticTable (1, 1)) = lambdaQuadraticRay (1, 1)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (1, 2)โŠข โ†‘(lambdaQuadraticTable (1, 2)) = lambdaQuadraticRay (1, 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (1, 3)โŠข โ†‘(lambdaQuadraticTable (1, 3)) = lambdaQuadraticRay (1, 3)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (2, 0)โŠข โ†‘(lambdaQuadraticTable (2, 0)) = lambdaQuadraticRay (2, 0)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (2, 1)โŠข โ†‘(lambdaQuadraticTable (2, 1)) = lambdaQuadraticRay (2, 1)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (2, 2)โŠข โ†‘(lambdaQuadraticTable (2, 2)) = lambdaQuadraticRay (2, 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (2, 3)โŠข โ†‘(lambdaQuadraticTable (2, 3)) = lambdaQuadraticRay (2, 3)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, 0)โŠข โ†‘(lambdaQuadraticTable (3, 0)) = lambdaQuadraticRay (3, 0)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, 1)โŠข โ†‘(lambdaQuadraticTable (3, 1)) = lambdaQuadraticRay (3, 1)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, 2)โŠข โ†‘(lambdaQuadraticTable (3, 2)) = lambdaQuadraticRay (3, 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:EisensteinEPrimaryPhase.odd (3, 3)โŠข โ†‘(lambdaQuadraticTable (3, 3)) = lambdaQuadraticRay (3, 3) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (3, 3)) = lambdaQuadraticRay (3, 3) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (0, 1)) = lambdaQuadraticRay (0, 1)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (0, 3)) = lambdaQuadraticRay (0, 3)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (1, 0)) = lambdaQuadraticRay (1, 0)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (1, 1)) = lambdaQuadraticRay (1, 1)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (1, 2)) = lambdaQuadraticRay (1, 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (1, 3)) = lambdaQuadraticRay (1, 3)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (2, 1)) = lambdaQuadraticRay (2, 1)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (2, 3)) = lambdaQuadraticRay (2, 3)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (3, 0)) = lambdaQuadraticRay (3, 0)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (3, 1)) = lambdaQuadraticRay (3, 1)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (3, 2)) = lambdaQuadraticRay (3, 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข โ†‘(lambdaQuadraticTable (3, 3)) = lambdaQuadraticRay (3, 3) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = -I / ((1 + -I + -I + -1) / 2) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = -I / ((1 + -I + -I + -1) / 2 * ((1 + -I + 1 + I) / 2))hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = (I ^ (-3).cast + I ^ (2 - (-3).cast)) / 2 / ((1 + -I + -I + -1) / 2 * ((1 + I + 1 + -I) / 2))hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = (1 + -I + -I + -1) / 2 / ((1 + -I + -I + -1) / 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = I / ((1 + -I + -I + -1) / 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = -(I * (2 / (1 + -I + -I + -1)))hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = (1 + I + 1 + -I) / 2 / ((1 + -I + -I + -1) / 2 * ((1 + I + I + -1) / 2))hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = I * (2 / (1 + -I + -I + -1))hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = -(I * (2 / (1 + -I + -I + -1)))hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = (1 + I + I + -1) / 2 / ((1 + -I + -I + -1) / 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = (1 + -I + 1 + I) / 2 / ((1 + -I + -I + -1) / 2 * ((1 + -I + -I + -1) / 2))hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = I * (2 / (1 + -I + -I + -1))hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = -I / ((1 + -I + -I + -1) / 2) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = I * Iโปยน hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = I * Iโปยนhcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = I ^ (-3).cast * Iโปยน * (-1 / 2) + I ^ (2 - (-3).cast) * Iโปยน * (-1 / 2)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = I * Iโปยนhcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = -(I * Iโปยน)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = I * Iโปยนhcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = -Iโปยน ^ 2hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = -(I * Iโปยน)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = I * Iโปยนhcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = -(I * Iโปยน)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = Iโปยน ^ 2hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -1 = -(I * Iโปยน)hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข 1 = I * Iโปยน All goals completed! ๐Ÿ™ all_goals hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -2 = I * (I ^ (-3).cast + I ^ (2 - (-3).cast)) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -2 = I * (I ^ 1 + I ^ (2 - 1)) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -2 = I * (I + I) hcmp:โˆ€ (a b : ZMod 4), a = b โ†” a.val = b.valhn3:-3 = 1hcases:โˆ€ (x : ZMod 4), x = 0 โˆจ x = 1 โˆจ x = 2 โˆจ x = 3hr:TrueโŠข -2 = I ^ 2 * 2 All goals completed! ๐Ÿ™def lambdaQuadraticCharacter : ActualEisensteinCubic.Oโ†’*โ„‚ where toFun n:=(lambdaQuadraticTable (residue n):โ„‚) map_one' := โŠข โ†‘(lambdaQuadraticTable (residue 1)) = 1 h:residue 1 = (1, 0)โŠข โ†‘(lambdaQuadraticTable (residue 1)) = 1 h:residue 1 = (1, 0)โŠข โ†‘(lambdaQuadraticTable (1, 0)) = 1 exact_mod_cast (show lambdaQuadraticTable ((1:ZMod 4),0)=1 from h:residue 1 = (1, 0)โŠข lambdaQuadraticTable (1, 0) = 1 All goals completed! ๐Ÿ™) map_mul' x y := x:ActualEisensteinCubic.Oy:ActualEisensteinCubic.OโŠข โ†‘(lambdaQuadraticTable (residue (x * y))) = โ†‘(lambdaQuadraticTable (residue x)) * โ†‘(lambdaQuadraticTable (residue y)) x:ActualEisensteinCubic.Oy:ActualEisensteinCubic.OโŠข โ†‘(lambdaQuadraticTable (residue x) * lambdaQuadraticTable (residue y)) = โ†‘(lambdaQuadraticTable (residue x)) * โ†‘(lambdaQuadraticTable (residue y)) x:ActualEisensteinCubic.Oy:ActualEisensteinCubic.OโŠข โ†‘(lambdaQuadraticTable (residue x)) * โ†‘(lambdaQuadraticTable (residue y)) = โ†‘(lambdaQuadraticTable (residue x)) * โ†‘(lambdaQuadraticTable (residue y)) All goals completed! ๐Ÿ™lemma lambdaQuadraticCharacter_periodic (x y : ActualEisensteinCubic.O) (h : (4:ActualEisensteinCubic.O)โˆฃx-y) : lambdaQuadraticCharacter x=lambdaQuadraticCharacter y := x:ActualEisensteinCubic.Oy:ActualEisensteinCubic.Oh:4 โˆฃ x - yโŠข lambdaQuadraticCharacter x = lambdaQuadraticCharacter y x:ActualEisensteinCubic.Oy:ActualEisensteinCubic.Oh:4 โˆฃ x - yโŠข โ†‘(lambdaQuadraticTable (residue x)) = โ†‘(lambdaQuadraticTable (residue y)) All goals completed! ๐Ÿ™end QuadraticAllOddCRTopen scoped BigOperators Classicalnamespace CanonicalRowCompletionopen ActualEisensteinCubicopen CompletedGauss hiding Oopen CubicJacobiGlobal hiding Oopen QuadraticAllOddCRTopen CanonicalQuadraticSieve hiding Oopen ConcreteTraceCRT (eisEmbedding)open UniqueFactorizationMonoidlemma localRowValue_square (x : ActualEisensteinCubic.O) (P : Ideal ActualEisensteinCubic.O) : localRowValue x P^2=eisEmbedding (primeValue P x) := x:ActualEisensteinCubic.OP:Ideal ActualEisensteinCubic.OโŠข localRowValue x P ^ 2 = eisEmbedding (primeValue P x) x:ActualEisensteinCubic.OP:Ideal ActualEisensteinCubic.OโŠข (if h : P.IsMaximal โˆง lambda โˆ‰ P then (actualSextic P โ‹ฏ) ((Ideal.Quotient.mk P) x) else 0) ^ 2 = eisEmbedding (if h : P.IsMaximal โˆง lambda โˆ‰ P then (cubicChar P โ‹ฏ) ((Ideal.Quotient.mk P) x) else 0) x:ActualEisensteinCubic.OP:Ideal ActualEisensteinCubic.Oh:P.IsMaximal โˆง lambda โˆ‰ PโŠข (actualSextic P โ‹ฏ) ((Ideal.Quotient.mk P) x) ^ 2 = eisEmbedding ((cubicChar P โ‹ฏ) ((Ideal.Quotient.mk P) x))x:ActualEisensteinCubic.OP:Ideal ActualEisensteinCubic.Oh:ยฌ(P.IsMaximal โˆง lambda โˆ‰ P)โŠข 0 ^ 2 = eisEmbedding 0 x:ActualEisensteinCubic.OP:Ideal ActualEisensteinCubic.Oh:P.IsMaximal โˆง lambda โˆ‰ PโŠข (actualSextic P โ‹ฏ) ((Ideal.Quotient.mk P) x) ^ 2 = eisEmbedding ((cubicChar P โ‹ฏ) ((Ideal.Quotient.mk P) x)) x:ActualEisensteinCubic.OP:Ideal ActualEisensteinCubic.Oh:P.IsMaximal โˆง lambda โˆ‰ Pthis:P.IsMaximal := ยทยทยทโŠข (actualSextic P โ‹ฏ) ((Ideal.Quotient.mk P) x) ^ 2 = eisEmbedding ((cubicChar P โ‹ฏ) ((Ideal.Quotient.mk P) x)) x:ActualEisensteinCubic.OP:Ideal ActualEisensteinCubic.Oh:P.IsMaximal โˆง lambda โˆ‰ Pthis:P.IsMaximal := ยทยทยทโŠข (actualSextic P โ‹ฏ) ((Ideal.Quotient.mk P) x) ^ 2 = eisEmbedding ((cubicChar P โ‹ฏ) ((Ideal.Quotient.mk P) x)) x:ActualEisensteinCubic.OP:Ideal ActualEisensteinCubic.Oh:P.IsMaximal โˆง lambda โˆ‰ Pthis:P.IsMaximal := ยทยทยทโŠข ((cubicChar P โ‹ฏ).ringHomComp eisEmbedding) ((Ideal.Quotient.mk P) x) = eisEmbedding ((cubicChar P โ‹ฏ) ((Ideal.Quotient.mk P) x)) All goals completed! ๐Ÿ™ x:ActualEisensteinCubic.OP:Ideal ActualEisensteinCubic.Oh:ยฌ(P.IsMaximal โˆง lambda โˆ‰ P)โŠข 0 ^ 2 = eisEmbedding 0 All goals completed! ๐Ÿ™theorem idealRowHom_square (x : ActualEisensteinCubic.O) (I : Ideal ActualEisensteinCubic.O) : idealRowHom x I^2=eisEmbedding (idealSymbol I x) := x:ActualEisensteinCubic.OI:Ideal ActualEisensteinCubic.OโŠข (idealRowHom x) I ^ 2 = eisEmbedding (idealSymbol I x) x:ActualEisensteinCubic.OI:Ideal ActualEisensteinCubic.Ohm:โˆ€ (s : Multiset (Ideal ActualEisensteinCubic.O)), (Multiset.map (localRowValue x) s).prod ^ 2 = eisEmbedding (Multiset.map (fun P => primeValue P x) s).prodโŠข (idealRowHom x) I ^ 2 = eisEmbedding (idealSymbol I x) x:ActualEisensteinCubic.OI:Ideal ActualEisensteinCubic.Ohm:โˆ€ (s : Multiset (Ideal ActualEisensteinCubic.O)), (Multiset.map (localRowValue x) s).prod ^ 2 = eisEmbedding (Multiset.map (fun P => primeValue P x) s).prodhI:I = 0โŠข (idealRowHom x) I ^ 2 = eisEmbedding (idealSymbol I x)x:ActualEisensteinCubic.OI:Ideal ActualEisensteinCubic.Ohm:โˆ€ (s : Multiset (Ideal ActualEisensteinCubic.O)), (Multiset.map (localRowValue x) s).prod ^ 2 = eisEmbedding (Multiset.map (fun P => primeValue P x) s).prodhI:ยฌI = 0โŠข (idealRowHom x) I ^ 2 = eisEmbedding (idealSymbol I x) x:ActualEisensteinCubic.OI:Ideal ActualEisensteinCubic.Ohm:โˆ€ (s : Multiset (Ideal ActualEisensteinCubic.O)), (Multiset.map (localRowValue x) s).prod ^ 2 = eisEmbedding (Multiset.map (fun P => primeValue P x) s).prodhI:I = 0โŠข (idealRowHom x) I ^ 2 = eisEmbedding (idealSymbol I x) x:ActualEisensteinCubic.Ohm:โˆ€ (s : Multiset (Ideal ActualEisensteinCubic.O)), (Multiset.map (localRowValue x) s).prod ^ 2 = eisEmbedding (Multiset.map (fun P => primeValue P x) s).prodโŠข (idealRowHom x) 0 ^ 2 = eisEmbedding (idealSymbol 0 x) All goals completed! ๐Ÿ™ x:ActualEisensteinCubic.OI:Ideal ActualEisensteinCubic.Ohm:โˆ€ (s : Multiset (Ideal ActualEisensteinCubic.O)), (Multiset.map (localRowValue x) s).prod ^ 2 = eisEmbedding (Multiset.map (fun P => primeValue P x) s).prodhI:ยฌI = 0โŠข (idealRowHom x) I ^ 2 = eisEmbedding (idealSymbol I x) x:ActualEisensteinCubic.OI:Ideal ActualEisensteinCubic.Ohm:โˆ€ (s : Multiset (Ideal ActualEisensteinCubic.O)), (Multiset.map (localRowValue x) s).prod ^ 2 = eisEmbedding (Multiset.map (fun P => primeValue P x) s).prodhI:ยฌI = 0โŠข (if I = 0 then 0 else (Multiset.map (localRowValue x) (normalizedFactors I)).prod) ^ 2 = eisEmbedding (if I = 0 then 0 else (Multiset.map (fun P => primeValue P x) (normalizedFactors I)).prod) x:ActualEisensteinCubic.OI:Ideal ActualEisensteinCubic.Ohm:โˆ€ (s : Multiset (Ideal ActualEisensteinCubic.O)), (Multiset.map (localRowValue x) s).prod ^ 2 = eisEmbedding (Multiset.map (fun P => primeValue P x) s).prodhI:ยฌI = 0โŠข (Multiset.map (localRowValue x) (normalizedFactors I)).prod ^ 2 = eisEmbedding (Multiset.map (fun P => primeValue P x) (normalizedFactors I)).prod All goals completed! ๐Ÿ™lemma actualSextic_cube_quadratic (P : Ideal ActualEisensteinCubic.O) [P.IsMaximal] (hg : lambdaโˆ‰P) : actualSextic P hg^3=character P := P:Ideal ActualEisensteinCubic.Oinstโœ:P.IsMaximalhg:lambda โˆ‰ PโŠข actualSextic P hg ^ 3 = character P P:Ideal ActualEisensteinCubic.Oinstโœ:P.IsMaximalhg:lambda โˆ‰ Pthis:Field (ActualEisensteinCubic.O โงธ P) := Quotient.field PโŠข actualSextic P hg ^ 3 = character P P:Ideal ActualEisensteinCubic.Oinstโœ:P.IsMaximalhg:lambda โˆ‰ Pthisโœ:Field (ActualEisensteinCubic.O โงธ P) := Quotient.field Pthis:Fintype (ActualEisensteinCubic.O โงธ P) := Fintype.ofFinite (ActualEisensteinCubic.O โงธ P)โŠข actualSextic P hg ^ 3 = character P P:Ideal ActualEisensteinCubic.Oinstโœ:P.IsMaximalhg:lambda โˆ‰ Pthisโœ:Field (ActualEisensteinCubic.O โงธ P) := Quotient.field Pthis:Fintype (ActualEisensteinCubic.O โงธ P) := Fintype.ofFinite (ActualEisensteinCubic.O โงธ P)ฯ‡:MulChar (ActualEisensteinCubic.O โงธ P) ActualEisensteinCubic.Ohฯ‡:actualSextic P hg = ฯ‡.ringHomComp eisEmbeddinghฯ‡3:ฯ‡ ^ 3 = (quadraticChar (ActualEisensteinCubic.O โงธ P)).ringHomComp (Int.castRingHom ActualEisensteinCubic.O)โŠข actualSextic P hg ^ 3 = character P P:Ideal ActualEisensteinCubic.Oinstโœ:P.IsMaximalhg:lambda โˆ‰ Pthisโœ:Field (ActualEisensteinCubic.O โงธ P) := Quotient.field Pthis:Fintype (ActualEisensteinCubic.O โงธ P) := Fintype.ofFinite (ActualEisensteinCubic.O โงธ P)ฯ‡:MulChar (ActualEisensteinCubic.O โงธ P) ActualEisensteinCubic.Ohฯ‡:actualSextic P hg = ฯ‡.ringHomComp eisEmbeddinghฯ‡3:ฯ‡ ^ 3 = (quadraticChar (ActualEisensteinCubic.O โงธ P)).ringHomComp (Int.castRingHom ActualEisensteinCubic.O)โŠข ((quadraticChar (ActualEisensteinCubic.O โงธ P)).ringHomComp (Int.castRingHom ActualEisensteinCubic.O)).ringHomComp eisEmbedding = character P P:Ideal ActualEisensteinCubic.Oinstโœ:P.IsMaximalhg:lambda โˆ‰ Pthisโœ:Field (ActualEisensteinCubic.O โงธ P) := Quotient.field Pthis:Fintype (ActualEisensteinCubic.O โงธ P) := Fintype.ofFinite (ActualEisensteinCubic.O โงธ P)ฯ‡:MulChar (ActualEisensteinCubic.O โงธ P) ActualEisensteinCubic.Ohฯ‡:actualSextic P hg = ฯ‡.ringHomComp eisEmbeddinghฯ‡3:ฯ‡ ^ 3 = (quadraticChar (ActualEisensteinCubic.O โงธ P)).ringHomComp (Int.castRingHom ActualEisensteinCubic.O)x:(ActualEisensteinCubic.O โงธ P)หฃโŠข (((quadraticChar (ActualEisensteinCubic.O โงธ P)).ringHomComp (Int.castRingHom ActualEisensteinCubic.O)).ringHomComp eisEmbedding) โ†‘x = (character P) โ†‘x P:Ideal ActualEisensteinCubic.Oinstโœ:P.IsMaximalhg:lambda โˆ‰ Pthisโœ:Field (ActualEisensteinCubic.O โงธ P) := Quotient.field Pthis:Fintype (ActualEisensteinCubic.O โงธ P) := Fintype.ofFinite (ActualEisensteinCubic.O โงธ P)ฯ‡:MulChar (ActualEisensteinCubic.O โงธ P) ActualEisensteinCubic.Ohฯ‡:actualSextic P hg = ฯ‡.ringHomComp eisEmbeddinghฯ‡3:ฯ‡ ^ 3 = (quadraticChar (ActualEisensteinCubic.O โงธ P)).ringHomComp (Int.castRingHom ActualEisensteinCubic.O)x:(ActualEisensteinCubic.O โงธ P)หฃโŠข eisEmbedding โ†‘((quadraticChar (ActualEisensteinCubic.O โงธ P)) โ†‘x) = โ†‘((quadraticChar (ActualEisensteinCubic.O โงธ P)) โ†‘x) All goals completed! ๐Ÿ™lemma idealRowHom_lambda_prime_cube (p : ActualEisensteinCubic.O) (hp : Prime p) (hprimary : lambda^2โˆฃp-1) (hs : Supported (Ideal.span {p})) : idealRowHom lambda (Ideal.span {p})^3=lambdaQuadraticCharacter p := p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})โŠข (idealRowHom lambda) (span {p}) ^ 3 = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทโŠข (idealRowHom lambda) (span {p}) ^ 3 = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})โŠข (idealRowHom lambda) (span {p}) ^ 3 = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})hg:lambda โˆ‰ span {p}hc:ringChar (CanonicalQuadraticSieve.O โงธ span {p}) โ‰  2โŠข (idealRowHom lambda) (span {p}) ^ 3 = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})hg:lambda โˆ‰ span {p}hc:ringChar (CanonicalQuadraticSieve.O โงธ span {p}) โ‰  2โŠข (actualSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) lambda) ^ 3 = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})hg:lambda โˆ‰ span {p}hc:ringChar (CanonicalQuadraticSieve.O โงธ span {p}) โ‰  2โŠข (actualSextic (span {p}) hg) ((Ideal.Quotient.mk (span {p})) lambda) ^ 3 = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})hg:lambda โˆ‰ span {p}hc:ringChar (CanonicalQuadraticSieve.O โงธ span {p}) โ‰  2โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})hg:lambda โˆ‰ span {p}hc:ringChar (CanonicalQuadraticSieve.O โงธ span {p}) โ‰  2he:(character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (ActualEisensteinCoordinates.residue p)โŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})hg:lambda โˆ‰ span {p}hc:ringChar (CanonicalQuadraticSieve.O โงธ span {p}) โ‰  2he:(character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (ActualEisensteinCoordinates.residue p)ho:EisensteinEPrimaryPhase.odd (ActualEisensteinCoordinates.residue p) โ†” ยฌ2 โˆฃ pโŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})hg:lambda โˆ‰ span {p}hc:ringChar (CanonicalQuadraticSieve.O โงธ span {p}) โ‰  2he:(character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (ActualEisensteinCoordinates.residue p)ho:EisensteinEPrimaryPhase.odd (ActualEisensteinCoordinates.residue p) โ†” ยฌ2 โˆฃ phs':ยฌlambda โˆฃ p โˆง ยฌ2 โˆฃ pโŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})hg:lambda โˆ‰ span {p}hc:ringChar (CanonicalQuadraticSieve.O โงธ span {p}) โ‰  2he:(character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (ActualEisensteinCoordinates.residue p)ho:EisensteinEPrimaryPhase.odd (ActualEisensteinCoordinates.residue p) โ†” ยฌ2 โˆฃ phs':ยฌlambda โˆฃ p โˆง ยฌ2 โˆฃ pโŠข (character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticCharacter p p:ActualEisensteinCubic.Ohp:Prime phprimary:lambda ^ 2 โˆฃ p - 1hs:Supported (span {p})this:(span {p}).IsMaximal := ยทยทยทhmem:span {p} โˆˆ normalizedFactors (span {p})hg:lambda โˆ‰ span {p}hc:ringChar (CanonicalQuadraticSieve.O โงธ span {p}) โ‰  2he:(character (span {p})) ((Ideal.Quotient.mk (span {p})) lambda) = lambdaQuadraticRay (ActualEisensteinCoordinates.residue p)ho:EisensteinEPrimaryPhase.odd (ActualEisensteinCoordinates.residue p) โ†” ยฌ2 โˆฃ phs':ยฌlambda โˆฃ p โˆง ยฌ2 โˆฃ pโŠข lambdaQuadraticRay (ActualEisensteinCoordinates.residue p) = lambdaQuadraticCharacter p All goals completed! ๐Ÿ™theorem idealRowHom_lambda_cube (y : ActualEisensteinCubic.O) (hy : lambda^2โˆฃy-1) (hs : Supported (Ideal.span {y})) : idealRowHom lambda (Ideal.span {y})^3=lambdaQuadraticCharacter y := y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})โŠข (idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter y y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})hy0:y โ‰  0โŠข (idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter y y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})hy0:y โ‰  0s:Multiset ActualEisensteinCubic.Ohprod:s.prod = yhfactors:โˆ€ r โˆˆ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1โŠข (idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter y y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hy0:y โ‰  0s:Multiset ActualEisensteinCubic.Ohs:Supported (span {s.prod})hprod:s.prod = yhfactors:โˆ€ r โˆˆ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1โŠข (idealRowHom lambda) (span {s.prod}) ^ 3 = lambdaQuadraticCharacter s.prod s:Multiset ActualEisensteinCubic.Ohs:Supported (span {s.prod})hfactors:โˆ€ r โˆˆ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1โŠข (idealRowHom lambda) (span {s.prod}) ^ 3 = lambdaQuadraticCharacter s.prod induction s using Multiset.induction_on with hs:Supported (span {Multiset.prod 0})hfactors:โˆ€ r โˆˆ 0, Prime r โˆง lambda ^ 2 โˆฃ r - 1โŠข (idealRowHom lambda) (span {Multiset.prod 0}) ^ 3 = lambdaQuadraticCharacter (Multiset.prod 0) All goals completed! ๐Ÿ™ p:ActualEisensteinCubic.Os:Multiset ActualEisensteinCubic.Oih:Supported (span {s.prod}) โ†’ (โˆ€ r โˆˆ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1) โ†’ (idealRowHom lambda) (span {s.prod}) ^ 3 = lambdaQuadraticCharacter s.prodhs:Supported (span {(p ::โ‚˜ s).prod})hfactors:โˆ€ r โˆˆ p ::โ‚˜ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1โŠข (idealRowHom lambda) (span {(p ::โ‚˜ s).prod}) ^ 3 = lambdaQuadraticCharacter (p ::โ‚˜ s).prod p:ActualEisensteinCubic.Os:Multiset ActualEisensteinCubic.Oih:Supported (span {s.prod}) โ†’ (โˆ€ r โˆˆ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1) โ†’ (idealRowHom lambda) (span {s.prod}) ^ 3 = lambdaQuadraticCharacter s.prodhs:Supported (span {(p ::โ‚˜ s).prod})hfactors:โˆ€ r โˆˆ p ::โ‚˜ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1hp:Prime p โˆง lambda ^ 2 โˆฃ p - 1โŠข (idealRowHom lambda) (span {(p ::โ‚˜ s).prod}) ^ 3 = lambdaQuadraticCharacter (p ::โ‚˜ s).prod p:ActualEisensteinCubic.Os:Multiset ActualEisensteinCubic.Oih:Supported (span {s.prod}) โ†’ (โˆ€ r โˆˆ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1) โ†’ (idealRowHom lambda) (span {s.prod}) ^ 3 = lambdaQuadraticCharacter s.prodhs:Supported (span {(p ::โ‚˜ s).prod})hfactors:โˆ€ r โˆˆ p ::โ‚˜ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1hp:Prime p โˆง lambda ^ 2 โˆฃ p - 1htail:โˆ€ q โˆˆ s, Prime q โˆง lambda ^ 2 โˆฃ q - 1โŠข (idealRowHom lambda) (span {(p ::โ‚˜ s).prod}) ^ 3 = lambdaQuadraticCharacter (p ::โ‚˜ s).prod p:ActualEisensteinCubic.Os:Multiset ActualEisensteinCubic.Oih:Supported (span {s.prod}) โ†’ (โˆ€ r โˆˆ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1) โ†’ (idealRowHom lambda) (span {s.prod}) ^ 3 = lambdaQuadraticCharacter s.prodhs:Supported (span {(p ::โ‚˜ s).prod})hfactors:โˆ€ r โˆˆ p ::โ‚˜ s, Prime r โˆง lambda ^ 2 โˆฃ r - 1hp:Prime p โˆง lambda ^ 2 โˆฃ p - 1htail:โˆ€ q โˆˆ s, Prime q โˆง lambda ^ 2 โˆฃ q - 1hsplit:Supported (span {p}) โˆง Supported (span {s.prod})โŠข (idealRowHom lambda) (span {(p ::โ‚˜ s).prod}) ^ 3 = lambdaQuadraticCharacter (p ::โ‚˜ s).prod All goals completed! ๐Ÿ™theorem idealRowHom_lambda_formula (y : ActualEisensteinCubic.O) (hy : lambda^2โˆฃy-1) (hs : Supported (Ideal.span {y})) : idealRowHom lambda (Ideal.span {y})= eisEmbedding (CubicRamified.linearRay 1 0 y)^2*lambdaQuadraticCharacter y := y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})โŠข (idealRowHom lambda) (span {y}) = eisEmbedding (CubicRamified.linearRay 1 0 y) ^ 2 * lambdaQuadraticCharacter y y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (idealSymbol (span {y}) lambda)โŠข (idealRowHom lambda) (span {y}) = eisEmbedding (CubicRamified.linearRay 1 0 y) ^ 2 * lambdaQuadraticCharacter y y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (symbol lambda y)โŠข (idealRowHom lambda) (span {y}) = eisEmbedding (CubicRamified.linearRay 1 0 y) ^ 2 * lambdaQuadraticCharacter y y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (CubicRamified.linearRay 1 0 y)โŠข (idealRowHom lambda) (span {y}) = eisEmbedding (CubicRamified.linearRay 1 0 y) ^ 2 * lambdaQuadraticCharacter y y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (CubicRamified.linearRay 1 0 y)hthree:(idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter yโŠข (idealRowHom lambda) (span {y}) = eisEmbedding (CubicRamified.linearRay 1 0 y) ^ 2 * lambdaQuadraticCharacter y y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (CubicRamified.linearRay 1 0 y)hthree:(idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter yhq:lambdaQuadraticCharacter y ^ 2 = 1โŠข (idealRowHom lambda) (span {y}) = eisEmbedding (CubicRamified.linearRay 1 0 y) ^ 2 * lambdaQuadraticCharacter y y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (CubicRamified.linearRay 1 0 y)hthree:(idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter yhq:lambdaQuadraticCharacter y ^ 2 = 1hsix:(idealRowHom lambda) (span {y}) ^ 6 = 1โŠข (idealRowHom lambda) (span {y}) = eisEmbedding (CubicRamified.linearRay 1 0 y) ^ 2 * lambdaQuadraticCharacter y calc _ = (idealRowHom lambda (Ideal.span {y})^2)^2*(idealRowHom lambda (Ideal.span {y})^3):=y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (CubicRamified.linearRay 1 0 y)hthree:(idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter yhq:lambdaQuadraticCharacter y ^ 2 = 1hsix:(idealRowHom lambda) (span {y}) ^ 6 = 1โŠข (idealRowHom lambda) (span {y}) = ((idealRowHom lambda) (span {y}) ^ 2) ^ 2 * (idealRowHom lambda) (span {y}) ^ 3 calc _ = idealRowHom lambda (Ideal.span {y})*idealRowHom lambda (Ideal.span {y})^6:=y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (CubicRamified.linearRay 1 0 y)hthree:(idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter yhq:lambdaQuadraticCharacter y ^ 2 = 1hsix:(idealRowHom lambda) (span {y}) ^ 6 = 1โŠข (idealRowHom lambda) (span {y}) = (idealRowHom lambda) (span {y}) * (idealRowHom lambda) (span {y}) ^ 6 All goals completed! ๐Ÿ™ _ = _:=y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (CubicRamified.linearRay 1 0 y)hthree:(idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter yhq:lambdaQuadraticCharacter y ^ 2 = 1hsix:(idealRowHom lambda) (span {y}) ^ 6 = 1โŠข (idealRowHom lambda) (span {y}) * (idealRowHom lambda) (span {y}) ^ 6 = ((idealRowHom lambda) (span {y}) ^ 2) ^ 2 * (idealRowHom lambda) (span {y}) ^ 3 All goals completed! ๐Ÿ™ _ = _:=y:ActualEisensteinCubic.Ohy:lambda ^ 2 โˆฃ y - 1hs:Supported (span {y})htwo:(idealRowHom lambda) (span {y}) ^ 2 = eisEmbedding (CubicRamified.linearRay 1 0 y)hthree:(idealRowHom lambda) (span {y}) ^ 3 = lambdaQuadraticCharacter yhq:lambdaQuadraticCharacter y ^ 2 = 1hsix:(idealRowHom lambda) (span {y}) ^ 6 = 1โŠข ((idealRowHom lambda) (span {y}) ^ 2) ^ 2 * (idealRowHom lambda) (span {y}) ^ 3 = eisEmbedding (CubicRamified.linearRay 1 0 y) ^ 2 * lambdaQuadraticCharacter y All goals completed! ๐Ÿ™theorem idealRowHom_lambda_mod_thirty_six (x y : ActualEisensteinCubic.O) (hx : lambda^2โˆฃx-1) (hy : lambda^2โˆฃy-1) (hsx : Supported (Ideal.span {x})) (hsy : Supported (Ideal.span {y})) (hxy : (36:ActualEisensteinCubic.O)โˆฃx-y) : idealRowHom lambda (Ideal.span {x})=idealRowHom lambda (Ideal.span {y}) := x:ActualEisensteinCubic.Oy:ActualEisensteinCubic.Ohx:lambda ^ 2 โˆฃ x - 1hy:lambda ^ 2 โˆฃ y - 1hsx:Supported (span {x})hsy:Supported (span {y})hxy:36 โˆฃ x - yโŠข (idealRowHom lambda) (span {x}) = (idealRowHom lambda) (span {y}) All goals completed! ๐Ÿ™end CanonicalRowCompletionnamespace CubicEisensteinsectionopen Filter MeasureTheoryopen scoped BigOperators Classical Topology ContDiff MatrixGroupsopen ActualEisensteinCubic ConcreteTraceCRTlocal notation "O" => ActualEisensteinCubic.Olemma cuspRemainder_absolute_chart (a b : โ„) (ha : 1โ‰คa) (hab : a<b) (s : โ„‚) (hs : 4<s.re) (M : SL(2,ActualEisensteinCubic.O)) (z : โ„‚) (hz : โ€–zโ€–โ‰ค1) (v : โ„) (hv : 1/2โ‰คv) (hv0 : 0<v) : Summable (fun r : CuspCosets => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–) โˆง (โˆ‘'r : CuspCosets,โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–)โ‰คeisensteinRemainderBound b s := a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vโŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vG:(Fin 2 ร— Fin 2 โ†’ โ„ค) โ†’ โ„ := fun n => max 5 (2 * b) ^ s.re * โ€–nโ€– ^ (-s.re)โŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vG:(Fin 2 ร— Fin 2 โ†’ โ„ค) โ†’ โ„ := fun n => max 5 (2 * b) ^ s.re * โ€–nโ€– ^ (-s.re)f:CuspCosets โ†’ Fin 2 ร— Fin 2 โ†’ โ„ค := fun r => rowCoordinates (translatedCuspRow M r)โŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vG:(Fin 2 ร— Fin 2 โ†’ โ„ค) โ†’ โ„ := fun n => max 5 (2 * b) ^ s.re * โ€–nโ€– ^ (-s.re)f:CuspCosets โ†’ Fin 2 ร— Fin 2 โ†’ โ„ค := fun r => rowCoordinates (translatedCuspRow M r)R:CuspCosets โ†’ โ„ := fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–โŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vG:(Fin 2 ร— Fin 2 โ†’ โ„ค) โ†’ โ„ := fun n => max 5 (2 * b) ^ s.re * โ€–nโ€– ^ (-s.re)f:CuspCosets โ†’ Fin 2 ร— Fin 2 โ†’ โ„ค := fun r => rowCoordinates (translatedCuspRow M r)R:CuspCosets โ†’ โ„ := fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–hg:Summable GโŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vG:(Fin 2 ร— Fin 2 โ†’ โ„ค) โ†’ โ„ := fun n => max 5 (2 * b) ^ s.re * โ€–nโ€– ^ (-s.re)f:CuspCosets โ†’ Fin 2 ร— Fin 2 โ†’ โ„ค := fun r => rowCoordinates (translatedCuspRow M r)R:CuspCosets โ†’ โ„ := fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–hg:Summable Ghi:Function.Injective fโŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vG:(Fin 2 ร— Fin 2 โ†’ โ„ค) โ†’ โ„ := fun n => max 5 (2 * b) ^ s.re * โ€–nโ€– ^ (-s.re)f:CuspCosets โ†’ Fin 2 ร— Fin 2 โ†’ โ„ค := fun r => rowCoordinates (translatedCuspRow M r)R:CuspCosets โ†’ โ„ := fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–hg:Summable Ghi:Function.Injective fhb:โˆ€ (r : CuspCosets), R r โ‰ค G (f r)โŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vG:(Fin 2 ร— Fin 2 โ†’ โ„ค) โ†’ โ„ := fun n => max 5 (2 * b) ^ s.re * โ€–nโ€– ^ (-s.re)f:CuspCosets โ†’ Fin 2 ร— Fin 2 โ†’ โ„ค := fun r => rowCoordinates (translatedCuspRow M r)R:CuspCosets โ†’ โ„ := fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–hg:Summable Ghi:Function.Injective fhb:โˆ€ (r : CuspCosets), R r โ‰ค G (f r)hr:Summable RโŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vG:(Fin 2 ร— Fin 2 โ†’ โ„ค) โ†’ โ„ := fun n => max 5 (2 * b) ^ s.re * โ€–nโ€– ^ (-s.re)f:CuspCosets โ†’ Fin 2 ร— Fin 2 โ†’ โ„ค := fun r => rowCoordinates (translatedCuspRow M r)R:CuspCosets โ†’ โ„ := fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–hg:Summable Ghi:Function.Injective fhb:โˆ€ (r : CuspCosets), R r โ‰ค G (f r)hr:Summable RโŠข โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.reM:SL(2, O)z:โ„‚hz:โ€–zโ€– โ‰ค 1v:โ„hv:1 / 2 โ‰ค vhv0:0 < vG:(Fin 2 ร— Fin 2 โ†’ โ„ค) โ†’ โ„ := fun n => max 5 (2 * b) ^ s.re * โ€–nโ€– ^ (-s.re)f:CuspCosets โ†’ Fin 2 ร— Fin 2 โ†’ โ„ค := fun r => rowCoordinates (translatedCuspRow M r)R:CuspCosets โ†’ โ„ := fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€–hg:Summable Ghi:Function.Injective fhb:โˆ€ (r : CuspCosets), R r โ‰ค G (f r)hr:Summable Rhsum:โˆ‘' (r : CuspCosets), R r โ‰ค โˆ‘' (n : Fin 2 ร— Fin 2 โ†’ โ„ค), G nโŠข โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix M โ€ข upperPoint z v hv0))โ€– โ‰ค eisensteinRemainderBound b s All goals completed! ๐Ÿ™theorem cuspRemainder_absolute_bound (a b : โ„) (ha : 1โ‰คa) (hab : a<b) (s : โ„‚) (hs : 4<s.re) (w : HyperbolicSpace) : Summable (fun r : CuspCosets => โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€–) โˆง (โˆ‘'r : CuspCosets,โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€–)โ‰คeisensteinRemainderBound b s := a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.rew:HyperbolicSpaceโŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.rew:HyperbolicSpaceM:SL(2, O)z:โ„‚v:โ„hv:0 < vhMw:integralComplexMatrix M โ€ข w = upperPoint z v hvhz:normSq z โ‰ค 1 / 3hfloor:โˆš(2 / 3) โ‰ค vโŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.rew:HyperbolicSpaceM:SL(2, O)z:โ„‚v:โ„hv:0 < vhMw:integralComplexMatrix M โ€ข w = upperPoint z v hvhz:normSq z โ‰ค 1 / 3hfloor:โˆš(2 / 3) โ‰ค vhz1:โ€–zโ€– โ‰ค 1โŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.rew:HyperbolicSpaceM:SL(2, O)z:โ„‚v:โ„hv:0 < vhMw:integralComplexMatrix M โ€ข w = upperPoint z v hvhz:normSq z โ‰ค 1 / 3hfloor:โˆš(2 / 3) โ‰ค vhz1:โ€–zโ€– โ‰ค 1hv1:1 / 2 โ‰ค vโŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.rew:HyperbolicSpaceM:SL(2, O)z:โ„‚v:โ„hv:0 < vhMw:integralComplexMatrix M โ€ข w = upperPoint z v hvhz:normSq z โ‰ค 1 / 3hfloor:โˆš(2 / 3) โ‰ค vhz1:โ€–zโ€– โ‰ค 1hv1:1 / 2 โ‰ค vhw:w = integralComplexMatrix Mโปยน โ€ข upperPoint z v hvโŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r w)โ€– โ‰ค eisensteinRemainderBound b s a:โ„b:โ„ha:1 โ‰ค ahab:a < bs:โ„‚hs:4 < s.rew:HyperbolicSpaceM:SL(2, O)z:โ„‚v:โ„hv:0 < vhMw:integralComplexMatrix M โ€ข w = upperPoint z v hvhz:normSq z โ‰ค 1 / 3hfloor:โˆš(2 / 3) โ‰ค vhz1:โ€–zโ€– โ‰ค 1hv1:1 / 2 โ‰ค vhw:w = integralComplexMatrix Mโปยน โ€ข upperPoint z v hvโŠข (Summable fun r => โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix Mโปยน โ€ข upperPoint z v hv))โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile a b s (cosetHeight r (integralComplexMatrix Mโปยน โ€ข upperPoint z v hv))โ€– โ‰ค eisensteinRemainderBound b s All goals completed! ๐Ÿ™lemma cuspRemainder_aux_norm (b : โ„) (s : โ„‚) (v : โ„) (hv : 0<v) (hvb : vโ‰คb) : โ€–cuspRemainderProfile (b+1) (b+2) s vโ€–=v^s.re := b:โ„s:โ„‚v:โ„hv:0 < vhvb:v โ‰ค bโŠข โ€–cuspRemainderProfile (b + 1) (b + 2) s vโ€– = v ^ s.re All goals completed! ๐Ÿ™lemma cuspRemainder_row_scaled_deriv_aux_bound (a b : โ„) (hab : a<b) (s : โ„‚) (C : โ„) (hC0 : 0โ‰คC) (hC : โˆ€v,|v*deriv (cuspTransition a b) v|โ‰คC) (u : Fin 2โ†’โ„‚) (hu : uโ‰ 0) (p : SpatialCoordinates) (hp : 0<p 2) (j : Fin 3) : โ€–(p 2:โ„‚)*deriv (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (p j)โ€–โ‰ค (โ€–sโ€–+C)*โ€–cuspRemainderProfile (b+1) (b+2) s (rowHeight u p)โ€– := a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3โŠข โ€–โ†‘(p 2) * deriv (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight u p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3hh:0 < rowHeight u pโŠข โ€–โ†‘(p 2) * deriv (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight u p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3hh:0 < rowHeight u phb:rowHeight u p โ‰ค bโŠข โ€–โ†‘(p 2) * deriv (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight u p)โ€–a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3hh:0 < rowHeight u phb:ยฌrowHeight u p โ‰ค bโŠข โ€–โ†‘(p 2) * deriv (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight u p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3hh:0 < rowHeight u phb:rowHeight u p โ‰ค bโŠข โ€–โ†‘(p 2) * deriv (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight u p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3hh:0 < rowHeight u phb:rowHeight u p โ‰ค bโŠข โ€–โ†‘(p 2) * deriv (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * rowHeight u p ^ s.re All goals completed! ๐Ÿ™ a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3hh:0 < rowHeight u phb:ยฌrowHeight u p โ‰ค bโŠข โ€–โ†‘(p 2) * deriv (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight u p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3hh:0 < rowHeight u phb:ยฌrowHeight u p โ‰ค bhd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight u p) * โ†‘(rowHeight u p) * โ†‘(rowLogD u p j)) (p j)โŠข โ€–โ†‘(p 2) * deriv (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight u p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3hh:0 < rowHeight u phb:ยฌrowHeight u p โ‰ค bhd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight u p) * โ†‘(rowHeight u p) * โ†‘(rowLogD u p j)) (p j)โŠข โ€–โ†‘(p 2) * (0 * โ†‘(rowHeight u p) * โ†‘(rowLogD u p j))โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight u p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cu:Fin 2 โ†’ โ„‚hu:u โ‰  0p:SpatialCoordinateshp:0 < p 2j:Fin 3hh:0 < rowHeight u phb:ยฌrowHeight u p โ‰ค bhd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight u q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight u p) * โ†‘(rowHeight u p) * โ†‘(rowLogD u p j)) (p j)โŠข 0 โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight u p)โ€– All goals completed! ๐Ÿ™endopen Filteropen scoped BigOperators Classical Topology ContDiffdef weightedHeightProfile (F : โ„โ†’โ„‚) (r : CuspCosets) (p : SpatialCoordinates) : โ„‚ := (cosetCharacter r)โปยน*F (rowHeight (embeddedRow r) p)lemma weightedHeightProfile_axis_differentiable (F : โ„โ†’โ„‚) (hF : โˆ€v,0<vโ†’ContDiffAt โ„ โˆž F v) (r : CuspCosets) (p : SpatialCoordinates) (hp : 0<p 2) (j : Fin 3) : DifferentiableAt โ„ (axisSlice (weightedHeightProfile F r) p j) (p j) := ((rowProfile_axis_derivatives F hF (embeddedRow r) (embeddedRow_ne_zero r) p hp j).1.const_mul _).differentiableAtlemma heightPoincare_axis_termwise (F : โ„โ†’โ„‚) (hzero : โˆ€vโ‰ค1,F v=0) (hF : โˆ€v,0<vโ†’ContDiffAt โ„ โˆž F v) (p : SpatialCoordinates) (hp : 0<p 2) (j : Fin 3) : Summable (fun r => deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField F) p j) (โˆ‘'r,deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) (p j) := F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3โŠข (Summable fun r => deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField F) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) (p j) F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1โŠข (Summable fun r => deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField F) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) (p j) F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1ht:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)โŠข (Summable fun r => deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField F) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) (p j) F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1ht:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ UโŠข (Summable fun r => deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField F) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) (p j) F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1ht:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0โŠข (Summable fun r => deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField F) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) (p j) F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1ht:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0โŠข HasDerivAt (axisSlice (heightPoincareField F) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile F r) p j) (p j)) (p j) F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1ht:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0โŠข HasDerivAt (axisSlice (heightPoincareField F) p j) (โˆ‘ b โˆˆ S, deriv (axisSlice (weightedHeightProfile F b) p j) (p j)) (p j) F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1ht:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0hd:HasDerivAt (โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j) (โˆ‘ i โˆˆ S, deriv (axisSlice (weightedHeightProfile F i) p j) (p j)) (p j)โŠข HasDerivAt (axisSlice (heightPoincareField F) p j) (โˆ‘ b โˆˆ S, deriv (axisSlice (weightedHeightProfile F b) p j) (p j)) (p j) F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1ht:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0hd:HasDerivAt (โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j) (โˆ‘ i โˆˆ S, deriv (axisSlice (weightedHeightProfile F i) p j) (p j)) (p j)โŠข axisSlice (heightPoincareField F) p j =แถ [๐“ (p j)] โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j filter_upwards [hn] with t F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1htโœ:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0hd:HasDerivAt (โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j) (โˆ‘ i โˆˆ S, deriv (axisSlice (weightedHeightProfile F i) p j) (p j)) (p j)t:โ„ht:Function.update p j t โˆˆ UโŠข axisSlice (heightPoincareField F) p j t = (โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j) t F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1htโœ:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0hd:HasDerivAt (โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j) (โˆ‘ i โˆˆ S, deriv (axisSlice (weightedHeightProfile F i) p j) (p j)) (p j)t:โ„ht:Function.update p j t โˆˆ UโŠข axisSlice (heightPoincareField F) p j t = โˆ‘ c โˆˆ S, axisSlice (weightedHeightProfile F c) p j t F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1htโœ:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0hd:HasDerivAt (โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j) (โˆ‘ i โˆˆ S, deriv (axisSlice (weightedHeightProfile F i) p j) (p j)) (p j)t:โ„ht:Function.update p j t โˆˆ UโŠข โˆ‘' (r : CuspCosets), weightedHeightProfile F r (Function.update p j t) = โˆ‘ r โˆˆ S, weightedHeightProfile F r (Function.update p j t) F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1htโœ:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0hd:HasDerivAt (โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j) (โˆ‘ i โˆˆ S, deriv (axisSlice (weightedHeightProfile F i) p j) (p j)) (p j)t:โ„ht:Function.update p j t โˆˆ UโŠข โˆ€ b โˆ‰ S, weightedHeightProfile F b (Function.update p j t) = 0 F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1htโœ:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0hd:HasDerivAt (โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j) (โˆ‘ i โˆˆ S, deriv (axisSlice (weightedHeightProfile F i) p j) (p j)) (p j)t:โ„ht:Function.update p j t โˆˆ Ur:CuspCosetshr:r โˆ‰ SโŠข weightedHeightProfile F r (Function.update p j t) = 0 F:โ„ โ†’ โ„‚hzero:โˆ€ v โ‰ค 1, F v = 0hF:โˆ€ (v : โ„), 0 < v โ†’ ContDiffAt โ„ โˆž F vp:SpatialCoordinateshp:0 < p 2j:Fin 3U:Set SpatialCoordinateshU:IsOpen UhpU:p โˆˆ US:Finset CuspCosetshrows:โˆ€ q โˆˆ U, 0 < q 2 โˆง โˆ€ r โˆ‰ S, rowHeight (embeddedRow r) q < 1htโœ:Tendsto (fun t => Function.update p j t) (๐“ (p j)) (๐“ p)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), Function.update p j t โˆˆ Uhz:โˆ€ r โˆ‰ S, deriv (axisSlice (weightedHeightProfile F r) p j) (p j) = 0hd:HasDerivAt (โˆ‘ i โˆˆ S, axisSlice (weightedHeightProfile F i) p j) (โˆ‘ i โˆˆ S, deriv (axisSlice (weightedHeightProfile F i) p j) (p j)) (p j)t:โ„ht:Function.update p j t โˆˆ Ur:CuspCosetshr:r โˆ‰ SโŠข (cosetCharacter r)โปยน * F (rowHeight (embeddedRow r) (Function.update p j t)) = 0 All goals completed! ๐Ÿ™lemma weightedRemainder_axis_deriv (a b : โ„) (s : โ„‚) (r : CuspCosets) (p : SpatialCoordinates) (hp : 0<p 2) (j : Fin 3) : deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)= deriv (axisSlice (smoothSummand s r) p j) (p j)- deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j) := a:โ„b:โ„s:โ„‚r:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3โŠข deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = deriv (axisSlice (smoothSummand s r) p j) (p j) - deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j) a:โ„b:โ„s:โ„‚r:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3hn:โˆ€แถ  (t : โ„) in ๐“ (p j), 0 < Function.update p j t 2โŠข deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = deriv (axisSlice (smoothSummand s r) p j) (p j) - deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j) a:โ„b:โ„s:โ„‚r:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3hn:โˆ€แถ  (t : โ„) in ๐“ (p j), 0 < Function.update p j t 2he:axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j =แถ [๐“ (p j)] fun t => axisSlice (smoothSummand s r) p j t - axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j tโŠข deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = deriv (axisSlice (smoothSummand s r) p j) (p j) - deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j) a:โ„b:โ„s:โ„‚r:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3hn:โˆ€แถ  (t : โ„) in ๐“ (p j), 0 < Function.update p j t 2he:axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j =แถ [๐“ (p j)] fun t => axisSlice (smoothSummand s r) p j t - axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j tโŠข deriv (fun t => axisSlice (smoothSummand s r) p j t - axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j t) (p j) = deriv (axisSlice (smoothSummand s r) p j) (p j) - deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j) All goals completed! ๐Ÿ™def eisensteinRemainderField (a b : โ„) (s : โ„‚) (p : SpatialCoordinates) : โ„‚ := smoothEisenstein s p-smoothCuspSeedField a b s ptheorem eisensteinRemainder_axis_termwise (a b : โ„) (ha : 1<a) (hab : a<b) (s : โ„‚) (hs : 2<s.re) (p : SpatialCoordinates) (hp : 0<p 2) (j : Fin 3) : Summable (fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘'r,deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j) := a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3โŠข (Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j) a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3hE:(Summable fun r => deriv (axisSlice (smoothSummand s r) p j) (p j)) โˆง (Summable fun r => deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) โˆง HasDerivAt (axisSlice (smoothEisenstein s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j)) (p j) โˆง HasDerivAt (deriv (axisSlice (smoothEisenstein s) p j)) (โˆ‘' (r : CuspCosets), deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) (p j)โŠข (Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j) a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3hE:(Summable fun r => deriv (axisSlice (smoothSummand s r) p j) (p j)) โˆง (Summable fun r => deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) โˆง HasDerivAt (axisSlice (smoothEisenstein s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j)) (p j) โˆง HasDerivAt (deriv (axisSlice (smoothEisenstein s) p j)) (โˆ‘' (r : CuspCosets), deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) (p j)hS:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) (p j)โŠข (Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j) a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3hE:(Summable fun r => deriv (axisSlice (smoothSummand s r) p j) (p j)) โˆง (Summable fun r => deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) โˆง HasDerivAt (axisSlice (smoothEisenstein s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j)) (p j) โˆง HasDerivAt (deriv (axisSlice (smoothEisenstein s) p j)) (โˆ‘' (r : CuspCosets), deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) (p j)hS:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) (p j)hcoeff:โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j) - โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)โŠข (Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j) a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3hE:(Summable fun r => deriv (axisSlice (smoothSummand s r) p j) (p j)) โˆง (Summable fun r => deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) โˆง HasDerivAt (axisSlice (smoothEisenstein s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j)) (p j) โˆง HasDerivAt (deriv (axisSlice (smoothEisenstein s) p j)) (โˆ‘' (r : CuspCosets), deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) (p j)hS:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) (p j)hcoeff:โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j) - โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)โŠข HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j) a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3hE:(Summable fun r => deriv (axisSlice (smoothSummand s r) p j) (p j)) โˆง (Summable fun r => deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) โˆง HasDerivAt (axisSlice (smoothEisenstein s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j)) (p j) โˆง HasDerivAt (deriv (axisSlice (smoothEisenstein s) p j)) (โˆ‘' (r : CuspCosets), deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) (p j)hS:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) (p j)hcoeff:โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j) - โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)โŠข HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j) - โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) (p j) a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3hE:(Summable fun r => deriv (axisSlice (smoothSummand s r) p j) (p j)) โˆง (Summable fun r => deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) โˆง HasDerivAt (axisSlice (smoothEisenstein s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j)) (p j) โˆง HasDerivAt (deriv (axisSlice (smoothEisenstein s) p j)) (โˆ‘' (r : CuspCosets), deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) (p j)hS:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) (p j)hcoeff:โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j) - โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)โŠข axisSlice (eisensteinRemainderField a b s) p j =แถ [๐“ (p j)] axisSlice (smoothEisenstein s) p j - axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3hE:(Summable fun r => deriv (axisSlice (smoothSummand s r) p j) (p j)) โˆง (Summable fun r => deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) โˆง HasDerivAt (axisSlice (smoothEisenstein s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j)) (p j) โˆง HasDerivAt (deriv (axisSlice (smoothEisenstein s) p j)) (โˆ‘' (r : CuspCosets), deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) (p j)hS:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) (p j)hcoeff:โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j) - โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), 0 < Function.update p j t 2โŠข axisSlice (eisensteinRemainderField a b s) p j =แถ [๐“ (p j)] axisSlice (smoothEisenstein s) p j - axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j filter_upwards [hn] with t a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3hE:(Summable fun r => deriv (axisSlice (smoothSummand s r) p j) (p j)) โˆง (Summable fun r => deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) โˆง HasDerivAt (axisSlice (smoothEisenstein s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j)) (p j) โˆง HasDerivAt (deriv (axisSlice (smoothEisenstein s) p j)) (โˆ‘' (r : CuspCosets), deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) (p j)hS:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) (p j)hcoeff:โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j) - โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), 0 < Function.update p j t 2t:โ„ht:0 < Function.update p j t 2โŠข axisSlice (eisensteinRemainderField a b s) p j t = (axisSlice (smoothEisenstein s) p j - axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j) t a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:2 < s.rep:SpatialCoordinateshp:0 < p 2j:Fin 3hE:(Summable fun r => deriv (axisSlice (smoothSummand s r) p j) (p j)) โˆง (Summable fun r => deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) โˆง HasDerivAt (axisSlice (smoothEisenstein s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j)) (p j) โˆง HasDerivAt (deriv (axisSlice (smoothEisenstein s) p j)) (โˆ‘' (r : CuspCosets), deriv (deriv (axisSlice (smoothSummand s r) p j)) (p j)) (p j)hS:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (heightPoincareField (cuspSeedProfile a b s)) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)) (p j)hcoeff:โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = โˆ‘' (r : CuspCosets), deriv (axisSlice (smoothSummand s r) p j) (p j) - โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspSeedProfile a b s) r) p j) (p j)hn:โˆ€แถ  (t : โ„) in ๐“ (p j), 0 < Function.update p j t 2t:โ„ht:0 < Function.update p j t 2โŠข smoothEisenstein s (Function.update p j t) - smoothCuspSeedField a b s (Function.update p j t) = smoothEisenstein s (Function.update p j t) - heightPoincareField (cuspSeedProfile a b s) (Function.update p j t) All goals completed! ๐Ÿ™end CubicEisensteinopen Filter MeasureTheoryopen scoped BigOperators Classical Topology ContDiff Manifoldnamespace CubicEisensteinlemma weightedRemainder_scaled_deriv_bound (a b : โ„) (hab : a<b) (s : โ„‚) (C : โ„) (hC0 : 0โ‰คC) (hC : โˆ€v,|v*deriv (cuspTransition a b) v|โ‰คC) (r : CuspCosets) (p : SpatialCoordinates) (hp : 0<p 2) (j : Fin 3) : โ€–(p 2:โ„‚)*deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€–โ‰ค (โ€–sโ€–+C)*โ€–cuspRemainderProfile (b+1) (b+2) s (rowHeight (embeddedRow r) p)โ€– := a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cr:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3โŠข โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cr:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3g:SpatialCoordinates โ†’ โ„‚ := fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)โŠข โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cr:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3g:SpatialCoordinates โ†’ โ„‚ := fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)hd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j)) (p j)โŠข โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cr:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3g:SpatialCoordinates โ†’ โ„‚ := fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)hd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j)) (p j)hw:HasDerivAt (fun y => (cosetCharacter r)โปยน * axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j y) ((cosetCharacter r)โปยน * (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j))) (p j)โŠข โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cr:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3g:SpatialCoordinates โ†’ โ„‚ := fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)hd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j)) (p j)hw:HasDerivAt (fun y => (cosetCharacter r)โปยน * axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j y) ((cosetCharacter r)โปยน * (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j))) (p j)he:deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = (cosetCharacter r)โปยน * deriv (axisSlice g p j) (p j)โŠข โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cr:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3g:SpatialCoordinates โ†’ โ„‚ := fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)hd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j)) (p j)hw:HasDerivAt (fun y => (cosetCharacter r)โปยน * axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j y) ((cosetCharacter r)โปยน * (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j))) (p j)he:deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = (cosetCharacter r)โปยน * deriv (axisSlice g p j) (p j)โŠข โ€–โ†‘(p 2) * ((cosetCharacter r)โปยน * deriv (axisSlice g p j) (p j))โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– calc โ€–(p 2:โ„‚)*((cosetCharacter r)โปยน*deriv (axisSlice g p j) (p j))โ€– = โ€–(cosetCharacter r)โปยน*((p 2:โ„‚)*deriv (axisSlice g p j) (p j))โ€– := a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cr:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3g:SpatialCoordinates โ†’ โ„‚ := fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)hd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j)) (p j)hw:HasDerivAt (fun y => (cosetCharacter r)โปยน * axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j y) ((cosetCharacter r)โปยน * (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j))) (p j)he:deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = (cosetCharacter r)โปยน * deriv (axisSlice g p j) (p j)โŠข โ€–โ†‘(p 2) * ((cosetCharacter r)โปยน * deriv (axisSlice g p j) (p j))โ€– = โ€–(cosetCharacter r)โปยน * (โ†‘(p 2) * deriv (axisSlice g p j) (p j))โ€– a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cr:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3g:SpatialCoordinates โ†’ โ„‚ := fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)hd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j)) (p j)hw:HasDerivAt (fun y => (cosetCharacter r)โปยน * axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j y) ((cosetCharacter r)โปยน * (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j))) (p j)he:deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = (cosetCharacter r)โปยน * deriv (axisSlice g p j) (p j)โŠข โ†‘(p 2) * ((cosetCharacter r)โปยน * deriv (axisSlice g p j) (p j)) = (cosetCharacter r)โปยน * (โ†‘(p 2) * deriv (axisSlice g p j) (p j)); All goals completed! ๐Ÿ™ _ = โ€–(p 2:โ„‚)*deriv (axisSlice g p j) (p j)โ€– := a:โ„b:โ„hab:a < bs:โ„‚C:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cr:CuspCosetsp:SpatialCoordinateshp:0 < p 2j:Fin 3g:SpatialCoordinates โ†’ โ„‚ := fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)hd:HasDerivAt (axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j) (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j)) (p j)hw:HasDerivAt (fun y => (cosetCharacter r)โปยน * axisSlice (fun q => cuspRemainderProfile a b s (rowHeight (embeddedRow r) q)) p j y) ((cosetCharacter r)โปยน * (deriv (cuspRemainderProfile a b s) (rowHeight (embeddedRow r) p) * โ†‘(rowHeight (embeddedRow r) p) * โ†‘(rowLogD (embeddedRow r) p j))) (p j)he:deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j) = (cosetCharacter r)โปยน * deriv (axisSlice g p j) (p j)โŠข โ€–(cosetCharacter r)โปยน * (โ†‘(p 2) * deriv (axisSlice g p j) (p j))โ€– = โ€–โ†‘(p 2) * deriv (axisSlice g p j) (p j)โ€– All goals completed! ๐Ÿ™ _ โ‰ค _ := cuspRemainder_row_scaled_deriv_aux_bound a b hab s C hC0 hC _ (embeddedRow_ne_zero r) p hp jtheorem eisensteinRemainder_scaled_axis_bound (a b : โ„) (ha : 1<a) (hab : a<b) (s : โ„‚) (hs : 4<s.re) : โˆƒB : โ„,0โ‰คB โˆง โˆ€p : SpatialCoordinates,0<p 2โ†’โˆ€j : Fin 3, โ€–(p 2:โ„‚)*deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€–โ‰คB := a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reโŠข โˆƒ B, 0 โ‰ค B โˆง โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค CโŠข โˆƒ B, 0 โ‰ค B โˆง โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค CโŠข โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3โŠข โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3hA:(Summable fun r => โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– โ‰ค eisensteinRemainderBound (b + 2) sโŠข โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3hA:(Summable fun r => โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– โ‰ค eisensteinRemainderBound (b + 2) shB:Summable fun i => (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow i) p)โ€–โŠข โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3hA:(Summable fun r => โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– โ‰ค eisensteinRemainderBound (b + 2) shB:Summable fun i => (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow i) p)โ€–hb:โˆ€ (r : CuspCosets), โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–โŠข โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3hA:(Summable fun r => โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– โ‰ค eisensteinRemainderBound (b + 2) shB:Summable fun i => (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow i) p)โ€–hb:โˆ€ (r : CuspCosets), โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–hnorm:Summable fun r => โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€–โŠข โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3hA:(Summable fun r => โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– โ‰ค eisensteinRemainderBound (b + 2) shB:Summable fun i => (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow i) p)โ€–hb:โˆ€ (r : CuspCosets), โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–hnorm:Summable fun r => โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€–ht:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j)โŠข โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3hA:(Summable fun r => โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– โ‰ค eisensteinRemainderBound (b + 2) shB:Summable fun i => (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow i) p)โ€–hb:โˆ€ (r : CuspCosets), โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–hnorm:Summable fun r => โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€–ht:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j)โŠข โ€–โˆ‘' (x : CuspCosets), โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) x) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3hA:(Summable fun r => โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– โ‰ค eisensteinRemainderBound (b + 2) shB:Summable fun i => (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow i) p)โ€–hb:โˆ€ (r : CuspCosets), โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–hnorm:Summable fun r => โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€–ht:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j)โŠข โˆ‘' (i : CuspCosets), โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) i) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3hA:(Summable fun r => โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– โ‰ค eisensteinRemainderBound (b + 2) shB:Summable fun i => (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow i) p)โ€–hb:โˆ€ (r : CuspCosets), โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–hnorm:Summable fun r => โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€–ht:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j)โŠข โˆ‘' (i : CuspCosets), (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow i) p)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reC:โ„hC0:0 โ‰ค ChC:โˆ€ (v : โ„), |v * deriv (cuspTransition a b) v| โ‰ค Cp:SpatialCoordinateshp:0 < p 2j:Fin 3hA:(Summable fun r => โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–) โˆง โˆ‘' (r : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€– โ‰ค eisensteinRemainderBound (b + 2) shB:Summable fun i => (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow i) p)โ€–hb:โˆ€ (r : CuspCosets), โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€– โ‰ค (โ€–sโ€– + C) * โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow r) p)โ€–hnorm:Summable fun r => โ€–โ†‘(p 2) * deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)โ€–ht:(Summable fun r => deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) โˆง HasDerivAt (axisSlice (eisensteinRemainderField a b s) p j) (โˆ‘' (r : CuspCosets), deriv (axisSlice (weightedHeightProfile (cuspRemainderProfile a b s) r) p j) (p j)) (p j)โŠข (โ€–sโ€– + C) * โˆ‘' (x : CuspCosets), โ€–cuspRemainderProfile (b + 1) (b + 2) s (rowHeight (embeddedRow x) p)โ€– โ‰ค (โ€–sโ€– + C) * eisensteinRemainderBound (b + 2) s All goals completed! ๐Ÿ™def kernelEisensteinRemainder (a b : โ„) (s : โ„‚) (hs : 2<s.re) : KernelQuotientโ†’โ„‚ := fun q => kernelQuotientEisenstein s hs q-kernelQuotientSeed a b s qlemma kernelEisensteinRemainder_smooth (a b : โ„) (ha : 1<a) (hab : a<b) (s : โ„‚) (hs : 2<s.re) : ContMDiff ๐“˜(โ„,SpatialCoordinates) ๐“˜(โ„,โ„‚) โˆž (kernelEisensteinRemainder a b s hs) := (kernelQuotientEisenstein_contMDiff s hs).sub (kernelQuotientSeed_contMDiff a b s ha hab)lemma kernelEisensteinRemainder_euclidean_smooth (a b : โ„) (ha : 1<a) (hab : a<b) (s : โ„‚) (hs : 2<s.re) (p : EuclideanSpatial) (hp : 0<p 2) : ContDiffAt โ„ โˆž (fun q => kernelEisensteinRemainder a b s hs (kernelEuclideanProjection q)) p := ((((kernelEisensteinRemainder_smooth a b ha hab s hs).comp kernelProjection_contMDiff) (euclideanToHyperbolic p)).comp p (euclideanToHyperbolic_contMDiffAt p hp)).contDiffAtlemma kernelEisensteinRemainder_euclidean_eq (a b : โ„) (s : โ„‚) (hs : 2<s.re) (p : EuclideanSpatial) (hp : 0<p 2) : kernelEisensteinRemainder a b s hs (kernelEuclideanProjection p)=eisensteinRemainderField a b s p.ofLp := a:โ„b:โ„s:โ„‚hs:2 < s.rep:EuclideanSpatialhp:0 < p.ofLp 2โŠข kernelEisensteinRemainder a b s hs (kernelEuclideanProjection p) = eisensteinRemainderField a b s p.ofLp a:โ„b:โ„s:โ„‚hs:2 < s.rep:EuclideanSpatialhp:0 < p.ofLp 2โŠข kernelQuotientEisenstein s hs ((integralOrbitProjection globalKubotaKernel โˆ˜ euclideanToHyperbolic) p) - kernelQuotientSeed a b s ((integralOrbitProjection globalKubotaKernel โˆ˜ euclideanToHyperbolic) p) = eisensteinRemainderField a b s p.ofLp a:โ„b:โ„s:โ„‚hs:2 < s.rep:EuclideanSpatialhp:0 < p.ofLp 2โŠข kernelQuotientEisenstein s hs (integralOrbitProjection globalKubotaKernel (euclideanToHyperbolic p)) - kernelQuotientSeed a b s (integralOrbitProjection globalKubotaKernel (euclideanToHyperbolic p)) = eisensteinRemainderField a b s p.ofLp a:โ„b:โ„s:โ„‚hs:2 < s.rep:EuclideanSpatialhp:0 < p.ofLp 2โŠข upperEisenstein (โ†‘(p.ofLp 0) + I * โ†‘(p.ofLp 1)) (p.ofLp 2) hp s - kernelQuotientSeed a b s (integralOrbitProjection globalKubotaKernel (upperPoint (โ†‘(p.ofLp 0) + I * โ†‘(p.ofLp 1)) (p.ofLp 2) hp)) = eisensteinRemainderField a b s p.ofLp a:โ„b:โ„s:โ„‚hs:2 < s.rep:EuclideanSpatialhp:0 < p.ofLp 2โŠข upperEisenstein (โ†‘(p.ofLp 0) + I * โ†‘(p.ofLp 1)) (p.ofLp 2) hp s - kernelQuotientSeed a b s (integralOrbitProjection globalKubotaKernel (upperPoint (โ†‘(p.ofLp 0) + I * โ†‘(p.ofLp 1)) (p.ofLp 2) hp)) = smoothEisenstein s p.ofLp - smoothCuspSeedField a b s p.ofLp a:โ„b:โ„s:โ„‚hs:2 < s.rep:EuclideanSpatialhp:0 < p.ofLp 2โŠข upperEisenstein (โ†‘(p.ofLp 0) + I * โ†‘(p.ofLp 1)) (p.ofLp 2) hp s - kernelQuotientSeed a b s (integralOrbitProjection globalKubotaKernel (upperPoint (โ†‘(p.ofLp 0) + I * โ†‘(p.ofLp 1)) (p.ofLp 2) hp)) = upperEisenstein (โ†‘(p.ofLp 0) + โ†‘(p.ofLp 1) * I) (p.ofLp 2) hp s - smoothCuspSeed a b s (upperPoint (โ†‘(p.ofLp 0) + โ†‘(p.ofLp 1) * I) (p.ofLp 2) hp) a:โ„b:โ„s:โ„‚hs:2 < s.rep:EuclideanSpatialhp:0 < p.ofLp 2โŠข upperEisenstein (โ†‘(p.ofLp 0) + โ†‘(p.ofLp 1) * I) (p.ofLp 2) hp s - kernelQuotientSeed a b s (integralOrbitProjection globalKubotaKernel (upperPoint (โ†‘(p.ofLp 0) + โ†‘(p.ofLp 1) * I) (p.ofLp 2) hp)) = upperEisenstein (โ†‘(p.ofLp 0) + โ†‘(p.ofLp 1) * I) (p.ofLp 2) hp s - smoothCuspSeed a b s (upperPoint (โ†‘(p.ofLp 0) + โ†‘(p.ofLp 1) * I) (p.ofLp 2) hp) All goals completed! ๐Ÿ™theorem kernelEisensteinRemainder_scaled_fderiv_bound (a b : โ„) (ha : 1<a) (hab : a<b) (s : โ„‚) (hs : 4<s.re) : โˆƒB : โ„,0โ‰คB โˆง โˆ€p : EuclideanSpatial,0<p 2โ†’โˆ€j : Fin 3, โ€–(p 2:โ„‚)*fderiv โ„ (fun q => kernelEisensteinRemainder a b s (a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„p:EuclideanSpatialj:Fin 3q:EuclideanSpatialโŠข 2 < s.re All goals completed! ๐Ÿ™) (kernelEuclideanProjection q)) p (euclideanCoordinateVector j)โ€–โ‰คB := a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reโŠข โˆƒ B, 0 โ‰ค B โˆง โˆ€ (p : EuclideanSpatial), 0 < p.ofLp 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p.ofLp 2) * (fderiv โ„ (fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)) p) (euclideanCoordinateVector j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„hB:0 โ‰ค Bhbound:โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค BโŠข โˆƒ B, 0 โ‰ค B โˆง โˆ€ (p : EuclideanSpatial), 0 < p.ofLp 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p.ofLp 2) * (fderiv โ„ (fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)) p) (euclideanCoordinateVector j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„hB:0 โ‰ค Bhbound:โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค BโŠข โˆ€ (p : EuclideanSpatial), 0 < p.ofLp 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p.ofLp 2) * (fderiv โ„ (fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)) p) (euclideanCoordinateVector j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„hB:0 โ‰ค Bhbound:โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค Bp:EuclideanSpatialhp:0 < p.ofLp 2j:Fin 3โŠข โ€–โ†‘(p.ofLp 2) * (fderiv โ„ (fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)) p) (euclideanCoordinateVector j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„hB:0 โ‰ค Bhbound:โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค Bp:EuclideanSpatialhp:0 < p.ofLp 2j:Fin 3f:EuclideanSpatial โ†’ โ„‚ := fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)โŠข โ€–โ†‘(p.ofLp 2) * (fderiv โ„ (fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)) p) (euclideanCoordinateVector j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„hB:0 โ‰ค Bhbound:โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค Bp:EuclideanSpatialhp:0 < p.ofLp 2j:Fin 3f:EuclideanSpatial โ†’ โ„‚ := fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)hf:โˆ€ (q : EuclideanSpatial), 0 < q.ofLp 2 โ†’ ContDiffAt โ„ โˆž f qโŠข โ€–โ†‘(p.ofLp 2) * (fderiv โ„ (fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)) p) (euclideanCoordinateVector j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„hB:0 โ‰ค Bhbound:โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค Bp:EuclideanSpatialhp:0 < p.ofLp 2j:Fin 3f:EuclideanSpatial โ†’ โ„‚ := fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)hf:โˆ€ (q : EuclideanSpatial), 0 < q.ofLp 2 โ†’ ContDiffAt โ„ โˆž f qhe:โˆ€ (q : SpatialCoordinates), 0 < q 2 โ†’ f (WithLp.toLp 2 q) = eisensteinRemainderField a b s qโŠข โ€–โ†‘(p.ofLp 2) * (fderiv โ„ (fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)) p) (euclideanCoordinateVector j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„hB:0 โ‰ค Bhbound:โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค Bp:EuclideanSpatialhp:0 < p.ofLp 2j:Fin 3f:EuclideanSpatial โ†’ โ„‚ := fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)hf:โˆ€ (q : EuclideanSpatial), 0 < q.ofLp 2 โ†’ ContDiffAt โ„ โˆž f qhe:โˆ€ (q : SpatialCoordinates), 0 < q 2 โ†’ f (WithLp.toLp 2 q) = eisensteinRemainderField a b s qheq:axisSlice (fun q => f (WithLp.toLp 2 q)) p.ofLp j =แถ [๐“ (p.ofLp j)] axisSlice (eisensteinRemainderField a b s) p.ofLp jโŠข โ€–โ†‘(p.ofLp 2) * (fderiv โ„ (fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)) p) (euclideanCoordinateVector j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„hB:0 โ‰ค Bhbound:โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค Bp:EuclideanSpatialhp:0 < p.ofLp 2j:Fin 3f:EuclideanSpatial โ†’ โ„‚ := fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)hf:โˆ€ (q : EuclideanSpatial), 0 < q.ofLp 2 โ†’ ContDiffAt โ„ โˆž f qhe:โˆ€ (q : SpatialCoordinates), 0 < q 2 โ†’ f (WithLp.toLp 2 q) = eisensteinRemainderField a b s qheq:axisSlice (fun q => f (WithLp.toLp 2 q)) p.ofLp j =แถ [๐“ (p.ofLp j)] axisSlice (eisensteinRemainderField a b s) p.ofLp jโŠข โ€–โ†‘(p.ofLp 2) * (fderiv โ„ f p) (euclideanCoordinateVector j)โ€– โ‰ค B a:โ„b:โ„ha:1 < ahab:a < bs:โ„‚hs:4 < s.reB:โ„hB:0 โ‰ค Bhbound:โˆ€ (p : SpatialCoordinates), 0 < p 2 โ†’ โˆ€ (j : Fin 3), โ€–โ†‘(p 2) * deriv (axisSlice (eisensteinRemainderField a b s) p j) (p j)โ€– โ‰ค Bp:EuclideanSpatialhp:0 < p.ofLp 2j:Fin 3f:EuclideanSpatial โ†’ โ„‚ := fun q => kernelEisensteinRemainder a b s โ‹ฏ (kernelEuclideanProjection q)hf:โˆ€ (q : EuclideanSpatial), 0 < q.ofLp 2 โ†’ ContDiffAt โ„ โˆž f qhe:โˆ€ (q : SpatialCoordinates), 0 < q 2 โ†’ f (WithLp.toLp 2 q) = eisensteinRemainderField a b s qheq:axisSlice (fun q => f (WithLp.toLp 2 q)) p.ofLp j =แถ [๐“ (p.ofLp j)] axisSlice (eisensteinRemainderField a b s) p.ofLp jโŠข โ€–โ†‘(p.ofLp 2) * deriv (axisSlice (eisensteinRemainderField a b s) p.ofLp j) (p.ofLp j)โ€– โ‰ค B All goals completed! ๐Ÿ™end CubicEisensteinendend OAI