import OAI.NumberTheory.DirichletL.Mellin.CompactWeights import OAI.NumberTheory.DirichletL.QuadraticSieve.CoefficientCancellationnamespace 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 BigOperators Classical SchwartzMapnamespace QuadraticInitialBoundopen ActualEisensteinCubic ConcreteTraceCRT EisensteinSchwartzPoissondef quadraticRow {Ξ± : Type*} (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (S : Finset Ξ±) (z : O) : β„‚ := (finiteSquarefreeRow P hg S z) ^ 3theorem quadraticRow_eq_canonical {Ξ± : Type*} (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (S : Finset Ξ±) (z : O) : quadraticRow P hg S z = finiteSexticRow (fun i : S => P i.val) (fun i => hg i.val) (fun _ => 3) z := Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:O⊒ quadraticRow P hg S z = finiteSexticRow (fun i => P ↑i) β‹― (fun x => 3) z Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:O⊒ (∏ i ∈ S, (canonicalSextic (P i) β‹―) ((Ideal.Quotient.mk (P i)) z)) ^ 3 = (∏ x, (canonicalSextic (P ↑x) β‹―) ((Ideal.Quotient.mk (P ↑x)) z)) ^ 3 All goals completed! πŸ™theorem quadraticRow_star {Ξ± : Type*} (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (S : Finset Ξ±) (z : O) : star (quadraticRow P hg S z) = quadraticRow P hg S z := Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:O⊒ star (quadraticRow P hg S z) = quadraticRow P hg S z Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:O⊒ star (finiteSexticRow (fun i => P ↑i) β‹― (fun x => 3) z) = finiteSexticRow (fun i => P ↑i) β‹― (fun x => 3) z Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:O⊒ ∏ x, star ((canonicalSextic (P ↑x) β‹― ^ 3) ((Ideal.Quotient.mk (P ↑x)) z)) = ∏ x, (canonicalSextic (P ↑x) β‹― ^ 3) ((Ideal.Quotient.mk (P ↑x)) z) Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:O⊒ βˆ€ x ∈ Finset.univ, star ((canonicalSextic (P ↑x) β‹― ^ 3) ((Ideal.Quotient.mk (P ↑x)) z)) = (canonicalSextic (P ↑x) β‹― ^ 3) ((Ideal.Quotient.mk (P ↑x)) z) Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:Oi:β†₯Sa✝:i ∈ Finset.univ⊒ star ((canonicalSextic (P ↑i) β‹― ^ 3) ((Ideal.Quotient.mk (P ↑i)) z)) = (canonicalSextic (P ↑i) β‹― ^ 3) ((Ideal.Quotient.mk (P ↑i)) z) Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:Oi:β†₯Sa✝:i ∈ Finset.univ⊒ star (((quadraticChar (ActualEisensteinCubic.O β§Έ P ↑i)).ringHomComp (Int.castRingHom β„‚)) ((Ideal.Quotient.mk (P ↑i)) z)) = ((quadraticChar (ActualEisensteinCubic.O β§Έ P ↑i)).ringHomComp (Int.castRingHom β„‚)) ((Ideal.Quotient.mk (P ↑i)) z) All goals completed! πŸ™theorem quadraticRow_disjoint_union {Ξ± : Type*} [DecidableEq Ξ±] (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (S T : Finset Ξ±) (hd : Disjoint S T) (z : O) : quadraticRow P hg (S βˆͺ T) z = quadraticRow P hg S z * quadraticRow P hg T z := Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±hd:Disjoint S Tz:O⊒ quadraticRow P hg (S βˆͺ T) z = quadraticRow P hg S z * quadraticRow P hg T z All goals completed! πŸ™theorem quadraticRow_pair_kernel {Ξ± : Type*} [DecidableEq Ξ±] (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (S T : Finset Ξ±) (z : O) : star (quadraticRow P hg S z) * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * finiteSexticRow (activePrimes P S T) (fun i => hg i.val) (fun _ => 3) z := Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:O⊒ star (quadraticRow P hg S z) * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * finiteSexticRow (activePrimes P S T) β‹― (fun x => 3) z Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:Oh:(star (finiteSquarefreeRow P hg S z) * finiteSquarefreeRow P hg T z) ^ 3 = (rowCoprimeMask P (S ∩ T) z * star (finiteSquarefreeRow P hg (S \ T) z) * finiteSquarefreeRow P hg (T \ S) z) ^ 3⊒ star (quadraticRow P hg S z) * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * finiteSexticRow (activePrimes P S T) β‹― (fun x => 3) z Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:Oh:(star (finiteSquarefreeRow P hg S z) * finiteSquarefreeRow P hg T z) ^ 3 = (rowCoprimeMask P (S ∩ T) z * star (finiteSquarefreeRow P hg (S \ T) z) * finiteSquarefreeRow P hg (T \ S) z) ^ 3hm:rowCoprimeMask P (S ∩ T) z ^ 3 = rowCoprimeMask P (S ∩ T) z⊒ star (quadraticRow P hg S z) * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * finiteSexticRow (activePrimes P S T) β‹― (fun x => 3) z Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:Oh:(star (finiteSquarefreeRow P hg S z) * finiteSquarefreeRow P hg T z) ^ 3 = (rowCoprimeMask P (S ∩ T) z * star (finiteSquarefreeRow P hg (S \ T) z) * finiteSquarefreeRow P hg (T \ S) z) ^ 3hm:rowCoprimeMask P (S ∩ T) z ^ 3 = rowCoprimeMask P (S ∩ T) zhd:Disjoint (S \ T) (T \ S)⊒ star (quadraticRow P hg S z) * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * finiteSexticRow (activePrimes P S T) β‹― (fun x => 3) z Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:Ohm:rowCoprimeMask P (S ∩ T) z ^ 3 = rowCoprimeMask P (S ∩ T) zhd:Disjoint (S \ T) (T \ S)h:star (finiteSquarefreeRow P hg S z ^ 3) * finiteSquarefreeRow P hg T z ^ 3 = rowCoprimeMask P (S ∩ T) z * star (finiteSquarefreeRow P hg (S \ T) z ^ 3) * finiteSquarefreeRow P hg (T \ S) z ^ 3⊒ star (quadraticRow P hg S z) * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * finiteSexticRow (activePrimes P S T) β‹― (fun x => 3) z Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:Ohm:rowCoprimeMask P (S ∩ T) z ^ 3 = rowCoprimeMask P (S ∩ T) zhd:Disjoint (S \ T) (T \ S)h:star (quadraticRow P hg S z) * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * star (quadraticRow P hg (S \ T) z) * quadraticRow P hg (T \ S) z⊒ star (quadraticRow P hg S z) * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * finiteSexticRow (activePrimes P S T) β‹― (fun x => 3) z Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:Ohm:rowCoprimeMask P (S ∩ T) z ^ 3 = rowCoprimeMask P (S ∩ T) zhd:Disjoint (S \ T) (T \ S)h:quadraticRow P hg S z * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * quadraticRow P hg (S \ T) z * quadraticRow P hg (T \ S) z⊒ quadraticRow P hg S z * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * finiteSexticRow (activePrimes P S T) β‹― (fun x => 3) z Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:Ohm:rowCoprimeMask P (S ∩ T) z ^ 3 = rowCoprimeMask P (S ∩ T) zhd:Disjoint (S \ T) (T \ S)h:quadraticRow P hg S z * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * quadraticRow P hg (S \ T) z * quadraticRow P hg (T \ S) z⊒ quadraticRow P hg S z * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * quadraticRow P hg (activeSupport S T) z Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:Ohm:rowCoprimeMask P (S ∩ T) z ^ 3 = rowCoprimeMask P (S ∩ T) zhd:Disjoint (S \ T) (T \ S)h:quadraticRow P hg S z * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * quadraticRow P hg (S \ T) z * quadraticRow P hg (T \ S) z⊒ quadraticRow P hg S z * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * quadraticRow P hg (S \ T βˆͺ T \ S) z Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±z:Ohm:rowCoprimeMask P (S ∩ T) z ^ 3 = rowCoprimeMask P (S ∩ T) zhd:Disjoint (S \ T) (T \ S)h:quadraticRow P hg S z * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * quadraticRow P hg (S \ T) z * quadraticRow P hg (T \ S) z⊒ quadraticRow P hg S z * quadraticRow P hg T z = rowCoprimeMask P (S ∩ T) z * (quadraticRow P hg (S \ T) z * quadraticRow P hg (T \ S) z) All goals completed! πŸ™theorem quadratic_gram_offdiagonal {Ξ± : Type*} [DecidableEq Ξ±] (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hinj : Function.Injective P) (hg : βˆ€ i, lambda βˆ‰ P i) (hc : βˆ€ i, ringChar (O β§Έ P i) β‰  2) (S T : Finset Ξ±) (hne : S β‰  T) (W : 𝓒(ℝ, β„‚)) (M : ℝ) (hM : 0 < M) : β€–βˆ‘' z : O, (star (quadraticRow P hg S z) * quadraticRow P hg T z) * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ (2 : ℝ) ^ (S ∩ T).card * (pvControl W * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–) := Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2S:Finset Ξ±T:Finset Ξ±hne:S β‰  TW:𝓒(ℝ, β„‚)M:ℝhM:0 < M⊒ β€–βˆ‘' (z : O), star (quadraticRow P hg S z) * quadraticRow P hg T z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ 2 ^ #(S ∩ T) * (pvControl W * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–) Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2S:Finset Ξ±T:Finset Ξ±hne:S β‰  TW:𝓒(ℝ, β„‚)M:ℝhM:0 < Mthis:Nonempty β†₯(activeSupport S T) := ···⊒ β€–βˆ‘' (z : O), star (quadraticRow P hg S z) * quadraticRow P hg T z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ 2 ^ #(S ∩ T) * (pvControl W * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–) simp_rw Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2S:Finset Ξ±T:Finset Ξ±hne:S β‰  TW:𝓒(ℝ, β„‚)M:ℝhM:0 < Mthis:Nonempty β†₯(activeSupport S T) := ···⊒ β€–βˆ‘' (z : O), star (quadraticRow P hg S z) * quadraticRow P hg T z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ 2 ^ #(S ∩ T) * (pvControl W * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–)Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2S:Finset Ξ±T:Finset Ξ±hne:S β‰  TW:𝓒(ℝ, β„‚)M:ℝhM:0 < Mthis:Nonempty β†₯(activeSupport S T) := ···⊒ β€–βˆ‘' (z : O), rowCoprimeMask P (S ∩ T) z * finiteSexticRow (activePrimes P S T) β‹― (fun x => 3) z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ 2 ^ #(S ∩ T) * (pvControl W * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–)] exact canonical_masked_polya_vinogradov P hinj (S ∩ T) (activePrimes P S T) (activePrimes_pairwise_isCoprime P hinj S T) (fun i => hg i.val) (fun i => hc i.val) (fun _ => 3) (fun _ => Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2S:Finset Ξ±T:Finset Ξ±hne:S β‰  TW:𝓒(ℝ, β„‚)M:ℝhM:0 < Mthis:Nonempty β†₯(activeSupport S T) := Β·Β·Β·x✝:β†₯(activeSupport S T)⊒ 3 β‰  0 All goals completed! πŸ™) (fun _ => Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2S:Finset Ξ±T:Finset Ξ±hne:S β‰  TW:𝓒(ℝ, β„‚)M:ℝhM:0 < Mthis:Nonempty β†₯(activeSupport S T) := Β·Β·Β·x✝:β†₯(activeSupport S T)⊒ 3 < 6 All goals completed! πŸ™) W M hMdef supportNorm {Ξ± : Type*} (P : Ξ± β†’ Ideal O) (S : Finset Ξ±) : ℝ := Ideal.absNorm (∏ i ∈ S, P i)theorem supportNorm_nonneg {Ξ± : Type*} (P : Ξ± β†’ Ideal O) (S : Finset Ξ±) : 0 ≀ supportNorm P S := Nat.cast_nonneg _theorem two_pow_card_le_supportNorm {Ξ± : Type*} (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (S : Finset Ξ±) : (2 : ℝ) ^ S.card ≀ supportNorm P S := Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset α⊒ 2 ^ #S ≀ supportNorm P S Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±hnorm:βˆ€ (i : Ξ±), 2 ≀ ↑(absNorm (P i))⊒ 2 ^ #S ≀ supportNorm P S Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±hnorm:βˆ€ (i : Ξ±), 2 ≀ ↑(absNorm (P i))⊒ 2 ^ #S ≀ ↑(absNorm (∏ i ∈ S, P i)) Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±hnorm:βˆ€ (i : Ξ±), 2 ≀ ↑(absNorm (P i))⊒ 2 ^ #S ≀ ∏ i ∈ S, ↑(absNorm (P i)) calc _ = ∏ _i ∈ S, (2 : ℝ) := Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±hnorm:βˆ€ (i : Ξ±), 2 ≀ ↑(absNorm (P i))⊒ 2 ^ #S = ∏ _i ∈ S, 2 All goals completed! πŸ™ _ ≀ _ := Finset.prod_le_prodβ‚€ (fun _ _ => Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±hnorm:βˆ€ (i : Ξ±), 2 ≀ ↑(absNorm (P i))x✝¹:Ξ±x✝:x✝¹ ∈ S⊒ 0 ≀ 2 All goals completed! πŸ™) (fun i _ => hnorm i)theorem divisor_conductor_bound {Ξ± : Type*} [DecidableEq Ξ±] (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (S T : Finset Ξ±) (N : ℝ) (hN : 0 ≀ N) (hS : supportNorm P S ≀ N) (hT : supportNorm P T ≀ N) : (2 : ℝ) ^ (S ∩ T).card * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N := Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±T:Finset Ξ±N:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ N⊒ 2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±T:Finset Ξ±N:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ Nhid:↑(absNorm ((∏ i ∈ activeSupport S T, P i) * (∏ i ∈ S ∩ T, P i) ^ 2)) = ↑(absNorm ((∏ i ∈ S, P i) * ∏ i ∈ T, P i))⊒ 2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±T:Finset Ξ±N:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ Nhid:↑(absNorm (∏ i ∈ activeSupport S T, P i)) * ↑(absNorm (∏ i ∈ S ∩ T, P i)) ^ 2 = ↑(absNorm (∏ i ∈ S, P i)) * ↑(absNorm (∏ i ∈ T, P i))⊒ 2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±T:Finset Ξ±N:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ Nhid:β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ^ 2 * ↑(absNorm (∏ i ∈ S ∩ T, P i)) ^ 2 = ↑(absNorm (∏ i ∈ S, P i)) * ↑(absNorm (∏ i ∈ T, P i))⊒ 2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±T:Finset Ξ±N:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ Nhid:β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ^ 2 * supportNorm P (S ∩ T) ^ 2 = supportNorm P S * supportNorm P T⊒ 2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±T:Finset Ξ±N:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ Nhid:β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ^ 2 * supportNorm P (S ∩ T) ^ 2 = supportNorm P S * supportNorm P Thpow:2 ^ #(S ∩ T) ≀ supportNorm P (S ∩ T)⊒ 2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±T:Finset Ξ±N:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ Nhid:β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ^ 2 * supportNorm P (S ∩ T) ^ 2 = supportNorm P S * supportNorm P Thpow:2 ^ #(S ∩ T) ≀ supportNorm P (S ∩ T)hmul:2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ supportNorm P (S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–βŠ’ 2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±T:Finset Ξ±N:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ Nhid:β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ^ 2 * supportNorm P (S ∩ T) ^ 2 = supportNorm P S * supportNorm P Thpow:2 ^ #(S ∩ T) ≀ supportNorm P (S ∩ T)hmul:2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ supportNorm P (S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–hsq:(2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–) ^ 2 ≀ (supportNorm P (S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–) ^ 2⊒ 2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalS:Finset Ξ±T:Finset Ξ±N:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ Nhid:β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ^ 2 * supportNorm P (S ∩ T) ^ 2 = supportNorm P S * supportNorm P Thpow:2 ^ #(S ∩ T) ≀ supportNorm P (S ∩ T)hmul:2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ supportNorm P (S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–hsq:(2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–) ^ 2 ≀ (supportNorm P (S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–) ^ 2hprod:supportNorm P S * supportNorm P T ≀ N * N⊒ 2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€– ≀ N All goals completed! πŸ™theorem quadratic_gram_offdiagonal_of_norm_le {Ξ± : Type*} [DecidableEq Ξ±] (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hinj : Function.Injective P) (hg : βˆ€ i, lambda βˆ‰ P i) (hc : βˆ€ i, ringChar (O β§Έ P i) β‰  2) (S T : Finset Ξ±) (hne : S β‰  T) (N : ℝ) (hN : 0 ≀ N) (hS : supportNorm P S ≀ N) (hT : supportNorm P T ≀ N) (W : 𝓒(ℝ, β„‚)) (M : ℝ) (hM : 0 < M) : β€–βˆ‘' z : O, (star (quadraticRow P hg S z) * quadraticRow P hg T z) * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ pvControl W * N := Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2S:Finset Ξ±T:Finset Ξ±hne:S β‰  TN:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ NW:𝓒(ℝ, β„‚)M:ℝhM:0 < M⊒ β€–βˆ‘' (z : O), star (quadraticRow P hg S z) * quadraticRow P hg T z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ pvControl W * N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2S:Finset Ξ±T:Finset Ξ±hne:S β‰  TN:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ NW:𝓒(ℝ, β„‚)M:ℝhM:0 < M⊒ 2 ^ #(S ∩ T) * (pvControl W * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–) ≀ pvControl W * N Ξ±:Type u_1inst✝¹:DecidableEq Ξ±P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2S:Finset Ξ±T:Finset Ξ±hne:S β‰  TN:ℝhN:0 ≀ NhS:supportNorm P S ≀ NhT:supportNorm P T ≀ NW:𝓒(ℝ, β„‚)M:ℝhM:0 < M⊒ pvControl W * (2 ^ #(S ∩ T) * β€–eisEmbedding (finitePrimeModulus (activePrimes P S T))β€–) ≀ pvControl W * N All goals completed! πŸ™def diagonalControl (W : 𝓒(ℝ, β„‚)) : ℝ := 16 * (1 + Real.pi) ^ 2 * (Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚) Wtheorem diagonalControl_nonneg (W : 𝓒(ℝ, β„‚)) : 0 ≀ diagonalControl W := W:𝓒(ℝ, β„‚)⊒ 0 ≀ diagonalControl W W:𝓒(ℝ, β„‚)⊒ 0 ≀ 16 * (1 + Ο€) ^ 2 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) W All goals completed! πŸ™theorem radial_weight_lattice_bound (W : 𝓒(ℝ, β„‚)) (M : ℝ) (hM : 1 ≀ M) : (βˆ‘' z : O, β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–) ≀ diagonalControl W * M := W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ M⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < M⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < t⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) W⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ B⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ Bhp:βˆ€ (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ B * ((1 + t * β€–eisEmbedding zβ€– ^ 2) ^ 2)⁻¹⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ Bhp:βˆ€ (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ B * ((1 + t * β€–eisEmbedding zβ€– ^ 2) ^ 2)⁻¹hs:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–βŠ’ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ Bhp:βˆ€ (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ B * ((1 + t * β€–eisEmbedding zβ€– ^ 2) ^ 2)⁻¹hs:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–hb:βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ βˆ‘' (i : O), B * ((1 + t * β€–eisEmbedding iβ€– ^ 2) ^ 2)⁻¹⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ Bhp:βˆ€ (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ B * ((1 + t * β€–eisEmbedding zβ€– ^ 2) ^ 2)⁻¹hs:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–hb:βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ Bhp:βˆ€ (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ B * ((1 + t * β€–eisEmbedding zβ€– ^ 2) ^ 2)⁻¹hs:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–hb:βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹hsmall:t * βˆ‘' (h : EisensteinSchwartzPoisson.O), ((1 + t * β€–eisEmbedding hβ€– ^ 2) ^ 2)⁻¹ ≀ 4 * (1 + Ο€) ^ 2⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ Bhp:βˆ€ (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ B * ((1 + t * β€–eisEmbedding zβ€– ^ 2) ^ 2)⁻¹hs:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–hb:βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹hsmall:t * βˆ‘' (h : EisensteinSchwartzPoisson.O), ((1 + t * β€–eisEmbedding hβ€– ^ 2) ^ 2)⁻¹ ≀ 4 * (1 + Ο€) ^ 2hmul:t * βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ t * (B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹)⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ Bhp:βˆ€ (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ B * ((1 + t * β€–eisEmbedding zβ€– ^ 2) ^ 2)⁻¹hs:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–hb:βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹hsmall:t * βˆ‘' (h : EisensteinSchwartzPoisson.O), ((1 + t * β€–eisEmbedding hβ€– ^ 2) ^ 2)⁻¹ ≀ 4 * (1 + Ο€) ^ 2hmul:t * βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ t * (B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹)hcontrol:B * (t * βˆ‘' (h : EisensteinSchwartzPoisson.O), ((1 + t * β€–eisEmbedding hβ€– ^ 2) ^ 2)⁻¹) ≀ B * (4 * (1 + Ο€) ^ 2)⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ Bhp:βˆ€ (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ B * ((1 + t * β€–eisEmbedding zβ€– ^ 2) ^ 2)⁻¹hs:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–hb:βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹hsmall:t * βˆ‘' (h : EisensteinSchwartzPoisson.O), ((1 + t * β€–eisEmbedding hβ€– ^ 2) ^ 2)⁻¹ ≀ 4 * (1 + Ο€) ^ 2hmul:t * βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ t * (B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹)hcontrol:B * (t * βˆ‘' (h : EisensteinSchwartzPoisson.O), ((1 + t * β€–eisEmbedding hβ€– ^ 2) ^ 2)⁻¹) ≀ B * (4 * (1 + Ο€) ^ 2)hfinal:t * βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mt:ℝ := M⁻¹ht:0 < tht1:t ≀ 1B:ℝ := 4 * ((Finset.Iic (2, 0)).sup (schwartzSeminormFamily ℝ ℝ β„‚)) WhB:0 ≀ Bhp:βˆ€ (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ B * ((1 + t * β€–eisEmbedding zβ€– ^ 2) ^ 2)⁻¹hs:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–hb:βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹hsmall:t * βˆ‘' (h : EisensteinSchwartzPoisson.O), ((1 + t * β€–eisEmbedding hβ€– ^ 2) ^ 2)⁻¹ ≀ 4 * (1 + Ο€) ^ 2hmul:t * βˆ‘' (i : O), β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ t * (B * βˆ‘' (x : O), ((1 + t * β€–eisEmbedding xβ€– ^ 2) ^ 2)⁻¹)hcontrol:B * (t * βˆ‘' (h : EisensteinSchwartzPoisson.O), ((1 + t * β€–eisEmbedding hβ€– ^ 2) ^ 2)⁻¹) ≀ B * (4 * (1 + Ο€) ^ 2)hfinal:t * βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl Whh:M * (t * βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–) ≀ M * diagonalControl W⊒ βˆ‘' (z : O), β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M All goals completed! πŸ™theorem quadraticRow_norm_le_one {Ξ± : Type*} (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (S : Finset Ξ±) (z : O) : β€–quadraticRow P hg S zβ€– ≀ 1 := Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:O⊒ β€–quadraticRow P hg S zβ€– ≀ 1 Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±z:O⊒ β€–finiteSexticRow (fun i => P ↑i) β‹― (fun x => 3) zβ€– ≀ 1 All goals completed! πŸ™theorem quadratic_pair_summable {Ξ± : Type*} (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (S T : Finset Ξ±) (W : 𝓒(ℝ, β„‚)) (M : ℝ) (hM : 0 < M) : Summable (fun z : O => (star (quadraticRow P hg S z) * quadraticRow P hg T z) * W (β€–eisEmbedding zβ€– ^ 2 / M)) := Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:0 < M⊒ Summable fun z => star (quadraticRow P hg S z) * quadraticRow P hg T z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:0 < MhW:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–βŠ’ Summable fun z => star (quadraticRow P hg S z) * quadraticRow P hg T z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:0 < MhW:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–βŠ’ Summable fun a => β€–star (quadraticRow P hg S a) * quadraticRow P hg T a * W (β€–eisEmbedding aβ€– ^ 2 / M)β€– Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:0 < MhW:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–βŠ’ βˆ€ (b : O), β€–star (quadraticRow P hg S b) * quadraticRow P hg T b * W (β€–eisEmbedding bβ€– ^ 2 / M)β€– ≀ β€–W (β€–eisEmbedding bβ€– ^ 2 / M)β€– Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:0 < MhW:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–z:O⊒ β€–star (quadraticRow P hg S z) * quadraticRow P hg T z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±T:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:0 < MhW:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–z:O⊒ β€–quadraticRow P hg S zβ€– * β€–quadraticRow P hg T zβ€– * β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– All goals completed! πŸ™theorem quadratic_gram_diagonal {Ξ± : Type*} (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (S : Finset Ξ±) (W : 𝓒(ℝ, β„‚)) (M : ℝ) (hM : 1 ≀ M) : β€–βˆ‘' z : O, (star (quadraticRow P hg S z) * quadraticRow P hg S z) * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M := Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ M⊒ β€–βˆ‘' (z : O), star (quadraticRow P hg S z) * quadraticRow P hg S z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < M⊒ β€–βˆ‘' (z : O), star (quadraticRow P hg S z) * quadraticRow P hg S z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mhs:Summable fun x => β€–star (quadraticRow P hg S x) * quadraticRow P hg S x * W (β€–eisEmbedding xβ€– ^ 2 / M)β€–βŠ’ β€–βˆ‘' (z : O), star (quadraticRow P hg S z) * quadraticRow P hg S z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mhs:Summable fun x => β€–star (quadraticRow P hg S x) * quadraticRow P hg S x * W (β€–eisEmbedding xβ€– ^ 2 / M)β€–hW:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–βŠ’ β€–βˆ‘' (z : O), star (quadraticRow P hg S z) * quadraticRow P hg S z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ diagonalControl W * M Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mhs:Summable fun x => β€–star (quadraticRow P hg S x) * quadraticRow P hg S x * W (β€–eisEmbedding xβ€– ^ 2 / M)β€–hW:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–βŠ’ βˆ€ (i : O), β€–star (quadraticRow P hg S i) * quadraticRow P hg S i * W (β€–eisEmbedding iβ€– ^ 2 / M)β€– ≀ β€–W (β€–eisEmbedding iβ€– ^ 2 / M)β€– Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mhs:Summable fun x => β€–star (quadraticRow P hg S x) * quadraticRow P hg S x * W (β€–eisEmbedding xβ€– ^ 2 / M)β€–hW:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–z:O⊒ β€–star (quadraticRow P hg S z) * quadraticRow P hg S z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– Ξ±:Type u_1P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iS:Finset Ξ±W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < Mhs:Summable fun x => β€–star (quadraticRow P hg S x) * quadraticRow P hg S x * W (β€–eisEmbedding xβ€– ^ 2 / M)β€–hW:Summable fun z => β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€–z:O⊒ β€–quadraticRow P hg S zβ€– * β€–quadraticRow P hg S zβ€– * β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ β€–W (β€–eisEmbedding zβ€– ^ 2 / M)β€– All goals completed! πŸ™private theorem norm_sq_finite_sum {Ξ² : Type*} (C : Finset Ξ²) (a r : Ξ² β†’ β„‚) : (↑(β€–βˆ‘ n ∈ C, a n * r nβ€– ^ 2) : β„‚) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, (star (a n) * a m) * (star (r n) * r m) := Ξ²:Type u_1C:Finset Ξ²a:Ξ² β†’ β„‚r:Ξ² β†’ β„‚βŠ’ ↑(β€–βˆ‘ n ∈ C, a n * r nβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * (star (r n) * r m) Ξ²:Type u_1C:Finset Ξ²a:Ξ² β†’ β„‚r:Ξ² β†’ β„‚βŠ’ (starRingEnd β„‚) (βˆ‘ n ∈ C, a n * r n) * βˆ‘ n ∈ C, a n * r n = βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * (star (r n) * r m) Ξ²:Type u_1C:Finset Ξ²a:Ξ² β†’ β„‚r:Ξ² β†’ β„‚βŠ’ (βˆ‘ x ∈ C, star (a x) * star (r x)) * βˆ‘ n ∈ C, a n * r n = βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * (star (r n) * r m) Ξ²:Type u_1C:Finset Ξ²a:Ξ² β†’ β„‚r:Ξ² β†’ β„‚βŠ’ βˆ‘ i ∈ C, βˆ‘ j ∈ C, star (a i) * star (r i) * (a j * r j) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * (star (r n) * r m) Ξ²:Type u_1C:Finset Ξ²a:Ξ² β†’ β„‚r:Ξ² β†’ β„‚βŠ’ βˆ€ x ∈ C, βˆ‘ j ∈ C, star (a x) * star (r x) * (a j * r j) = βˆ‘ m ∈ C, star (a x) * a m * (star (r x) * r m) Ξ²:Type u_1C:Finset Ξ²a:Ξ² β†’ β„‚r:Ξ² β†’ β„‚n:Ξ²hn:n ∈ C⊒ βˆ‘ j ∈ C, star (a n) * star (r n) * (a j * r j) = βˆ‘ m ∈ C, star (a n) * a m * (star (r n) * r m) Ξ²:Type u_1C:Finset Ξ²a:Ξ² β†’ β„‚r:Ξ² β†’ β„‚n:Ξ²hn:n ∈ C⊒ βˆ€ x ∈ C, star (a n) * star (r n) * (a x * r x) = star (a n) * a x * (star (r n) * r x) Ξ²:Type u_1C:Finset Ξ²a:Ξ² β†’ β„‚r:Ξ² β†’ β„‚n:Ξ²hn:n ∈ Cm:Ξ²hm:m ∈ C⊒ star (a n) * star (r n) * (a m * r m) = star (a n) * a m * (star (r n) * r m) All goals completed! πŸ™theorem quadratic_mean_summable {Ξ± Ξ² : Type*} (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (C : Finset Ξ²) (support : Ξ² β†’ Finset Ξ±) (a : Ξ² β†’ β„‚) (W : 𝓒(ℝ, β„‚)) (M : ℝ) (hM : 0 < M) : Summable (fun z : O => W (β€–eisEmbedding zβ€– ^ 2 / M) * (↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) : β„‚)) := Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < M⊒ Summable fun z => W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mhs:Summable fun b => βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M))⊒ Summable fun z => W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mhs:Summable fun b => βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M))⊒ βˆ€ (b : O), βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M)) = W (β€–eisEmbedding bβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) bβ€– ^ 2) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mhs:Summable fun b => βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M))z:O⊒ βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) z) * quadraticRow P hg (support i_1) z * W (β€–eisEmbedding zβ€– ^ 2 / M)) = W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mhs:Summable fun b => βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M))z:O⊒ βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) z) * quadraticRow P hg (support i_1) z * W (β€–eisEmbedding zβ€– ^ 2 / M)) = W (β€–eisEmbedding zβ€– ^ 2 / M) * βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mhs:Summable fun b => βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M))z:O⊒ βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) z) * quadraticRow P hg (support i_1) z * W (β€–eisEmbedding zβ€– ^ 2 / M)) = βˆ‘ x ∈ C, βˆ‘ i ∈ C, W (β€–eisEmbedding zβ€– ^ 2 / M) * (star (a x) * a i * (star (quadraticRow P hg (support x) z) * quadraticRow P hg (support i) z)) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mhs:Summable fun b => βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M))z:O⊒ βˆ€ x ∈ C, βˆ‘ i ∈ C, star (a x) * a i * (star (quadraticRow P hg (support x) z) * quadraticRow P hg (support i) z * W (β€–eisEmbedding zβ€– ^ 2 / M)) = βˆ‘ i ∈ C, W (β€–eisEmbedding zβ€– ^ 2 / M) * (star (a x) * a i * (star (quadraticRow P hg (support x) z) * quadraticRow P hg (support i) z)) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mhs:Summable fun b => βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M))z:On:Ξ²hn:n ∈ C⊒ βˆ‘ i ∈ C, star (a n) * a i * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support i) z * W (β€–eisEmbedding zβ€– ^ 2 / M)) = βˆ‘ i ∈ C, W (β€–eisEmbedding zβ€– ^ 2 / M) * (star (a n) * a i * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support i) z)) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mhs:Summable fun b => βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M))z:On:Ξ²hn:n ∈ C⊒ βˆ€ x ∈ C, star (a n) * a x * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support x) z * W (β€–eisEmbedding zβ€– ^ 2 / M)) = W (β€–eisEmbedding zβ€– ^ 2 / M) * (star (a n) * a x * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support x) z)) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mhs:Summable fun b => βˆ‘ i ∈ C, βˆ‘ i_1 ∈ C, star (a i) * a i_1 * (star (quadraticRow P hg (support i) b) * quadraticRow P hg (support i_1) b * W (β€–eisEmbedding bβ€– ^ 2 / M))z:On:Ξ²hn:n ∈ Cm:Ξ²hm:m ∈ C⊒ star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)) = W (β€–eisEmbedding zβ€– ^ 2 / M) * (star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z)) All goals completed! πŸ™theorem quadratic_mean_expand {Ξ± Ξ² : Type*} (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hg : βˆ€ i, lambda βˆ‰ P i) (C : Finset Ξ²) (support : Ξ² β†’ Finset Ξ±) (a : Ξ² β†’ β„‚) (W : 𝓒(ℝ, β„‚)) (M : ℝ) (hM : 0 < M) : (βˆ‘' z : O, W (β€–eisEmbedding zβ€– ^ 2 / M) * (↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) : β„‚)) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, (star (a n) * a m) * βˆ‘' z : O, (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z) * W (β€–eisEmbedding zβ€– ^ 2 / M) := Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < M⊒ βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mf:Ξ² β†’ Ξ² β†’ O β†’ β„‚ := fun n m z => star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M))⊒ βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mf:Ξ² β†’ Ξ² β†’ O β†’ β„‚ := fun n m z => star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M))hf:βˆ€ (n m : Ξ²), Summable (f n m)⊒ βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mf:Ξ² β†’ Ξ² β†’ O β†’ β„‚ := fun n m z => star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M))hf:βˆ€ (n m : Ξ²), Summable (f n m)heq:βˆ€ (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, f n m z⊒ βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mf:Ξ² β†’ Ξ² β†’ O β†’ β„‚ := fun n m z => star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M))hf:βˆ€ (n m : Ξ²), Summable (f n m)heq:βˆ€ (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, f n m z⊒ βˆ‘ i ∈ C, βˆ‘' (b : O), βˆ‘ i_1 ∈ C, f i i_1 b = βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mf:Ξ² β†’ Ξ² β†’ O β†’ β„‚ := fun n m z => star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M))hf:βˆ€ (n m : Ξ²), Summable (f n m)heq:βˆ€ (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, f n m z⊒ βˆ€ x ∈ C, βˆ‘' (b : O), βˆ‘ i ∈ C, f x i b = βˆ‘ m ∈ C, star (a x) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support x) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mf:Ξ² β†’ Ξ² β†’ O β†’ β„‚ := fun n m z => star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M))hf:βˆ€ (n m : Ξ²), Summable (f n m)heq:βˆ€ (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, f n m zn:Ξ²hn:n ∈ C⊒ βˆ‘' (b : O), βˆ‘ i ∈ C, f n i b = βˆ‘ m ∈ C, star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mf:Ξ² β†’ Ξ² β†’ O β†’ β„‚ := fun n m z => star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M))hf:βˆ€ (n m : Ξ²), Summable (f n m)heq:βˆ€ (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, f n m zn:Ξ²hn:n ∈ C⊒ βˆ‘ i ∈ C, βˆ‘' (b : O), f n i b = βˆ‘ m ∈ C, star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mf:Ξ² β†’ Ξ² β†’ O β†’ β„‚ := fun n m z => star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M))hf:βˆ€ (n m : Ξ²), Summable (f n m)heq:βˆ€ (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, f n m zn:Ξ²hn:n ∈ C⊒ βˆ€ x ∈ C, βˆ‘' (b : O), f n x b = star (a n) * a x * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support x) z * W (β€–eisEmbedding zβ€– ^ 2 / M) Ξ±:Type u_1Ξ²:Type u_2P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhg:βˆ€ (i : Ξ±), lambda βˆ‰ P iC:Finset Ξ²support:Ξ² β†’ Finset Ξ±a:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:0 < Mf:Ξ² β†’ Ξ² β†’ O β†’ β„‚ := fun n m z => star (a n) * a m * (star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M))hf:βˆ€ (n m : Ξ²), Summable (f n m)heq:βˆ€ (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) = βˆ‘ n ∈ C, βˆ‘ m ∈ C, f n m zn:Ξ²hn:n ∈ Cm:Ξ²hm:m ∈ C⊒ βˆ‘' (b : O), f n m b = star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M) All goals completed! πŸ™theorem quadratic_initial_mean_bound {Ξ± Ξ² : Type*} [DecidableEq Ξ±] [DecidableEq Ξ²] (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hinj : Function.Injective P) (hg : βˆ€ i, lambda βˆ‰ P i) (hc : βˆ€ i, ringChar (O β§Έ P i) β‰  2) (C : Finset Ξ²) (support : Ξ² β†’ Finset Ξ±) (hsupp : Set.InjOn support (↑C : Set Ξ²)) (N : ℝ) (hN : 0 ≀ N) (hNorm : βˆ€ n ∈ C, supportNorm P (support n) ≀ N) (a : Ξ² β†’ β„‚) (W : 𝓒(ℝ, β„‚)) (M : ℝ) (hM : 1 ≀ M) : β€–βˆ‘' z : O, W (β€–eisEmbedding zβ€– ^ 2 / M) * (↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) : β„‚)β€– ≀ (diagonalControl W * M + pvControl W * N * C.card) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 := Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ M⊒ β€–βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < M⊒ β€–βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * M⊒ β€–βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * N⊒ β€–βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ B⊒ β€–βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)⊒ β€–βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + B⊒ β€–βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–βŠ’ β€–βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ β€–βˆ‘' (z : O), W (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ β€–βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 calc _ ≀ βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–(star (a n) * a m) * K n mβ€– := Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ β€–βˆ‘ n ∈ C, βˆ‘ m ∈ C, star (a n) * a m * βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)β€– ≀ βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–star (a n) * a m * K n mβ€– All goals completed! πŸ™ _ ≀ βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) := Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–star (a n) * a m * K n mβ€– ≀ βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ βˆ€ i ∈ C, βˆ‘ m ∈ C, β€–star (a i) * a m * K i mβ€– ≀ βˆ‘ m ∈ C, β€–a iβ€– * β€–a mβ€– * ((if i = m then D else 0) + B) Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2n:Ξ²hn:n ∈ C⊒ βˆ‘ m ∈ C, β€–star (a n) * a m * K n mβ€– ≀ βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2n:Ξ²hn:n ∈ C⊒ βˆ€ i ∈ C, β€–star (a n) * a i * K n iβ€– ≀ β€–a nβ€– * β€–a iβ€– * ((if n = i then D else 0) + B) Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2n:Ξ²hn:n ∈ Cm:Ξ²hm:m ∈ C⊒ β€–star (a n) * a m * K n mβ€– ≀ β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2n:Ξ²hn:n ∈ Cm:Ξ²hm:m ∈ C⊒ β€–a nβ€– * β€–a mβ€– * β€–K n mβ€– ≀ β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) All goals completed! πŸ™ _ = D * (βˆ‘ n ∈ C, β€–a nβ€– ^ 2) + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2 := hcalc _ ≀ D * (βˆ‘ n ∈ C, β€–a nβ€– ^ 2) + B * ((C.card : ℝ) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2) := Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2 ≀ D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (↑(#C) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2) Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2 ≀ B * (↑(#C) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2) Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2 ≀ ↑(#C) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 All goals completed! πŸ™ _ = _ := Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (↑(#C) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2) = (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚W:𝓒(ℝ, β„‚)M:ℝhM:1 ≀ MhMp:0 < MD:ℝ := diagonalControl W * MB:ℝ := pvControl W * NhB:0 ≀ BK:Ξ² β†’ Ξ² β†’ β„‚ := fun n m => βˆ‘' (z : O), star (quadraticRow P hg (support n) z) * quadraticRow P hg (support m) z * W (β€–eisEmbedding zβ€– ^ 2 / M)hK:βˆ€ n ∈ C, βˆ€ m ∈ C, β€–K n mβ€– ≀ (if n = m then D else 0) + Bheq:βˆ€ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * β€–a nβ€– ^ 2 + B * β€–a nβ€– * βˆ‘ m ∈ C, β€–a mβ€–hcalc:βˆ‘ n ∈ C, βˆ‘ m ∈ C, β€–a nβ€– * β€–a mβ€– * ((if n = m then D else 0) + B) = D * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + B * (βˆ‘ n ∈ C, β€–a nβ€–) ^ 2⊒ diagonalControl W * M * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 + pvControl W * N * (↑(#C) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2) = (diagonalControl W * M + pvControl W * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2; All goals completed! πŸ™def sieveBump : ContDiffBump (0 : ℝ) where rIn := 1 rOut := 2 rIn_pos := ⊒ 0 < 1 All goals completed! πŸ™ rIn_lt_rOut := ⊒ 1 < 2 All goals completed! πŸ™def sieveCutoff : 𝓒(ℝ, β„‚) := ⊒ 𝓒(ℝ, β„‚) hc:HasCompactSupport fun t => ↑(↑sieveBump t)⊒ 𝓒(ℝ, β„‚) hc:HasCompactSupport fun t => ↑(↑sieveBump t)hs:ContDiff ℝ ∞ fun t => ↑(↑sieveBump t)⊒ 𝓒(ℝ, β„‚) All goals completed! πŸ™@[simp] theorem sieveCutoff_apply (t : ℝ) : sieveCutoff t = (sieveBump t : β„‚) := rfltheorem sieveBump_eq_one {t : ℝ} (ht0 : 0 ≀ t) (ht1 : t ≀ 1) : sieveBump t = 1 := t:ℝht0:0 ≀ tht1:t ≀ 1⊒ ↑sieveBump t = 1 t:ℝht0:0 ≀ tht1:t ≀ 1⊒ t ∈ Metric.closedBall 0 sieveBump.rIn t:ℝht0:0 ≀ tht1:t ≀ 1⊒ dist t 0 ≀ 1 All goals completed! πŸ™theorem quadratic_initial_finite_bound {Ξ± Ξ² : Type*} [DecidableEq Ξ±] [DecidableEq Ξ²] (P : Ξ± β†’ Ideal O) [βˆ€ i, (P i).IsMaximal] (hinj : Function.Injective P) (hg : βˆ€ i, lambda βˆ‰ P i) (hc : βˆ€ i, ringChar (O β§Έ P i) β‰  2) (C : Finset Ξ²) (support : Ξ² β†’ Finset Ξ±) (hsupp : Set.InjOn support (↑C : Set Ξ²)) (N : ℝ) (hN : 0 ≀ N) (hNorm : βˆ€ n ∈ C, supportNorm P (support n) ≀ N) (a : Ξ² β†’ β„‚) (M : ℝ) (hM : 1 ≀ M) (R : Finset O) (hR : βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ M) : (βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2) ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * C.card) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 := Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ M⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < M⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E z⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F z⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F zhH:βˆ€ (z : O), H z = ↑(F z)⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F zhH:βˆ€ (z : O), H z = ↑(F z)hHs:Summable H⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F zhH:βˆ€ (z : O), H z = ↑(F z)hHs:Summable HhFs:Summable F⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F zhH:βˆ€ (z : O), H z = ↑(F z)hHs:Summable HhFs:Summable Fhsum:β€–βˆ‘' (z : O), H zβ€– = βˆ‘' (z : O), F z⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * N * ↑(#C)) * βˆ‘ n ∈ C, β€–a nβ€– ^ 2 calc _ = βˆ‘ z ∈ R, F z := Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F zhH:βˆ€ (z : O), H z = ↑(F z)hHs:Summable HhFs:Summable Fhsum:β€–βˆ‘' (z : O), H zβ€– = βˆ‘' (z : O), F z⊒ βˆ‘ z ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 = βˆ‘ z ∈ R, F z Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F zhH:βˆ€ (z : O), H z = ↑(F z)hHs:Summable HhFs:Summable Fhsum:β€–βˆ‘' (z : O), H zβ€– = βˆ‘' (z : O), F z⊒ βˆ€ x ∈ R, β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) xβ€– ^ 2 = F x Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F zhH:βˆ€ (z : O), H z = ↑(F z)hHs:Summable HhFs:Summable Fhsum:β€–βˆ‘' (z : O), H zβ€– = βˆ‘' (z : O), F zz:Ohz:z ∈ R⊒ β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 = F z Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F zhH:βˆ€ (z : O), H z = ↑(F z)hHs:Summable HhFs:Summable Fhsum:β€–βˆ‘' (z : O), H zβ€– = βˆ‘' (z : O), F zz:Ohz:z ∈ Rht0:0 ≀ β€–eisEmbedding zβ€– ^ 2 / M⊒ β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 = F z Ξ±:Type u_1Ξ²:Type u_2inst✝²:DecidableEq Ξ±inst✝¹:DecidableEq Ξ²P:Ξ± β†’ Ideal Oinst✝:βˆ€ (i : Ξ±), (P i).IsMaximalhinj:Function.Injective Phg:βˆ€ (i : Ξ±), lambda βˆ‰ P ihc:βˆ€ (i : Ξ±), ringChar (O β§Έ P i) β‰  2C:Finset Ξ²support:Ξ² β†’ Finset Ξ±hsupp:InjOn support ↑CN:ℝhN:0 ≀ NhNorm:βˆ€ n ∈ C, supportNorm P (support n) ≀ Na:Ξ² β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ MhMp:0 < ME:O β†’ ℝ := fun z => β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2F:O β†’ ℝ := fun z => ↑sieveBump (β€–eisEmbedding zβ€– ^ 2 / M) * E zH:O β†’ β„‚ := fun z => sieveCutoff (β€–eisEmbedding zβ€– ^ 2 / M) * ↑(E z)hF:βˆ€ (z : O), 0 ≀ F zhH:βˆ€ (z : O), H z = ↑(F z)hHs:Summable HhFs:Summable Fhsum:β€–βˆ‘' (z : O), H zβ€– = βˆ‘' (z : O), F zz:Ohz:z ∈ Rht0:0 ≀ β€–eisEmbedding zβ€– ^ 2 / Mht1:β€–eisEmbedding zβ€– ^ 2 / M ≀ 1⊒ β€–βˆ‘ n ∈ C, a n * quadraticRow P hg (support n) zβ€– ^ 2 = F z All goals completed! πŸ™ _ ≀ βˆ‘' z : O, F z := hFs.sum_le_tsum R (fun z _ => hF z) _ = β€–βˆ‘' z : O, H zβ€– := hsum.symm _ ≀ _ := quadratic_initial_mean_bound P hinj hg hc C support hsupp N hN hNorm a sieveCutoff M hMopen ActualEisensteinCubic ConcreteTraceCRT EisensteinSchwartzPoissonopen ConcretePrimeRowBridge ShortDraftHeckeBridgedef initialSieveConstant : ℝ := diagonalControl sieveCutoff + 128 * pvControl sieveCutoff + 1theorem initialSieveConstant_pos : 0 < initialSieveConstant := ⊒ 0 < initialSieveConstant this:0 ≀ diagonalControl sieveCutoff⊒ 0 < initialSieveConstant this✝:0 ≀ diagonalControl sieveCutoffthis:0 ≀ pvControl sieveCutoff⊒ 0 < initialSieveConstant this✝:0 ≀ diagonalControl sieveCutoffthis:0 ≀ pvControl sieveCutoff⊒ 0 < diagonalControl sieveCutoff + 128 * pvControl sieveCutoff + 1 All goals completed! πŸ™theorem ideal_initial_quadratic_sieve (F : Finset (Ideal O)) (hFpos : βˆ€ I ∈ F, I β‰  βŠ₯) (hFgood : βˆ€ I ∈ F, βˆ€ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda βˆ‰ P) (hsq : βˆ€ I ∈ F, Squarefree I) (hchar : βˆ€ i : primePool F, ringChar (O β§Έ i.val) β‰  2) (N : β„•) (hN : 1 ≀ N) (hnorm : βˆ€ I ∈ F, Ideal.absNorm I ≀ N) (a : Ideal O β†’ β„‚) (M : ℝ) (hM : 1 ≀ M) (R : Finset O) (hR : βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ M) : (βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * (idealSexticRow F hFpos hFgood I z) ^ 3β€– ^ 2) ≀ initialSieveConstant * (M + (N : ℝ) ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 := F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ M⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := ···⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑N⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑F⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑N⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ n ∈ F, a n * quadraticRow (fun i => ↑i) β‹― (idealSupport F n) zβ€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ n ∈ F, β€–a nβ€– ^ 2⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2hsub:F βŠ† idealsUpTo N⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2hsub:F βŠ† idealsUpTo NhcardNat:#F ≀ 64 * (N + 1)⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2hsub:F βŠ† idealsUpTo NhcardNat:#F ≀ 64 * (N + 1)hcard:↑(#F) ≀ 128 * ↑N⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2hsub:F βŠ† idealsUpTo NhcardNat:#F ≀ 64 * (N + 1)hcard:↑(#F) ≀ 128 * ↑N⊒ diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F) ≀ initialSieveConstant * (M + ↑N ^ 2) F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2hsub:F βŠ† idealsUpTo NhcardNat:#F ≀ 64 * (N + 1)hcard:↑(#F) ≀ 128 * ↑Nhdiag:0 ≀ diagonalControl sieveCutoff⊒ diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F) ≀ initialSieveConstant * (M + ↑N ^ 2) F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2hsub:F βŠ† idealsUpTo NhcardNat:#F ≀ 64 * (N + 1)hcard:↑(#F) ≀ 128 * ↑Nhdiag:0 ≀ diagonalControl sieveCutoffhpv:0 ≀ pvControl sieveCutoff⊒ diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F) ≀ initialSieveConstant * (M + ↑N ^ 2) F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2hsub:F βŠ† idealsUpTo NhcardNat:#F ≀ 64 * (N + 1)hcard:↑(#F) ≀ 128 * ↑Nhdiag:0 ≀ diagonalControl sieveCutoffhpv:0 ≀ pvControl sieveCutoffhmul:pvControl sieveCutoff * ↑N * ↑(#F) ≀ pvControl sieveCutoff * ↑N * (128 * ↑N)⊒ diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F) ≀ initialSieveConstant * (M + ↑N ^ 2) F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ Mthis:βˆ€ (i : β†₯(primePool F)), (↑i).IsMaximal := Β·Β·Β·hNr:1 ≀ ↑Nhsupp:InjOn (idealSupport F) ↑FhNorm:βˆ€ I ∈ F, supportNorm (fun i => ↑i) (idealSupport F I) ≀ ↑Nhb:βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ (diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F)) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2hsub:F βŠ† idealsUpTo NhcardNat:#F ≀ 64 * (N + 1)hcard:↑(#F) ≀ 128 * ↑Nhdiag:0 ≀ diagonalControl sieveCutoffhpv:0 ≀ pvControl sieveCutoffhmul:pvControl sieveCutoff * ↑N * ↑(#F) ≀ pvControl sieveCutoff * ↑N * (128 * ↑N)⊒ diagonalControl sieveCutoff * M + pvControl sieveCutoff * ↑N * ↑(#F) ≀ (diagonalControl sieveCutoff + 128 * pvControl sieveCutoff + 1) * (M + ↑N ^ 2) nlinarith [mul_nonneg hdiag (sq_nonneg (N : ℝ)), mul_nonneg hpv (show 0 ≀ M F:Finset (Ideal O)hFpos:βˆ€ I ∈ F, I β‰  βŠ₯hFgood:βˆ€ I ∈ F, βˆ€ P ∈ normalizedFactors I, goodLambda βˆ‰ Phsq:βˆ€ I ∈ F, Squarefree Ihchar:βˆ€ (i : β†₯(primePool F)), ringChar (O β§Έ ↑i) β‰  2N:β„•hN:1 ≀ Nhnorm:βˆ€ I ∈ F, absNorm I ≀ Na:Ideal O β†’ β„‚M:ℝhM:1 ≀ MR:Finset OhR:βˆ€ z ∈ R, β€–eisEmbedding zβ€– ^ 2 ≀ M⊒ βˆ‘ z ∈ R, β€–βˆ‘ I ∈ F, a I * idealSexticRow F hFpos hFgood I z ^ 3β€– ^ 2 ≀ initialSieveConstant * (M + ↑N ^ 2) * βˆ‘ I ∈ F, β€–a Iβ€– ^ 2 All goals completed! πŸ™)]end QuadraticInitialBoundopen scoped Classical FourierTransform SchwartzMap ContDiffopen MeasureTheorynamespace CubicReflectionKerneldef gammaMultiplier (s : β„‚) : β„‚ := Complex.Gamma ((7 / 6 : β„‚) + s) * Complex.Gamma ((5 / 6 : β„‚) + s) / (Complex.Gamma ((7 / 6 : β„‚) - s) * Complex.Gamma ((5 / 6 : β„‚) - s))theorem gammaMultiplier_neg (s : β„‚) : gammaMultiplier (-s) = (gammaMultiplier s)⁻¹ := s:β„‚βŠ’ gammaMultiplier (-s) = (gammaMultiplier s)⁻¹ All goals completed! πŸ™theorem Gamma_vertical_ne_zero (a u : ℝ) (ha : 0 < a) : Complex.Gamma ((a : β„‚) + u * Complex.I) β‰  0 := a:ℝu:ℝha:0 < a⊒ Complex.Gamma (↑a + ↑u * I) β‰  0 a:ℝu:ℝha:0 < a⊒ 0 < (↑a + ↑u * I).re All goals completed! πŸ™theorem Gamma_vertical_conj (a u : ℝ) : Complex.Gamma ((a : β„‚) - u * Complex.I) = star (Complex.Gamma ((a : β„‚) + u * Complex.I)) := a:ℝu:β„βŠ’ Complex.Gamma (↑a - ↑u * I) = star (Complex.Gamma (↑a + ↑u * I)) a:ℝu:β„βŠ’ Complex.Gamma (↑a - ↑u * I) = (starRingEnd β„‚) (Complex.Gamma (↑a + ↑u * I)) a:ℝu:β„βŠ’ Complex.Gamma (↑a - ↑u * I) = Complex.Gamma ((starRingEnd β„‚) (↑a + ↑u * I)) a:ℝu:β„βŠ’ ↑a - ↑u * I = (starRingEnd β„‚) (↑a + ↑u * I) All goals completed! πŸ™theorem gammaMultiplier_norm_imaginary (u : ℝ) : β€–gammaMultiplier (u * Complex.I)β€– = 1 := u:β„βŠ’ β€–gammaMultiplier (↑u * I)β€– = 1 u:ℝha:Complex.Gamma (↑(7 / 6) + ↑u * I) β‰  0⊒ β€–gammaMultiplier (↑u * I)β€– = 1 u:ℝha:Complex.Gamma (↑(7 / 6) + ↑u * I) β‰  0hb:Complex.Gamma (↑(5 / 6) + ↑u * I) β‰  0⊒ β€–gammaMultiplier (↑u * I)β€– = 1 u:ℝha:Complex.Gamma (↑(7 / 6) + ↑u * I) β‰  0hb:Complex.Gamma (↑(5 / 6) + ↑u * I) β‰  0hca:Complex.Gamma (↑(7 / 6) - ↑u * I) = star (Complex.Gamma (↑(7 / 6) + ↑u * I))⊒ β€–gammaMultiplier (↑u * I)β€– = 1 u:ℝha:Complex.Gamma (↑(7 / 6) + ↑u * I) β‰  0hb:Complex.Gamma (↑(5 / 6) + ↑u * I) β‰  0hca:Complex.Gamma (↑(7 / 6) - ↑u * I) = star (Complex.Gamma (↑(7 / 6) + ↑u * I))hcb:Complex.Gamma (↑(5 / 6) - ↑u * I) = star (Complex.Gamma (↑(5 / 6) + ↑u * I))⊒ β€–gammaMultiplier (↑u * I)β€– = 1 u:ℝha:Complex.Gamma (7 / 6 + ↑u * I) β‰  0hb:Complex.Gamma (5 / 6 + ↑u * I) β‰  0hca:Complex.Gamma (7 / 6 - ↑u * I) = star (Complex.Gamma (7 / 6 + ↑u * I))hcb:Complex.Gamma (5 / 6 - ↑u * I) = star (Complex.Gamma (5 / 6 + ↑u * I))⊒ β€–gammaMultiplier (↑u * I)β€– = 1 u:ℝha:Complex.Gamma (7 / 6 + ↑u * I) β‰  0hb:Complex.Gamma (5 / 6 + ↑u * I) β‰  0hca:Complex.Gamma (7 / 6 - ↑u * I) = star (Complex.Gamma (7 / 6 + ↑u * I))hcb:Complex.Gamma (5 / 6 - ↑u * I) = star (Complex.Gamma (5 / 6 + ↑u * I))⊒ β€–Complex.Gamma (7 / 6 + ↑u * I)β€– * β€–Complex.Gamma (5 / 6 + ↑u * I)β€– / (β€–Complex.Gamma (7 / 6 + ↑u * I)β€– * β€–Complex.Gamma (5 / 6 + ↑u * I)β€–) = 1 All goals completed! πŸ™theorem Gamma_vertical_continuous (a : ℝ) (ha : 0 < a) : Continuous (fun u : ℝ => Complex.Gamma ((a : β„‚) + u * Complex.I)) := a:ℝha:0 < a⊒ Continuous fun u => Complex.Gamma (↑a + ↑u * I) a:ℝha:0 < a⊒ βˆ€ (x : ℝ), ContinuousAt (fun u => Complex.Gamma (↑a + ↑u * I)) x a:ℝha:0 < au:β„βŠ’ ContinuousAt (fun u => Complex.Gamma (↑a + ↑u * I)) u a:ℝha:0 < au:β„βŠ’ ContinuousAt (fun u => ↑a + ↑u * I) ua:ℝha:0 < au:β„βŠ’ βˆ€ (m : β„•), ↑a + ↑u * I β‰  -↑m a:ℝha:0 < au:β„βŠ’ ContinuousAt (fun u => ↑a + ↑u * I) u All goals completed! πŸ™ a:ℝha:0 < au:β„βŠ’ βˆ€ (m : β„•), ↑a + ↑u * I β‰  -↑m a:ℝha:0 < au:ℝn:β„•hn:↑a + ↑u * I = -↑n⊒ False a:ℝha:0 < au:ℝn:β„•hn:↑a + ↑u * I = -↑nheq:(↑a + ↑u * I).re = (-↑n).re⊒ False a:ℝha:0 < au:ℝn:β„•hn:↑a + ↑u * I = -↑nheq:a = -↑n⊒ False a:ℝha:0 < au:ℝn:β„•hn:↑a + ↑u * I = -↑nheq:a = -↑nthis:0 ≀ ↑n⊒ False All goals completed! πŸ™def axisMultiplier (u : ℝ) : β„‚ := gammaMultiplier ((2 * Real.pi * u : ℝ) * Complex.I)theorem axisMultiplier_norm (u : ℝ) : β€–axisMultiplier uβ€– = 1 := gammaMultiplier_norm_imaginary _theorem axisMultiplier_continuous : Continuous axisMultiplier := ⊒ Continuous axisMultiplier h1:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)⊒ Continuous axisMultiplier h1:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h2:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)⊒ Continuous axisMultiplier h1:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h2:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h3:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))⊒ Continuous axisMultiplier h1:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h2:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h3:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))h4:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))⊒ Continuous axisMultiplier h1:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h2:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h3:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))h4:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))hd:Continuous (((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u)) * (fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))⊒ Continuous axisMultiplier h1:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h2:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h3:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))h4:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))hd:Continuous (((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u)) * (fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))hne:βˆ€ (u : ℝ), Complex.Gamma (↑(7 / 6) + ↑(-(2 * Ο€ * u)) * I) * Complex.Gamma (↑(5 / 6) + ↑(-(2 * Ο€ * u)) * I) β‰  0⊒ Continuous axisMultiplier h1:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h2:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h3:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))h4:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))hd:Continuous (((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u)) * (fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))hne:βˆ€ (u : ℝ), Complex.Gamma (↑(7 / 6) + ↑(-(2 * Ο€ * u)) * I) * Complex.Gamma (↑(5 / 6) + ↑(-(2 * Ο€ * u)) * I) β‰  0⊒ axisMultiplier = (((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u) * (fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u) / (((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u)) * (fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u)) h1:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h2:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u)h3:Continuous ((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))h4:Continuous ((fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))hd:Continuous (((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u)) * (fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))hne:βˆ€ (u : ℝ), Complex.Gamma (↑(7 / 6) + ↑(-(2 * Ο€ * u)) * I) * Complex.Gamma (↑(5 / 6) + ↑(-(2 * Ο€ * u)) * I) β‰  0u:β„βŠ’ axisMultiplier u = ((((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u) * (fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => 2 * Ο€ * u) / (((fun u => Complex.Gamma (↑(7 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u)) * (fun u => Complex.Gamma (↑(5 / 6) + ↑u * I)) ∘ fun u => -(2 * Ο€ * u))) u All goals completed! πŸ™def spectralProfile (logSource : SchwartzMap ℝ β„‚) (u : ℝ) : β„‚ := axisMultiplier u * (𝓕 logSource) utheorem spectralProfile_norm (logSource : SchwartzMap ℝ β„‚) (u : ℝ) : β€–spectralProfile logSource uβ€– = β€–(𝓕 logSource) uβ€– := logSource:𝓒(ℝ, β„‚)u:β„βŠ’ β€–spectralProfile logSource uβ€– = β€–(𝓕 logSource) uβ€– All goals completed! πŸ™theorem spectralProfile_continuous (logSource : SchwartzMap ℝ β„‚) : Continuous (spectralProfile logSource) := axisMultiplier_continuous.mul (𝓕 logSource).continuoustheorem spectralProfile_moment_integrable (logSource : SchwartzMap ℝ β„‚) (j : β„•) : Integrable (fun u : ℝ => β€–uβ€– ^ j * β€–spectralProfile logSource uβ€–) := logSource:𝓒(ℝ, β„‚)j:β„•βŠ’ Integrable (fun u => β€–uβ€– ^ j * β€–spectralProfile logSource uβ€–) volume All goals completed! πŸ™theorem spectralProfile_pow_integrable (logSource : SchwartzMap ℝ β„‚) (j : β„•) : Integrable (fun u : ℝ => u ^ j β€’ spectralProfile logSource u) := logSource:𝓒(ℝ, β„‚)j:β„•βŠ’ Integrable (fun u => u ^ j β€’ spectralProfile logSource u) volume apply (spectralProfile_moment_integrable logSource j).mono' ((show Continuous (fun u : ℝ => u ^ j β€’ spectralProfile logSource u) logSource:𝓒(ℝ, β„‚)j:β„•βŠ’ Integrable (fun u => u ^ j β€’ spectralProfile logSource u) volume All goals completed! πŸ™).aestronglyMeasurable) exact Filter.Eventually.of_forall (fun u => logSource:𝓒(ℝ, β„‚)j:β„•u:β„βŠ’ β€–u ^ j β€’ spectralProfile logSource uβ€– ≀ β€–uβ€– ^ j * β€–spectralProfile logSource uβ€– All goals completed! πŸ™)def reflectedLogProfile (logSource : SchwartzMap ℝ β„‚) : ℝ β†’ β„‚ := 𝓕 (spectralProfile logSource)theorem reflectedLogProfile_smooth (logSource : SchwartzMap ℝ β„‚) : ContDiff ℝ ∞ (reflectedLogProfile logSource) := Real.contDiff_fourier (fun j _ => spectralProfile_moment_integrable logSource j)theorem reflectedLogProfile_deriv (logSource : SchwartzMap ℝ β„‚) (j : β„•) : iteratedDeriv j (reflectedLogProfile logSource) = 𝓕 (fun u : ℝ => (-2 * Real.pi * Complex.I * u) ^ j * spectralProfile logSource u) := logSource:𝓒(ℝ, β„‚)j:β„•βŠ’ iteratedDeriv j (reflectedLogProfile logSource) = 𝓕 fun u => (-2 * ↑π * I * ↑u) ^ j * spectralProfile logSource u simpa only [reflectedLogProfile, smul_eq_mul] using (Real.iteratedDeriv_fourier (N := (⊀ : β„•βˆž)) (fun n _ => spectralProfile_pow_integrable logSource n) (logSource:𝓒(ℝ, β„‚)j:β„•βŠ’ ↑j ≀ ⊀ All goals completed! πŸ™ : (j : β„•βˆž) ≀ ⊀))end CubicReflectionKernelendend OAI