import OAI.NumberTheory.DirichletL.CubicSieve.CrossFactorizationnamespace 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 Classicalnamespace CoprimeBilinearSieveopen FiniteSieveOperator CoprimeSieveOperator CoprimeMobiusExtensiontheorem disjoint_bilinear_expansion {ι n p : Type*} [DecidableEq ι] [Fintype n] [Fintype p] (B : Finset ι) (left : n → Finset ι) (right : p → Finset ι) (hl : ∀ j, left j ⊆ B) (hr : ∀ k, right k ⊆ B) (z : n → ℂ) (v : p → ℂ) : (∑ j, ∑ k, if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1 : ℂ) ^ D.card * (star (∑ j, if D ⊆ left j then z j else 0) * (∑ k, if D ⊆ right k then v k else 0)) := ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂ⊢ (∑ j, ∑ k, if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (∑ j, if D ⊆ left j then z j else 0) * ∑ k, if D ⊆ right k then v k else 0) ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0⊢ (∑ j, ∑ k, if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (∑ j, if D ⊆ left j then z j else 0) * ∑ k, if D ⊆ right k then v k else 0) simp_rw ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0⊢ (∑ j, ∑ k, if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (∑ j, if D ⊆ left j then z j else 0) * ∑ k, if D ⊆ right k then v k else 0)ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0⊢ (∑ x, ∑ x_1, ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left x ∧ D ⊆ right x_1 then star (z x) * v x_1 else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (∑ j, if D ⊆ left j then z j else 0) * ∑ k, if D ⊆ right k then v k else 0)] calc _ = ∑ j, ∑ D ∈ B.powerset, ∑ k, (-1 : ℂ) ^ D.card * (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) := ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0⊢ (∑ x, ∑ x_1, ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left x ∧ D ⊆ right x_1 then star (z x) * v x_1 else 0) = ∑ j, ∑ D ∈ B.powerset, ∑ k, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0⊢ ∀ x ∈ Finset.univ, (∑ x_1, ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left x ∧ D ⊆ right x_1 then star (z x) * v x_1 else 0) = ∑ D ∈ B.powerset, ∑ k, (-1) ^ #D * if D ⊆ left x ∧ D ⊆ right k then star (z x) * v k else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0j:na✝:j ∈ Finset.univ⊢ (∑ x, ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right x then star (z j) * v x else 0) = ∑ D ∈ B.powerset, ∑ k, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0 All goals completed! 🐙 _ = ∑ D ∈ B.powerset, ∑ j, ∑ k, (-1 : ℂ) ^ D.card * (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) := Finset.sum_comm _ = _ := ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0⊢ (∑ D ∈ B.powerset, ∑ j, ∑ k, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (∑ j, if D ⊆ left j then z j else 0) * ∑ k, if D ⊆ right k then v k else 0) ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0⊢ ∀ x ∈ B.powerset, (∑ j, ∑ k, (-1) ^ #x * if x ⊆ left j ∧ x ⊆ right k then star (z j) * v k else 0) = (-1) ^ #x * (star (∑ j, if x ⊆ left j then z j else 0) * ∑ k, if x ⊆ right k then v k else 0) ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝:D ∈ B.powerset⊢ (∑ j, ∑ k, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = (-1) ^ #D * (star (∑ j, if D ⊆ left j then z j else 0) * ∑ k, if D ⊆ right k then v k else 0) simp_rw ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝:D ∈ B.powerset⊢ (∑ j, ∑ k, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = (-1) ^ #D * (star (∑ j, if D ⊆ left j then z j else 0) * ∑ k, if D ⊆ right k then v k else 0)ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝:D ∈ B.powerset⊢ ((-1) ^ #D * ∑ i, ∑ i_1, if D ⊆ left i ∧ D ⊆ right i_1 then star (z i) * v i_1 else 0) = (-1) ^ #D * (star (∑ j, if D ⊆ left j then z j else 0) * ∑ k, if D ⊆ right k then v k else 0)] ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝:D ∈ B.powerset⊢ (∑ i, ∑ i_1, if D ⊆ left i ∧ D ⊆ right i_1 then star (z i) * v i_1 else 0) = star (∑ j, if D ⊆ left j then z j else 0) * ∑ k, if D ⊆ right k then v k else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝:D ∈ B.powerset⊢ (∑ i, ∑ i_1, if D ⊆ left i ∧ D ⊆ right i_1 then star (z i) * v i_1 else 0) = ∑ i, ∑ j, star (if D ⊆ left i then z i else 0) * if D ⊆ right j then v j else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝:D ∈ B.powerset⊢ ∀ x ∈ Finset.univ, (∑ i, if D ⊆ left x ∧ D ⊆ right i then star (z x) * v i else 0) = ∑ j, star (if D ⊆ left x then z x else 0) * if D ⊆ right j then v j else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝¹:D ∈ B.powersetj:na✝:j ∈ Finset.univ⊢ (∑ i, if D ⊆ left j ∧ D ⊆ right i then star (z j) * v i else 0) = ∑ j_1, star (if D ⊆ left j then z j else 0) * if D ⊆ right j_1 then v j_1 else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝¹:D ∈ B.powersetj:na✝:j ∈ Finset.univ⊢ ∀ x ∈ Finset.univ, (if D ⊆ left j ∧ D ⊆ right x then star (z j) * v x else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right x then v x else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univ⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:D ⊆ left j⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:¬D ⊆ left j⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:D ⊆ left j⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:¬D ⊆ left j⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:¬D ⊆ left jhk:D ⊆ right k⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:¬D ⊆ left jhk:¬D ⊆ right k⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0 ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:D ⊆ left jhk:D ⊆ right k⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:D ⊆ left jhk:¬D ⊆ right k⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:¬D ⊆ left jhk:D ⊆ right k⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0ι:Type u_1n:Type u_2p:Type u_3inst✝²:DecidableEq ιinst✝¹:Fintype ninst✝:Fintype pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ Bz:n → ℂv:p → ℂhp:∀ (j : n) (k : p), (if Disjoint (left j) (right k) then star (z j) * v k else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0D:Finset ιa✝²:D ∈ B.powersetj:na✝¹:j ∈ Finset.univk:pa✝:k ∈ Finset.univhj:¬D ⊆ left jhk:¬D ⊆ right k⊢ (if D ⊆ left j ∧ D ⊆ right k then star (z j) * v k else 0) = star (if D ⊆ left j then z j else 0) * if D ⊆ right k then v k else 0 All goals completed! 🐙theorem coprime_bilinear_operator_bound {ι m n p : Type*} [DecidableEq ι] [Fintype m] [Fintype n] [Fintype p] [DecidableEq m] [DecidableEq n] [DecidableEq p] (B : Finset ι) (left : n → Finset ι) (right : p → Finset ι) (hl : ∀ j, left j ⊆ B) (hr : ∀ k, right k ⊆ B) (A : Matrix m n ℂ) (C : Matrix m p ℂ) (a : n → ℂ) (b : p → ℂ) : (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, (2 : ℝ) ^ (left j).card * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, (2 : ℝ) ^ (right k).card * ‖b k‖ ^ 2) := ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂ⊢ (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2) ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0⊢ (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2) ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0Y:Finset ι → m → ℂ := fun D i => ∑ k, C i k * if D ⊆ right k then b k else 0⊢ (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2) ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0Y:Finset ι → m → ℂ := fun D i => ∑ k, C i k * if D ⊆ right k then b k else 0heq:∀ (i : m), (∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (X D i) * Y D i)⊢ (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2) ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0Y:Finset ι → m → ℂ := fun D i => ∑ k, C i k * if D ⊆ right k then b k else 0heq:∀ (i : m), (∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (X D i) * Y D i)hnorm:∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖ ≤ ∑ D ∈ B.powerset, ∑ i, ‖X D i‖ * ‖Y D i‖⊢ (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2) ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0Y:Finset ι → m → ℂ := fun D i => ∑ k, C i k * if D ⊆ right k then b k else 0heq:∀ (i : m), (∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (X D i) * Y D i)hnorm:∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖ ≤ ∑ D ∈ B.powerset, ∑ i, ‖X D i‖ * ‖Y D i‖hCS:(∑ i ∈ B.powerset ×ˢ Finset.univ, ‖X i.1 i.2‖ * ‖Y i.1 i.2‖) ^ 2 ≤ (∑ i ∈ B.powerset ×ˢ Finset.univ, ‖X i.1 i.2‖ ^ 2) * ∑ i ∈ B.powerset ×ˢ Finset.univ, ‖Y i.1 i.2‖ ^ 2⊢ (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2) ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0Y:Finset ι → m → ℂ := fun D i => ∑ k, C i k * if D ⊆ right k then b k else 0heq:∀ (i : m), (∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (X D i) * Y D i)hnorm:∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖ ≤ ∑ D ∈ B.powerset, ∑ i, ‖X D i‖ * ‖Y D i‖hCS:(∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ * ‖Y x x_1‖) ^ 2 ≤ (∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ ^ 2) * ∑ x ∈ B.powerset, ∑ x_1, ‖Y x x_1‖ ^ 2⊢ (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2) ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0Y:Finset ι → m → ℂ := fun D i => ∑ k, C i k * if D ⊆ right k then b k else 0heq:∀ (i : m), (∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (X D i) * Y D i)hnorm:∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖ ≤ ∑ D ∈ B.powerset, ∑ i, ‖X D i‖ * ‖Y D i‖hCS:(∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ * ‖Y x x_1‖) ^ 2 ≤ (∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ ^ 2) * ∑ x ∈ B.powerset, ∑ x_1, ‖Y x x_1‖ ^ 2hX:∑ D ∈ B.powerset, ∑ i, ‖X D i‖ ^ 2 ≤ ‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2⊢ (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2) ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0Y:Finset ι → m → ℂ := fun D i => ∑ k, C i k * if D ⊆ right k then b k else 0heq:∀ (i : m), (∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (X D i) * Y D i)hnorm:∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖ ≤ ∑ D ∈ B.powerset, ∑ i, ‖X D i‖ * ‖Y D i‖hCS:(∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ * ‖Y x x_1‖) ^ 2 ≤ (∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ ^ 2) * ∑ x ∈ B.powerset, ∑ x_1, ‖Y x x_1‖ ^ 2hX:∑ D ∈ B.powerset, ∑ i, ‖X D i‖ ^ 2 ≤ ‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2hY:∑ D ∈ B.powerset, ∑ i, ‖Y D i‖ ^ 2 ≤ ‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2⊢ (∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2) exact (pow_le_pow_left₀ (Finset.sum_nonneg (fun _ _ => norm_nonneg _)) hnorm 2).trans (hCS.trans (mul_le_mul hX hY (ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0Y:Finset ι → m → ℂ := fun D i => ∑ k, C i k * if D ⊆ right k then b k else 0heq:∀ (i : m), (∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (X D i) * Y D i)hnorm:∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖ ≤ ∑ D ∈ B.powerset, ∑ i, ‖X D i‖ * ‖Y D i‖hCS:(∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ * ‖Y x x_1‖) ^ 2 ≤ (∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ ^ 2) * ∑ x ∈ B.powerset, ∑ x_1, ‖Y x x_1‖ ^ 2hX:∑ D ∈ B.powerset, ∑ i, ‖X D i‖ ^ 2 ≤ ‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2hY:∑ D ∈ B.powerset, ∑ i, ‖Y D i‖ ^ 2 ≤ ‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2⊢ 0 ≤ ∑ x ∈ B.powerset, ∑ x_1, ‖Y x x_1‖ ^ 2 All goals completed! 🐙) (ι:Type u_1m:Type u_2n:Type u_3p:Type u_4inst✝⁶:DecidableEq ιinst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pB:Finset ιleft:n → Finset ιright:p → Finset ιhl:∀ (j : n), left j ⊆ Bhr:∀ (k : p), right k ⊆ BA:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂX:Finset ι → m → ℂ := fun D i => ∑ j, A i j * if D ⊆ left j then a j else 0Y:Finset ι → m → ℂ := fun D i => ∑ k, C i k * if D ⊆ right k then b k else 0heq:∀ (i : m), (∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0) = ∑ D ∈ B.powerset, (-1) ^ #D * (star (X D i) * Y D i)hnorm:∑ i, ‖∑ j, ∑ k, if Disjoint (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖ ≤ ∑ D ∈ B.powerset, ∑ i, ‖X D i‖ * ‖Y D i‖hCS:(∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ * ‖Y x x_1‖) ^ 2 ≤ (∑ x ∈ B.powerset, ∑ x_1, ‖X x x_1‖ ^ 2) * ∑ x ∈ B.powerset, ∑ x_1, ‖Y x x_1‖ ^ 2hX:∑ D ∈ B.powerset, ∑ i, ‖X D i‖ ^ 2 ≤ ‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2hY:∑ D ∈ B.powerset, ∑ i, ‖Y D i‖ ^ 2 ≤ ‖operator C‖ ^ 2 * ∑ k, 2 ^ #(right k) * ‖b k‖ ^ 2⊢ 0 ≤ ‖operator A‖ ^ 2 * ∑ j, 2 ^ #(left j) * ‖a j‖ ^ 2 All goals completed! 🐙)))end CoprimeBilinearSievenamespace IdealCoprimeBilinearSieveabbrev O := ActualEisensteinCubic.Oopen IdealMobiusDivisorSum IdealCoprimeSieveOperator FiniteSieveOperatortheorem support_weighted_energy_bound {n : Type*} [Fintype n] (ε : ℝ) (hε : 0 < ε) (column : n → Ideal O) (hcol : ∀ j, column j ≠ 0) (N : ℝ) (hnorm : ∀ j, (Ideal.absNorm (column j) : ℝ) ≤ N) (a : n → ℂ) : (∑ j, (2 : ℝ) ^ (primeSupport (column j)).card * ‖a j‖ ^ 2) ≤ (supportConstant ε hε * N ^ ε) * ∑ j, ‖a j‖ ^ 2 := n:Type u_1inst✝:Fintype nε:ℝhε:0 < εcolumn:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂ⊢ ∑ j, 2 ^ #(primeSupport (column j)) * ‖a j‖ ^ 2 ≤ supportConstant ε hε * N ^ ε * ∑ j, ‖a j‖ ^ 2 n:Type u_1inst✝:Fintype nε:ℝhε:0 < εcolumn:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂ⊢ ∑ j, 2 ^ #(primeSupport (column j)) * ‖a j‖ ^ 2 ≤ ∑ i, supportConstant ε hε * N ^ ε * ‖a i‖ ^ 2 n:Type u_1inst✝:Fintype nε:ℝhε:0 < εcolumn:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂ⊢ ∀ i ∈ Finset.univ, 2 ^ #(primeSupport (column i)) * ‖a i‖ ^ 2 ≤ supportConstant ε hε * N ^ ε * ‖a i‖ ^ 2 n:Type u_1inst✝:Fintype nε:ℝhε:0 < εcolumn:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂj:na✝:j ∈ Finset.univ⊢ 2 ^ #(primeSupport (column j)) * ‖a j‖ ^ 2 ≤ supportConstant ε hε * N ^ ε * ‖a j‖ ^ 2 n:Type u_1inst✝:Fintype nε:ℝhε:0 < εcolumn:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂj:na✝:j ∈ Finset.univ⊢ 2 ^ #(primeSupport (column j)) ≤ supportConstant ε hε * N ^ ε All goals completed! 🐙theorem ideal_coprime_bilinear_operator_bound {m n p : Type*} [Fintype m] [Fintype n] [Fintype p] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ε : ℝ) (hε : 0 < ε) (left : n → Ideal O) (right : p → Ideal O) (hl0 : ∀ j, left j ≠ 0) (hr0 : ∀ k, right k ≠ 0) (N₁ N₂ : ℝ) (hN₁ : 0 ≤ N₁) (_hN₂ : 0 ≤ N₂) (hlN : ∀ j, (Ideal.absNorm (left j) : ℝ) ≤ N₁) (hrN : ∀ k, (Ideal.absNorm (right k) : ℝ) ≤ N₂) (A : Matrix m n ℂ) (C : Matrix m p ℂ) (a : n → ℂ) (b : p → ℂ) : (∑ i, ‖∑ j, ∑ k, if IsCoprime (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2) := m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂ⊢ (∑ i, ‖∑ j, ∑ k, if IsCoprime (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)⊢ (∑ i, ‖∑ j, ∑ k, if IsCoprime (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ B⊢ (∑ i, ‖∑ j, ∑ k, if IsCoprime (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ B⊢ (∑ i, ‖∑ j, ∑ k, if IsCoprime (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ i, ‖∑ j, ∑ k, if Disjoint (primeSupport (left j)) (primeSupport (right k)) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ (∑ i, ‖∑ j, ∑ k, if IsCoprime (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2) simp_rw m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ i, ‖∑ j, ∑ k, if Disjoint (primeSupport (left j)) (primeSupport (right k)) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ (∑ i, ‖∑ j, ∑ k, if IsCoprime (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2)m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ (∑ i, ‖∑ j, ∑ k, if IsCoprime (left j) (right k) then star (A i j * a j) * (C i k * b k) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2)] at h m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2) ≤ (‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ ‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2 ≤ ‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ ‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2 ≤ ‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ 0 ≤ ‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ 0 ≤ ‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2 m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ ‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2 ≤ ‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2 All goals completed! 🐙 m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ ‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2 ≤ ‖operator C‖ ^ 2 * (supportConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2 All goals completed! 🐙 m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ 0 ≤ ‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2 All goals completed! 🐙 m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)⊢ 0 ≤ ‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2 m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εleft:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁_hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Matrix m n ℂC:Matrix m p ℂa:n → ℂb:p → ℂB:Finset (Ideal O) := (Finset.univ.biUnion fun j => primeSupport (left j)) ∪ Finset.univ.biUnion fun k => primeSupport (right k)hl:∀ (j : n), primeSupport (left j) ⊆ Bhr:∀ (k : p), primeSupport (right k) ⊆ Bh:(∑ x, ‖∑ x_1, ∑ x_2, if IsCoprime (left x_1) (right x_2) then star (A x x_1 * a x_1) * (C x x_2 * b x_2) else 0‖) ^ 2 ≤ (‖operator A‖ ^ 2 * ∑ j, 2 ^ #(primeSupport (left j)) * ‖a j‖ ^ 2) * (‖operator C‖ ^ 2 * ∑ k, 2 ^ #(primeSupport (right k)) * ‖b k‖ ^ 2)hpos:0 ≤ supportConstant ε hε⊢ 0 ≤ ‖operator A‖ ^ 2 * (supportConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2 All goals completed! 🐙end IdealCoprimeBilinearSievenamespace DivisorBlockCauchyabbrev O := ActualEisensteinCubic.Oopen IdealMobiusDivisorSum FiniteSieveOperator IdealCoprimeSieveOperatortheorem divisor_mask_energy {n : Type*} [Fintype n] (S : Finset (Ideal O)) (column : n → Ideal O) (hcol : ∀ j, column j ≠ 0) (a : n → ℂ) : (∑ D ∈ S, ∑ j, ‖if D ∣ column j then a j else 0‖ ^ 2) ≤ ∑ j, ((idealDivisors (column j)).card : ℝ) * ‖a j‖ ^ 2 := n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂ⊢ ∑ D ∈ S, ∑ j, ‖if D ∣ column j then a j else 0‖ ^ 2 ≤ ∑ j, ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2 n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂ⊢ ∑ y, ∑ x ∈ S, ‖if x ∣ column y then a y else 0‖ ^ 2 ≤ ∑ j, ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2 n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂ⊢ ∀ i ∈ Finset.univ, ∑ x ∈ S, ‖if x ∣ column i then a i else 0‖ ^ 2 ≤ ↑(#(idealDivisors (column i))) * ‖a i‖ ^ 2 n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂj:na✝:j ∈ Finset.univ⊢ ∑ x ∈ S, ‖if x ∣ column j then a j else 0‖ ^ 2 ≤ ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2 n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂj:na✝:j ∈ Finset.univhsub:{D ∈ S | D ∣ column j} ⊆ idealDivisors (column j)⊢ ∑ x ∈ S, ‖if x ∣ column j then a j else 0‖ ^ 2 ≤ ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2 n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂj:na✝:j ∈ Finset.univhsub:{D ∈ S | D ∣ column j} ⊆ idealDivisors (column j)hite:∀ (D : Ideal O), ‖if D ∣ column j then a j else 0‖ ^ 2 = if D ∣ column j then ‖a j‖ ^ 2 else 0⊢ ∑ x ∈ S, ‖if x ∣ column j then a j else 0‖ ^ 2 ≤ ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2 simp_rw n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂj:na✝:j ∈ Finset.univhsub:{D ∈ S | D ∣ column j} ⊆ idealDivisors (column j)hite:∀ (D : Ideal O), ‖if D ∣ column j then a j else 0‖ ^ 2 = if D ∣ column j then ‖a j‖ ^ 2 else 0⊢ ∑ x ∈ S, ‖if x ∣ column j then a j else 0‖ ^ 2 ≤ ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂj:na✝:j ∈ Finset.univhsub:{D ∈ S | D ∣ column j} ⊆ idealDivisors (column j)hite:∀ (D : Ideal O), ‖if D ∣ column j then a j else 0‖ ^ 2 = if D ∣ column j then ‖a j‖ ^ 2 else 0⊢ (∑ x ∈ S, if x ∣ column j then ‖a j‖ ^ 2 else 0) ≤ ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2] n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂj:na✝:j ∈ Finset.univhsub:{D ∈ S | D ∣ column j} ⊆ idealDivisors (column j)hite:∀ (D : Ideal O), ‖if D ∣ column j then a j else 0‖ ^ 2 = if D ∣ column j then ‖a j‖ ^ 2 else 0⊢ ↑(#({a ∈ S | a ∣ column j})) * ‖a j‖ ^ 2 ≤ ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2 exact mul_le_mul_of_nonneg_right (n:Type u_1inst✝:Fintype nS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0a:n → ℂj:na✝:j ∈ Finset.univhsub:{D ∈ S | D ∣ column j} ⊆ idealDivisors (column j)hite:∀ (D : Ideal O), ‖if D ∣ column j then a j else 0‖ ^ 2 = if D ∣ column j then ‖a j‖ ^ 2 else 0⊢ ↑(#({a ∈ S | a ∣ column j})) ≤ ↑(#(idealDivisors (column j))) All goals completed! 🐙) (sq_nonneg _)def divisorConstant (ε : ℝ) (hε : 0 < ε) : ℝ := (IdealDivisorBound.ideal_divisor_small_power ε hε).choosetheorem divisorConstant_pos (ε : ℝ) (hε : 0 < ε) : 0 < divisorConstant ε hε := (IdealDivisorBound.ideal_divisor_small_power ε hε).choose_spec.1theorem divisor_mask_energy_small_power {n : Type*} [Fintype n] (ε : ℝ) (hε : 0 < ε) (S : Finset (Ideal O)) (column : n → Ideal O) (hcol : ∀ j, column j ≠ 0) (N : ℝ) (hnorm : ∀ j, (Ideal.absNorm (column j) : ℝ) ≤ N) (a : n → ℂ) : (∑ D ∈ S, ∑ j, ‖if D ∣ column j then a j else 0‖ ^ 2) ≤ (divisorConstant ε hε * N ^ ε) * ∑ j, ‖a j‖ ^ 2 := n:Type u_1inst✝:Fintype nε:ℝhε:0 < εS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂ⊢ ∑ D ∈ S, ∑ j, ‖if D ∣ column j then a j else 0‖ ^ 2 ≤ divisorConstant ε hε * N ^ ε * ∑ j, ‖a j‖ ^ 2 n:Type u_1inst✝:Fintype nε:ℝhε:0 < εS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂ⊢ ∑ j, ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2 ≤ divisorConstant ε hε * N ^ ε * ∑ j, ‖a j‖ ^ 2 n:Type u_1inst✝:Fintype nε:ℝhε:0 < εS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂ⊢ ∑ j, ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2 ≤ ∑ i, divisorConstant ε hε * N ^ ε * ‖a i‖ ^ 2 n:Type u_1inst✝:Fintype nε:ℝhε:0 < εS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂ⊢ ∀ i ∈ Finset.univ, ↑(#(idealDivisors (column i))) * ‖a i‖ ^ 2 ≤ divisorConstant ε hε * N ^ ε * ‖a i‖ ^ 2 n:Type u_1inst✝:Fintype nε:ℝhε:0 < εS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂj:na✝:j ∈ Finset.univ⊢ ↑(#(idealDivisors (column j))) * ‖a j‖ ^ 2 ≤ divisorConstant ε hε * N ^ ε * ‖a j‖ ^ 2 n:Type u_1inst✝:Fintype nε:ℝhε:0 < εS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂj:na✝:j ∈ Finset.univ⊢ ↑(#(idealDivisors (column j))) ≤ divisorConstant ε hε * N ^ ε n:Type u_1inst✝:Fintype nε:ℝhε:0 < εS:Finset (Ideal O)column:n → Ideal Ohcol:∀ (j : n), column j ≠ 0N:ℝhnorm:∀ (j : n), ↑(absNorm (column j)) ≤ Na:n → ℂj:na✝:j ∈ Finset.univ⊢ ⋯.choose * ↑(absNorm (column j)) ^ ε ≤ divisorConstant ε hε * N ^ ε All goals completed! 🐙theorem rectangular_cauchy {α β : Type*} (S : Finset α) (T : Finset β) (H : α → β → ℝ) (E : α → ℝ) (F : β → ℝ) (C : ℝ) (_hC : 0 ≤ C) (hH : ∀ d ∈ S, ∀ e ∈ T, (H d e) ^ 2 ≤ C * E d * F e) : (∑ d ∈ S, ∑ e ∈ T, H d e) ^ 2 ≤ (S.card : ℝ) * T.card * C * (∑ d ∈ S, E d) * (∑ e ∈ T, F e) := α:Type u_1β:Type u_2S:Finset αT:Finset βH:α → β → ℝE:α → ℝF:β → ℝC:ℝ_hC:0 ≤ ChH:∀ d ∈ S, ∀ e ∈ T, H d e ^ 2 ≤ C * E d * F e⊢ (∑ d ∈ S, ∑ e ∈ T, H d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, E d) * ∑ e ∈ T, F e classical α:Type u_1β:Type u_2S:Finset αT:Finset βH:α → β → ℝE:α → ℝF:β → ℝC:ℝ_hC:0 ≤ ChH:∀ d ∈ S, ∀ e ∈ T, H d e ^ 2 ≤ C * E d * F ehCS:(∑ i ∈ S ×ˢ T, 1 * H i.1 i.2) ^ 2 ≤ (∑ i ∈ S ×ˢ T, 1 ^ 2) * ∑ i ∈ S ×ˢ T, H i.1 i.2 ^ 2⊢ (∑ d ∈ S, ∑ e ∈ T, H d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, E d) * ∑ e ∈ T, F e α:Type u_1β:Type u_2S:Finset αT:Finset βH:α → β → ℝE:α → ℝF:β → ℝC:ℝ_hC:0 ≤ ChH:∀ d ∈ S, ∀ e ∈ T, H d e ^ 2 ≤ C * E d * F ehCS:(∑ x ∈ S, ∑ x_1 ∈ T, H x x_1) ^ 2 ≤ ↑(#S) * ↑(#T) * ∑ x ∈ S, ∑ x_1 ∈ T, H x x_1 ^ 2⊢ (∑ d ∈ S, ∑ e ∈ T, H d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, E d) * ∑ e ∈ T, F e α:Type u_1β:Type u_2S:Finset αT:Finset βH:α → β → ℝE:α → ℝF:β → ℝC:ℝ_hC:0 ≤ ChH:∀ d ∈ S, ∀ e ∈ T, H d e ^ 2 ≤ C * E d * F ehCS:(∑ x ∈ S, ∑ x_1 ∈ T, H x x_1) ^ 2 ≤ ↑(#S) * ↑(#T) * ∑ x ∈ S, ∑ x_1 ∈ T, H x x_1 ^ 2hsum:∑ d ∈ S, ∑ e ∈ T, H d e ^ 2 ≤ (C * ∑ d ∈ S, E d) * ∑ e ∈ T, F e⊢ (∑ d ∈ S, ∑ e ∈ T, H d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, E d) * ∑ e ∈ T, F e α:Type u_1β:Type u_2S:Finset αT:Finset βH:α → β → ℝE:α → ℝF:β → ℝC:ℝ_hC:0 ≤ ChH:∀ d ∈ S, ∀ e ∈ T, H d e ^ 2 ≤ C * E d * F ehCS:(∑ x ∈ S, ∑ x_1 ∈ T, H x x_1) ^ 2 ≤ ↑(#S) * ↑(#T) * ∑ x ∈ S, ∑ x_1 ∈ T, H x x_1 ^ 2hsum:∑ d ∈ S, ∑ e ∈ T, H d e ^ 2 ≤ (C * ∑ d ∈ S, E d) * ∑ e ∈ T, F e⊢ ↑(#S) * ↑(#T) * ∑ x ∈ S, ∑ x_1 ∈ T, H x x_1 ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, E d) * ∑ e ∈ T, F e simpa only [mul_assoc] using mul_le_mul_of_nonneg_left hsum (show (0 : ℝ) ≤ (S.card : ℝ) * T.card α:Type u_1β:Type u_2S:Finset αT:Finset βH:α → β → ℝE:α → ℝF:β → ℝC:ℝ_hC:0 ≤ ChH:∀ d ∈ S, ∀ e ∈ T, H d e ^ 2 ≤ C * E d * F e⊢ (∑ d ∈ S, ∑ e ∈ T, H d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, E d) * ∑ e ∈ T, F e All goals completed! 🐙)end DivisorBlockCauchynamespace IdealDivisorBilinearBlocksabbrev O := ActualEisensteinCubic.Oopen FiniteSieveOperator IdealCoprimeSieveOperator DivisorBlockCauchydef blockValue {m n p : Type*} [Fintype m] [Fintype n] [Fintype p] (left : n → Ideal O) (right : p → Ideal O) (A : Ideal O → Matrix m n ℂ) (B : Ideal O → Matrix m p ℂ) (a : n → ℂ) (b : p → ℂ) (D E : Ideal O) : ℝ := ∑ i, ‖∑ j, ∑ k, if IsCoprime (left j) (right k) then star (A D i j * (if D ∣ left j then a j else 0)) * (B E i k * (if E ∣ right k then b k else 0)) else 0‖theorem blockValue_nonneg {m n p : Type*} [Fintype m] [Fintype n] [Fintype p] (left : n → Ideal O) (right : p → Ideal O) (A : Ideal O → Matrix m n ℂ) (B : Ideal O → Matrix m p ℂ) (a : n → ℂ) (b : p → ℂ) (D E : Ideal O) : 0 ≤ blockValue left right A B a b D E := Finset.sum_nonneg (fun _ _ => norm_nonneg _)theorem divisor_block_bound {m n p : Type*} [Fintype m] [Fintype n] [Fintype p] [DecidableEq m] [DecidableEq n] [DecidableEq p] (ε : ℝ) (hε : 0 < ε) (S T : Finset (Ideal O)) (left : n → Ideal O) (right : p → Ideal O) (hl0 : ∀ j, left j ≠ 0) (hr0 : ∀ k, right k ≠ 0) (N₁ N₂ : ℝ) (hN₁ : 0 ≤ N₁) (hN₂ : 0 ≤ N₂) (hlN : ∀ j, (Ideal.absNorm (left j) : ℝ) ≤ N₁) (hrN : ∀ k, (Ideal.absNorm (right k) : ℝ) ≤ N₂) (A : Ideal O → Matrix m n ℂ) (B : Ideal O → Matrix m p ℂ) (a : n → ℂ) (b : p → ℂ) (UA UB : ℝ) (hUA : 0 ≤ UA) (hUB : 0 ≤ UB) (hA : ∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UA) (hB : ∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UB) : (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ (S.card : ℝ) * T.card * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * ((divisorConstant ε hε * N₁ ^ ε) * ∑ j, ‖a j‖ ^ 2) * ((divisorConstant ε hε * N₂ ^ ε) * ∑ k, ‖b k‖ ^ 2) := m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UB⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hε⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hε⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ C⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL D⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER E⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER Ehp:∀ D ∈ S, ∀ E ∈ T, blockValue left right A B a b D E ^ 2 ≤ C * EL D * ER E⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER Ehp:∀ D ∈ S, ∀ E ∈ T, blockValue left right A B a b D E ^ 2 ≤ C * EL D * ER Ehc:(∑ d ∈ S, ∑ e ∈ T, blockValue left right A B a b d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, EL d) * ∑ e ∈ T, ER e⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER Ehp:∀ D ∈ S, ∀ E ∈ T, blockValue left right A B a b D E ^ 2 ≤ C * EL D * ER Ehc:(∑ d ∈ S, ∑ e ∈ T, blockValue left right A B a b d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, EL d) * ∑ e ∈ T, ER ehe1:∑ D ∈ S, ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2 ≤ divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER Ehp:∀ D ∈ S, ∀ E ∈ T, blockValue left right A B a b D E ^ 2 ≤ C * EL D * ER Ehc:(∑ d ∈ S, ∑ e ∈ T, blockValue left right A B a b d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, EL d) * ∑ e ∈ T, ER ehe1:∑ D ∈ S, ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2 ≤ divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2he2:∑ D ∈ T, ∑ j, ‖if D ∣ right j then b j else 0‖ ^ 2 ≤ divisorConstant ε hε * N₂ ^ ε * ∑ j, ‖b j‖ ^ 2⊢ (∑ D ∈ S, ∑ E ∈ T, blockValue left right A B a b D E) ^ 2 ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER Ehp:∀ D ∈ S, ∀ E ∈ T, blockValue left right A B a b D E ^ 2 ≤ C * EL D * ER Ehc:(∑ d ∈ S, ∑ e ∈ T, blockValue left right A B a b d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, EL d) * ∑ e ∈ T, ER ehe1:∑ D ∈ S, ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2 ≤ divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2he2:∑ D ∈ T, ∑ j, ‖if D ∣ right j then b j else 0‖ ^ 2 ≤ divisorConstant ε hε * N₂ ^ ε * ∑ j, ‖b j‖ ^ 2⊢ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, EL d) * ∑ e ∈ T, ER e ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER Ehp:∀ D ∈ S, ∀ E ∈ T, blockValue left right A B a b D E ^ 2 ≤ C * EL D * ER Ehc:(∑ d ∈ S, ∑ e ∈ T, blockValue left right A B a b d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, EL d) * ∑ e ∈ T, ER ehe1:∑ D ∈ S, ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2 ≤ divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2he2:∑ D ∈ T, ∑ j, ‖if D ∣ right j then b j else 0‖ ^ 2 ≤ divisorConstant ε hε * N₂ ^ ε * ∑ j, ‖b j‖ ^ 2⊢ (↑(#S) * ↑(#T) * C * ∑ D ∈ S, EL D) * ∑ E ∈ T, ER E ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER Ehp:∀ D ∈ S, ∀ E ∈ T, blockValue left right A B a b D E ^ 2 ≤ C * EL D * ER Ehc:(∑ d ∈ S, ∑ e ∈ T, blockValue left right A B a b d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, EL d) * ∑ e ∈ T, ER ehe2:∑ D ∈ T, ∑ j, ‖if D ∣ right j then b j else 0‖ ^ 2 ≤ divisorConstant ε hε * N₂ ^ ε * ∑ j, ‖b j‖ ^ 2he1:∑ D ∈ S, EL D ≤ divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2⊢ (↑(#S) * ↑(#T) * C * ∑ D ∈ S, EL D) * ∑ E ∈ T, ER E ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER Ehp:∀ D ∈ S, ∀ E ∈ T, blockValue left right A B a b D E ^ 2 ≤ C * EL D * ER Ehc:(∑ d ∈ S, ∑ e ∈ T, blockValue left right A B a b d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, EL d) * ∑ e ∈ T, ER ehe1:∑ D ∈ S, EL D ≤ divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2he2:∑ E ∈ T, ER E ≤ divisorConstant ε hε * N₂ ^ ε * ∑ j, ‖b j‖ ^ 2⊢ (↑(#S) * ↑(#T) * C * ∑ D ∈ S, EL D) * ∑ E ∈ T, ER E ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) m:Type u_1n:Type u_2p:Type u_3inst✝⁵:Fintype minst✝⁴:Fintype ninst✝³:Fintype pinst✝²:DecidableEq minst✝¹:DecidableEq ninst✝:DecidableEq pε:ℝhε:0 < εS:Finset (Ideal O)T:Finset (Ideal O)left:n → Ideal Oright:p → Ideal Ohl0:∀ (j : n), left j ≠ 0hr0:∀ (k : p), right k ≠ 0N₁:ℝN₂:ℝhN₁:0 ≤ N₁hN₂:0 ≤ N₂hlN:∀ (j : n), ↑(absNorm (left j)) ≤ N₁hrN:∀ (k : p), ↑(absNorm (right k)) ≤ N₂A:Ideal O → Matrix m n ℂB:Ideal O → Matrix m p ℂa:n → ℂb:p → ℂUA:ℝUB:ℝhUA:0 ≤ UAhUB:0 ≤ UBhA:∀ D ∈ S, ‖operator (A D)‖ ^ 2 ≤ UAhB:∀ E ∈ T, ‖operator (B E)‖ ^ 2 ≤ UBEL:Ideal O → ℝ := fun D => ∑ j, ‖if D ∣ left j then a j else 0‖ ^ 2ER:Ideal O → ℝ := fun E => ∑ k, ‖if E ∣ right k then b k else 0‖ ^ 2C:ℝ := UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)hs:0 ≤ supportConstant ε hεhd:0 ≤ divisorConstant ε hεhC:0 ≤ ChEL:∀ (D : Ideal O), 0 ≤ EL DhER:∀ (E : Ideal O), 0 ≤ ER Ehp:∀ D ∈ S, ∀ E ∈ T, blockValue left right A B a b D E ^ 2 ≤ C * EL D * ER Ehc:(∑ d ∈ S, ∑ e ∈ T, blockValue left right A B a b d e) ^ 2 ≤ (↑(#S) * ↑(#T) * C * ∑ d ∈ S, EL d) * ∑ e ∈ T, ER ehe1:∑ D ∈ S, EL D ≤ divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2he2:∑ E ∈ T, ER E ≤ divisorConstant ε hε * N₂ ^ ε * ∑ j, ‖b j‖ ^ 2⊢ (↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * ∑ D ∈ S, EL D) * ∑ E ∈ T, ER E ≤ ↑(#S) * ↑(#T) * (UA * UB * (supportConstant ε hε * N₁ ^ ε) * (supportConstant ε hε * N₂ ^ ε)) * (divisorConstant ε hε * N₁ ^ ε * ∑ j, ‖a j‖ ^ 2) * (divisorConstant ε hε * N₂ ^ ε * ∑ k, ‖b k‖ ^ 2) All goals completed! 🐙end IdealDivisorBilinearBlocksnamespace FiniteSieveRestrictionopen FiniteSieveOperatorvariable {n p : Type*} [Fintype n] [Fintype p] [DecidableEq n] [DecidableEq p]def extendByZero (S : Finset n) (f : n → p) (u : n → ℂ) (k : p) : ℂ := ∑ j ∈ S, if f j = k then u j else 0omit [Fintype n] [Fintype p] [DecidableEq n] in theorem extendByZero_apply_image (S : Finset n) (f : n → p) (u : n → ℂ) (hf : Set.InjOn f S) (j : n) (hj : j ∈ S) : extendByZero S f u (f j) = u j := n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ S⊢ extendByZero S f u (f j) = u j n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ S⊢ (∑ j_1 ∈ S, if f j_1 = f j then u j_1 else 0) = u j n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ S⊢ (if f j = f j then u j else 0) = u jn:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ S⊢ ∀ b ∈ S, b ≠ j → (if f b = f j then u b else 0) = 0n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ S⊢ j ∉ S → (if f j = f j then u j else 0) = 0 n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ S⊢ (if f j = f j then u j else 0) = u j All goals completed! 🐙 n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ S⊢ ∀ b ∈ S, b ≠ j → (if f b = f j then u b else 0) = 0 n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ Sk:nhk:k ∈ Shkj:k ≠ j⊢ (if f k = f j then u k else 0) = 0 All goals completed! 🐙 n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ S⊢ j ∉ S → (if f j = f j then u j else 0) = 0 All goals completed! 🐙omit [Fintype n] [Fintype p] [DecidableEq n] in theorem extendByZero_zero (S : Finset n) (f : n → p) (u : n → ℂ) (k : p) (hk : k ∉ S.image f) : extendByZero S f u k = 0 := n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂk:phk:k ∉ Finset.image f S⊢ extendByZero S f u k = 0 n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂk:phk:k ∉ Finset.image f S⊢ ∀ x ∈ S, (if f x = k then u x else 0) = 0 n:Type u_1p:Type u_2inst✝:DecidableEq pS:Finset nf:n → pu:n → ℂk:phk:k ∉ Finset.image f Sj:nhj:j ∈ S⊢ (if f j = k then u j else 0) = 0 All goals completed! 🐙omit [Fintype n] [DecidableEq n] in theorem extendByZero_energy (S : Finset n) (f : n → p) (u : n → ℂ) (hf : Set.InjOn f S) : (∑ k, ‖extendByZero S f u k‖ ^ 2) = ∑ j ∈ S, ‖u j‖ ^ 2 := n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑S⊢ ∑ k, ‖extendByZero S f u k‖ ^ 2 = ∑ j ∈ S, ‖u j‖ ^ 2 calc _ = ∑ k ∈ S.image f, ‖extendByZero S f u k‖ ^ 2 := n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑S⊢ ∑ k, ‖extendByZero S f u k‖ ^ 2 = ∑ k ∈ Finset.image f S, ‖extendByZero S f u k‖ ^ 2 n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑S⊢ ∑ k ∈ Finset.image f S, ‖extendByZero S f u k‖ ^ 2 = ∑ k, ‖extendByZero S f u k‖ ^ 2 n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑S⊢ ∀ x ∈ Finset.univ, x ∉ Finset.image f S → ‖extendByZero S f u x‖ ^ 2 = 0 n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sk:pa✝:k ∈ Finset.univhk:k ∉ Finset.image f S⊢ ‖extendByZero S f u k‖ ^ 2 = 0 All goals completed! 🐙 _ = ∑ j ∈ S, ‖extendByZero S f u (f j)‖ ^ 2 := n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑S⊢ ∑ k ∈ Finset.image f S, ‖extendByZero S f u k‖ ^ 2 = ∑ j ∈ S, ‖extendByZero S f u (f j)‖ ^ 2 n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑S⊢ InjOn f ↑S All goals completed! 🐙 _ = _ := Finset.sum_congr rfl (fun j hj => n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pS:Finset nf:n → pu:n → ℂhf:InjOn f ↑Sj:nhj:j ∈ S⊢ ‖extendByZero S f u (f j)‖ ^ 2 = ‖u j‖ ^ 2 All goals completed! 🐙)omit [Fintype n] [DecidableEq n] in theorem extendByZero_matrix {m : Type*} (S : Finset n) (f : n → p) (u : n → ℂ) (A : Matrix m p ℂ) (i : m) : (∑ k, A i k * extendByZero S f u k) = ∑ j ∈ S, A i (f j) * u j := n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:m⊢ ∑ k, A i k * extendByZero S f u k = ∑ j ∈ S, A i (f j) * u j n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:m⊢ (∑ k, ∑ i_1 ∈ S, A i k * if f i_1 = k then u i_1 else 0) = ∑ j ∈ S, A i (f j) * u j n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:m⊢ (∑ y ∈ S, ∑ x, A i x * if f y = x then u y else 0) = ∑ j ∈ S, A i (f j) * u j n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:m⊢ ∀ x ∈ S, (∑ x_1, A i x_1 * if f x = x_1 then u x else 0) = A i (f x) * u x n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:mj:na✝:j ∈ S⊢ (∑ x, A i x * if f j = x then u j else 0) = A i (f j) * u j n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:mj:na✝:j ∈ S⊢ (A i (f j) * if f j = f j then u j else 0) = A i (f j) * u jn:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:mj:na✝:j ∈ S⊢ ∀ b ∈ Finset.univ, b ≠ f j → (A i b * if f j = b then u j else 0) = 0n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:mj:na✝:j ∈ S⊢ f j ∉ Finset.univ → (A i (f j) * if f j = f j then u j else 0) = 0 n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:mj:na✝:j ∈ S⊢ (A i (f j) * if f j = f j then u j else 0) = A i (f j) * u j All goals completed! 🐙 n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:mj:na✝:j ∈ S⊢ ∀ b ∈ Finset.univ, b ≠ f j → (A i b * if f j = b then u j else 0) = 0 n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:mj:na✝¹:j ∈ Sk:pa✝:k ∈ Finset.univhkj:k ≠ f j⊢ (A i k * if f j = k then u j else 0) = 0 All goals completed! 🐙 n:Type u_1p:Type u_2inst✝¹:Fintype pinst✝:DecidableEq pm:Type u_3S:Finset nf:n → pu:n → ℂA:Matrix m p ℂi:mj:na✝:j ∈ S⊢ f j ∉ Finset.univ → (A i (f j) * if f j = f j then u j else 0) = 0 All goals completed! 🐙theorem masked_column_restriction_norm_le {m : Type*} [Fintype m] [DecidableEq m] (S : Finset n) (f : n → p) (hf : Set.InjOn f S) (A : Matrix m p ℂ) : ‖operator (fun i j => if j ∈ S then A i (f j) else 0)‖ ≤ ‖operator A‖ := n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mS:Finset nf:n → phf:InjOn f ↑SA:Matrix m p ℂ⊢ ‖operator fun i j => if j ∈ S then A i (f j) else 0‖ ≤ ‖operator A‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mS:Finset nf:n → phf:InjOn f ↑SA:Matrix m p ℂ⊢ ∀ (x : EuclideanSpace ℂ n), ‖(operator fun i j => if j ∈ S then A i (f j) else 0) x‖ ≤ ‖operator A‖ * ‖x‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mS:Finset nf:n → phf:InjOn f ↑SA:Matrix m p ℂu:EuclideanSpace ℂ n⊢ ‖(operator fun i j => if j ∈ S then A i (f j) else 0) u‖ ≤ ‖operator A‖ * ‖u‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mS:Finset nf:n → phf:InjOn f ↑SA:Matrix m p ℂu:EuclideanSpace ℂ nv:EuclideanSpace ℂ p := WithLp.toLp 2 (extendByZero S f u.ofLp)⊢ ‖(operator fun i j => if j ∈ S then A i (f j) else 0) u‖ ≤ ‖operator A‖ * ‖u‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mS:Finset nf:n → phf:InjOn f ↑SA:Matrix m p ℂu:EuclideanSpace ℂ nv:EuclideanSpace ℂ p := WithLp.toLp 2 (extendByZero S f u.ofLp)hv:‖v‖ ≤ ‖u‖⊢ ‖(operator fun i j => if j ∈ S then A i (f j) else 0) u‖ ≤ ‖operator A‖ * ‖u‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mS:Finset nf:n → phf:InjOn f ↑SA:Matrix m p ℂu:EuclideanSpace ℂ nv:EuclideanSpace ℂ p := WithLp.toLp 2 (extendByZero S f u.ofLp)hv:‖v‖ ≤ ‖u‖heq:(operator fun i j => if j ∈ S then A i (f j) else 0) u = (operator A) v⊢ ‖(operator fun i j => if j ∈ S then A i (f j) else 0) u‖ ≤ ‖operator A‖ * ‖u‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mS:Finset nf:n → phf:InjOn f ↑SA:Matrix m p ℂu:EuclideanSpace ℂ nv:EuclideanSpace ℂ p := WithLp.toLp 2 (extendByZero S f u.ofLp)hv:‖v‖ ≤ ‖u‖heq:(operator fun i j => if j ∈ S then A i (f j) else 0) u = (operator A) v⊢ ‖(operator A) v‖ ≤ ‖operator A‖ * ‖u‖ All goals completed! 🐙theorem column_restriction_norm_le {m : Type*} [Fintype m] [DecidableEq m] (f : n → p) (hf : Function.Injective f) (A : Matrix m p ℂ) : ‖operator (fun i j => A i (f j))‖ ≤ ‖operator A‖ := n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mf:n → phf:Function.Injective fA:Matrix m p ℂ⊢ ‖operator fun i j => A i (f j)‖ ≤ ‖operator A‖ All goals completed! 🐙theorem row_restriction_norm_le {m : Type*} [Fintype m] [DecidableEq m] (f : n → p) (hf : Function.Injective f) (A : Matrix p m ℂ) : ‖operator (fun i j => A (f i) j)‖ ≤ ‖operator A‖ := n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mf:n → phf:Function.Injective fA:Matrix p m ℂ⊢ ‖operator fun i j => A (f i) j‖ ≤ ‖operator A‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mf:n → phf:Function.Injective fA:Matrix p m ℂB:Matrix n m ℂ := fun i j => A (f i) j⊢ ‖operator fun i j => A (f i) j‖ ≤ ‖operator A‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mf:n → phf:Function.Injective fA:Matrix p m ℂB:Matrix n m ℂ := fun i j => A (f i) jh:‖operator fun i j => A.conjTranspose i (f j)‖ ≤ ‖operator A.conjTranspose‖⊢ ‖operator fun i j => A (f i) j‖ ≤ ‖operator A‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mf:n → phf:Function.Injective fA:Matrix p m ℂB:Matrix n m ℂ := fun i j => A (f i) jh:‖operator B.conjTranspose‖ ≤ ‖operator A.conjTranspose‖⊢ ‖operator fun i j => A (f i) j‖ ≤ ‖operator A‖ n:Type u_1p:Type u_2inst✝⁵:Fintype ninst✝⁴:Fintype pinst✝³:DecidableEq ninst✝²:DecidableEq pm:Type u_3inst✝¹:Fintype minst✝:DecidableEq mf:n → phf:Function.Injective fA:Matrix p m ℂB:Matrix n m ℂ := fun i j => A (f i) jh:‖operator B‖ ≤ ‖operator A‖⊢ ‖operator fun i j => A (f i) j‖ ≤ ‖operator A‖ All goals completed! 🐙theorem submatrix_norm_le {m q : Type*} [Fintype m] [Fintype q] [DecidableEq m] [DecidableEq q] (r : m → q) (hr : Function.Injective r) (c : n → p) (hc : Function.Injective c) (A : Matrix q p ℂ) : ‖operator (fun i j => A (r i) (c j))‖ ≤ ‖operator A‖ := (row_restriction_norm_le r hr (fun i j => A i (c j))).trans (column_restriction_norm_le c hc A)end FiniteSieveRestrictionopen scoped BigOperatorsnamespace FiniteSieveOperatortheorem squared_norm_le_of_energy {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (A : Matrix m n ℂ) (C : ℝ) (hC : 0 ≤ C) (h : ∀ a : n → ℂ, (∑ i, ‖∑ j, A i j * a j‖ ^ 2) ≤ C * ∑ j, ‖a j‖ ^ 2) : ‖operator A‖ ^ 2 ≤ C := m:Type u_1n:Type u_2inst✝³:Fintype minst✝²:Fintype ninst✝¹:DecidableEq minst✝:DecidableEq nA:Matrix m n ℂC:ℝhC:0 ≤ Ch:∀ (a : n → ℂ), ∑ i, ‖∑ j, A i j * a j‖ ^ 2 ≤ C * ∑ j, ‖a j‖ ^ 2⊢ ‖operator A‖ ^ 2 ≤ C m:Type u_1n:Type u_2inst✝³:Fintype minst✝²:Fintype ninst✝¹:DecidableEq minst✝:DecidableEq nA:Matrix m n ℂC:ℝhC:0 ≤ Ch:∀ (a : n → ℂ), ∑ i, ‖∑ j, A i j * a j‖ ^ 2 ≤ C * ∑ j, ‖a j‖ ^ 2hop:‖operator A‖ ≤ √C⊢ ‖operator A‖ ^ 2 ≤ C All goals completed! 🐙end FiniteSieveOperatoropen scoped BigOperators Classicalnamespace CanonicalQuadraticSieveabbrev O := ActualEisensteinCubic.Oopen ConcretePrimeRowBridge ActualEisensteinCubic CompletedGausstheorem idealSexticRow_ambient (F G : Finset (Ideal O)) (hFp : ∀ I ∈ F, I ≠ ⊥) (hGp : ∀ I ∈ G, I ≠ ⊥) (hFg : ∀ I ∈ F, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (hGg : ∀ I ∈ G, ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, goodLambda ∉ P) (I : Ideal O) (hIF : I ∈ F) (hIG : I ∈ G) (z : O) : idealSexticRow F hFp hFg I z = idealSexticRow G hGp hGg I z := F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:O⊢ idealSexticRow F hFp hFg I z = idealSexticRow G hGp hGg I z F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ idealSexticRow F hFp hFg I z = idealSexticRow G hGp hGg I z F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ ∏ i ∈ idealSupport F I, (canonicalSextic ((fun i => ↑i) i) ⋯) ((Ideal.Quotient.mk ((fun i => ↑i) i)) z) = ∏ i ∈ idealSupport G I, (canonicalSextic ((fun i => ↑i) i) ⋯) ((Ideal.Quotient.mk ((fun i => ↑i) i)) z) F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ ∀ (a : ↥(primePool F)) (ha : a ∈ idealSupport F I), idx a ha ∈ idealSupport G IF:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ ∀ (a₁ : ↥(primePool F)) (ha₁ : a₁ ∈ idealSupport F I) (a₂ : ↥(primePool F)) (ha₂ : a₂ ∈ idealSupport F I), idx a₁ ha₁ = idx a₂ ha₂ → a₁ = a₂F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ ∀ b ∈ idealSupport G I, ∃ a, ∃ (ha : a ∈ idealSupport F I), idx a ha = bF:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ ∀ (a : ↥(primePool F)) (ha : a ∈ idealSupport F I), (canonicalSextic ((fun i => ↑i) a) ⋯) ((Ideal.Quotient.mk ((fun i => ↑i) a)) z) = (canonicalSextic ((fun i => ↑i) (idx a ha)) ⋯) ((Ideal.Quotient.mk ((fun i => ↑i) (idx a ha))) z) F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ ∀ (a : ↥(primePool F)) (ha : a ∈ idealSupport F I), idx a ha ∈ idealSupport G I F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩i:↥(primePool F)hi:i ∈ idealSupport F I⊢ idx i hi ∈ idealSupport G I All goals completed! 🐙 F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ ∀ (a₁ : ↥(primePool F)) (ha₁ : a₁ ∈ idealSupport F I) (a₂ : ↥(primePool F)) (ha₂ : a₂ ∈ idealSupport F I), idx a₁ ha₁ = idx a₂ ha₂ → a₁ = a₂ F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩i:↥(primePool F)hi:i ∈ idealSupport F Ij:↥(primePool F)hj:j ∈ idealSupport F Ihij:idx i hi = idx j hj⊢ i = j All goals completed! 🐙 F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ ∀ b ∈ idealSupport G I, ∃ a, ∃ (ha : a ∈ idealSupport F I), idx a ha = b F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩j:↥(primePool G)hj:j ∈ idealSupport G I⊢ ∃ a, ∃ (ha : a ∈ idealSupport F I), idx a ha = j F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩j:↥(primePool G)hj:j ∈ idealSupport G Ii:↥(primePool F) := ⟨↑j, ⋯⟩⊢ ∃ a, ∃ (ha : a ∈ idealSupport F I), idx a ha = j F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩j:↥(primePool G)hj:j ∈ idealSupport G Ii:↥(primePool F) := ⟨↑j, ⋯⟩hi:i ∈ idealSupport F I⊢ ∃ a, ∃ (ha : a ∈ idealSupport F I), idx a ha = j All goals completed! 🐙 F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩⊢ ∀ (a : ↥(primePool F)) (ha : a ∈ idealSupport F I), (canonicalSextic ((fun i => ↑i) a) ⋯) ((Ideal.Quotient.mk ((fun i => ↑i) a)) z) = (canonicalSextic ((fun i => ↑i) (idx a ha)) ⋯) ((Ideal.Quotient.mk ((fun i => ↑i) (idx a ha))) z) F:Finset (Ideal O)G:Finset (Ideal O)hFp:∀ I ∈ F, I ≠ ⊥hGp:∀ I ∈ G, I ≠ ⊥hFg:∀ I ∈ F, ∀ P ∈ normalizedFactors I, goodLambda ∉ PhGg:∀ I ∈ G, ∀ P ∈ normalizedFactors I, goodLambda ∉ PI:Ideal OhIF:I ∈ FhIG:I ∈ Gz:Oidx:(i : ↥(primePool F)) → i ∈ idealSupport F I → ↥(primePool G) := fun i hi => ⟨↑i, ⋯⟩i:↥(primePool F)hi:i ∈ idealSupport F I⊢ (canonicalSextic ((fun i => ↑i) i) ⋯) ((Ideal.Quotient.mk ((fun i => ↑i) i)) z) = (canonicalSextic ((fun i => ↑i) (idx i hi)) ⋯) ((Ideal.Quotient.mk ((fun i => ↑i) (idx i hi))) z) All goals completed! 🐙def Admissible (I : Ideal O) : Prop := I ≠ 0 ∧ Squarefree I ∧ ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors I, lambda ∉ P ∧ ringChar (O ⧸ P) ≠ 2theorem singletonPositive (I : Ideal O) (h : Admissible I) : ∀ J ∈ ({I} : Finset (Ideal O)), J ≠ ⊥ := I:Ideal Oh:Admissible I⊢ ∀ J ∈ {I}, J ≠ ⊥ I:Ideal Oh:Admissible IJ:Ideal OhJ:J ∈ {I}⊢ J ≠ ⊥ J:Ideal Oh:Admissible JhJ:J ∈ {J}⊢ J ≠ ⊥ All goals completed! 🐙theorem singletonGood (I : Ideal O) (h : Admissible I) : ∀ J ∈ ({I} : Finset (Ideal O)), ∀ P ∈ UniqueFactorizationMonoid.normalizedFactors J, goodLambda ∉ P := I:Ideal Oh:Admissible I⊢ ∀ J ∈ {I}, ∀ P ∈ normalizedFactors J, goodLambda ∉ P I:Ideal Oh:Admissible IJ:Ideal OhJ:J ∈ {I}P:Ideal OhP:P ∈ normalizedFactors J⊢ goodLambda ∉ P J:Ideal OP:Ideal OhP:P ∈ normalizedFactors Jh:Admissible JhJ:J ∈ {J}⊢ goodLambda ∉ P All goals completed! 🐙def quadraticRow (I : Ideal O) (z : O) : ℂ := if h : Admissible I then (idealSexticRow {I} (singletonPositive I h) (singletonGood I h) I z) ^ 3 else 0theorem quadraticRow_eq (F : Finset (Ideal O)) (hF : ∀ I ∈ F, Admissible I) (I : Ideal O) (hI : I ∈ F) (z : O) : quadraticRow I z = (idealSexticRow F (fun J hJ => (hF J hJ).1) (fun J hJ P hP => (hF J hJ).2.2 P hP |>.1) I z) ^ 3 := F:Finset (Ideal O)hF:∀ I ∈ F, Admissible II:Ideal OhI:I ∈ Fz:O⊢ quadraticRow I z = idealSexticRow F ⋯ ⋯ I z ^ 3 F:Finset (Ideal O)hF:∀ I ∈ F, Admissible II:Ideal OhI:I ∈ Fz:O⊢ idealSexticRow {I} ⋯ ⋯ I z ^ 3 = idealSexticRow F ⋯ ⋯ I z ^ 3 F:Finset (Ideal O)hF:∀ I ∈ F, Admissible II:Ideal OhI:I ∈ Fz:O⊢ idealSexticRow {I} ⋯ ⋯ I z = idealSexticRow F ⋯ ⋯ I z All goals completed! 🐙def idealRange (X : ℝ) : Finset (Ideal O) := (idealsUpTo ⌊X⌋₊).filter Admissibletheorem mem_idealRange {X : ℝ} {I : Ideal O} : I ∈ idealRange X ↔ Admissible I ∧ (Ideal.absNorm I : ℝ) ≤ X := X:ℝI:Ideal O⊢ I ∈ idealRange X ↔ Admissible I ∧ ↑(absNorm I) ≤ X X:ℝI:Ideal O⊢ (1 ≤ absNorm I ∧ absNorm I ≤ ⌊X⌋₊) ∧ Admissible I ↔ Admissible I ∧ ↑(absNorm I) ≤ X X:ℝI:Ideal O⊢ (1 ≤ absNorm I ∧ absNorm I ≤ ⌊X⌋₊) ∧ Admissible I → Admissible I ∧ ↑(absNorm I) ≤ XX:ℝI:Ideal O⊢ Admissible I ∧ ↑(absNorm I) ≤ X → (1 ≤ absNorm I ∧ absNorm I ≤ ⌊X⌋₊) ∧ Admissible I X:ℝI:Ideal O⊢ (1 ≤ absNorm I ∧ absNorm I ≤ ⌊X⌋₊) ∧ Admissible I → Admissible I ∧ ↑(absNorm I) ≤ X X:ℝI:Ideal Oha:Admissible Ihp:1 ≤ absNorm IhN:absNorm I ≤ ⌊X⌋₊⊢ Admissible I ∧ ↑(absNorm I) ≤ X X:ℝI:Ideal Oha:Admissible Ihp:1 ≤ absNorm IhN:absNorm I ≤ ⌊X⌋₊⊢ ↑(absNorm I) ≤ X X:ℝI:Ideal Oha:Admissible Ihp:1 ≤ absNorm IhN:absNorm I ≤ ⌊X⌋₊hX:0 ≤ X⊢ ↑(absNorm I) ≤ X All goals completed! 🐙 X:ℝI:Ideal O⊢ Admissible I ∧ ↑(absNorm I) ≤ X → (1 ≤ absNorm I ∧ absNorm I ≤ ⌊X⌋₊) ∧ Admissible I X:ℝI:Ideal Oha:Admissible IhN:↑(absNorm I) ≤ X⊢ (1 ≤ absNorm I ∧ absNorm I ≤ ⌊X⌋₊) ∧ Admissible I All goals completed! 🐙theorem idealRange_mono {X Y : ℝ} (h : X ≤ Y) : idealRange X ⊆ idealRange Y := X:ℝY:ℝh:X ≤ Y⊢ idealRange X ⊆ idealRange Y X:ℝY:ℝh:X ≤ YI:Ideal OhI:I ∈ idealRange X⊢ I ∈ idealRange Y X:ℝY:ℝh:X ≤ YI:Ideal OhI:I ∈ idealRange Xha:Admissible IhN:↑(absNorm I) ≤ X⊢ I ∈ idealRange Y All goals completed! 🐙def matrix (M N : ℝ) : Matrix (idealRange M) (idealRange N) ℂ := fun I J => quadraticRow J.val (primaryGenerator I.val)def sieveNorm (M N : ℝ) : ℝ := ‖FiniteSieveOperator.operator (matrix M N)‖ ^ 2theorem sieveNorm_nonneg (M N : ℝ) : 0 ≤ sieveNorm M N := sq_nonneg _def rangeInclusion {X Y : ℝ} (h : X ≤ Y) (I : idealRange X) : idealRange Y := ⟨I.val, idealRange_mono h I.property⟩theorem rangeInclusion_injective {X Y : ℝ} (h : X ≤ Y) : Function.Injective (rangeInclusion h) := X:ℝY:ℝh:X ≤ Y⊢ Function.Injective (rangeInclusion h) X:ℝY:ℝh:X ≤ YI:↥(idealRange X)J:↥(idealRange X)heq:rangeInclusion h I = rangeInclusion h J⊢ I = J All goals completed! 🐙theorem sieveNorm_mono {M N M' N' : ℝ} (hM : M ≤ M') (hN : N ≤ N') : sieveNorm M N ≤ sieveNorm M' N' := M:ℝN:ℝM':ℝN':ℝhM:M ≤ M'hN:N ≤ N'⊢ sieveNorm M N ≤ sieveNorm M' N' M:ℝN:ℝM':ℝN':ℝhM:M ≤ M'hN:N ≤ N'h:‖FiniteSieveOperator.operator fun i j => matrix M' N' (rangeInclusion hM i) (rangeInclusion hN j)‖ ≤ ‖FiniteSieveOperator.operator (matrix M' N')‖⊢ sieveNorm M N ≤ sieveNorm M' N' M:ℝN:ℝM':ℝN':ℝhM:M ≤ M'hN:N ≤ N'h:‖FiniteSieveOperator.operator (matrix M N)‖ ≤ ‖FiniteSieveOperator.operator (matrix M' N')‖⊢ sieveNorm M N ≤ sieveNorm M' N' All goals completed! 🐙theorem family_squared_norm_le {m n : Type*} [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] (rows : m → Ideal O) (cols : n → Ideal O) (hr : Function.Injective rows) (hc : Function.Injective cols) (M N : ℝ) (hrows : ∀ i, Admissible (rows i) ∧ (Ideal.absNorm (rows i) : ℝ) ≤ M) (hcols : ∀ j, Admissible (cols j) ∧ (Ideal.absNorm (cols j) : ℝ) ≤ N) : ‖FiniteSieveOperator.operator (fun i j => quadraticRow (cols j) (primaryGenerator (rows i)))‖ ^ 2 ≤ sieveNorm M N := m:Type u_1n:Type u_2inst✝³:Fintype minst✝²:Fintype ninst✝¹:DecidableEq minst✝:DecidableEq nrows:m → Ideal Ocols:n → Ideal Ohr:Function.Injective rowshc:Function.Injective colsM:ℝN:ℝhrows:∀ (i : m), Admissible (rows i) ∧ ↑(absNorm (rows i)) ≤ Mhcols:∀ (j : n), Admissible (cols j) ∧ ↑(absNorm (cols j)) ≤ N⊢ ‖FiniteSieveOperator.operator fun i j => quadraticRow (cols j) (primaryGenerator (rows i))‖ ^ 2 ≤ sieveNorm M N m:Type u_1n:Type u_2inst✝³:Fintype minst✝²:Fintype ninst✝¹:DecidableEq minst✝:DecidableEq nrows:m → Ideal Ocols:n → Ideal Ohr:Function.Injective rowshc:Function.Injective colsM:ℝN:ℝhrows:∀ (i : m), Admissible (rows i) ∧ ↑(absNorm (rows i)) ≤ Mhcols:∀ (j : n), Admissible (cols j) ∧ ↑(absNorm (cols j)) ≤ Nr:m → ↥(idealRange M) := fun i => ⟨rows i, ⋯⟩⊢ ‖FiniteSieveOperator.operator fun i j => quadraticRow (cols j) (primaryGenerator (rows i))‖ ^ 2 ≤ sieveNorm M N m:Type u_1n:Type u_2inst✝³:Fintype minst✝²:Fintype ninst✝¹:DecidableEq minst✝:DecidableEq nrows:m → Ideal Ocols:n → Ideal Ohr:Function.Injective rowshc:Function.Injective colsM:ℝN:ℝhrows:∀ (i : m), Admissible (rows i) ∧ ↑(absNorm (rows i)) ≤ Mhcols:∀ (j : n), Admissible (cols j) ∧ ↑(absNorm (cols j)) ≤ Nr:m → ↥(idealRange M) := fun i => ⟨rows i, ⋯⟩c:n → ↥(idealRange N) := fun j => ⟨cols j, ⋯⟩⊢ ‖FiniteSieveOperator.operator fun i j => quadraticRow (cols j) (primaryGenerator (rows i))‖ ^ 2 ≤ sieveNorm M N m:Type u_1n:Type u_2inst✝³:Fintype minst✝²:Fintype ninst✝¹:DecidableEq minst✝:DecidableEq nrows:m → Ideal Ocols:n → Ideal Ohr:Function.Injective rowshc:Function.Injective colsM:ℝN:ℝhrows:∀ (i : m), Admissible (rows i) ∧ ↑(absNorm (rows i)) ≤ Mhcols:∀ (j : n), Admissible (cols j) ∧ ↑(absNorm (cols j)) ≤ Nr:m → ↥(idealRange M) := fun i => ⟨rows i, ⋯⟩c:n → ↥(idealRange N) := fun j => ⟨cols j, ⋯⟩hri:Function.Injective r⊢ ‖FiniteSieveOperator.operator fun i j => quadraticRow (cols j) (primaryGenerator (rows i))‖ ^ 2 ≤ sieveNorm M N m:Type u_1n:Type u_2inst✝³:Fintype minst✝²:Fintype ninst✝¹:DecidableEq minst✝:DecidableEq nrows:m → Ideal Ocols:n → Ideal Ohr:Function.Injective rowshc:Function.Injective colsM:ℝN:ℝhrows:∀ (i : m), Admissible (rows i) ∧ ↑(absNorm (rows i)) ≤ Mhcols:∀ (j : n), Admissible (cols j) ∧ ↑(absNorm (cols j)) ≤ Nr:m → ↥(idealRange M) := fun i => ⟨rows i, ⋯⟩c:n → ↥(idealRange N) := fun j => ⟨cols j, ⋯⟩hri:Function.Injective rhci:Function.Injective c⊢ ‖FiniteSieveOperator.operator fun i j => quadraticRow (cols j) (primaryGenerator (rows i))‖ ^ 2 ≤ sieveNorm M N m:Type u_1n:Type u_2inst✝³:Fintype minst✝²:Fintype ninst✝¹:DecidableEq minst✝:DecidableEq nrows:m → Ideal Ocols:n → Ideal Ohr:Function.Injective rowshc:Function.Injective colsM:ℝN:ℝhrows:∀ (i : m), Admissible (rows i) ∧ ↑(absNorm (rows i)) ≤ Mhcols:∀ (j : n), Admissible (cols j) ∧ ↑(absNorm (cols j)) ≤ Nr:m → ↥(idealRange M) := fun i => ⟨rows i, ⋯⟩c:n → ↥(idealRange N) := fun j => ⟨cols j, ⋯⟩hri:Function.Injective rhci:Function.Injective ch:‖FiniteSieveOperator.operator fun i j => matrix M N (r i) (c j)‖ ≤ ‖FiniteSieveOperator.operator (matrix M N)‖⊢ ‖FiniteSieveOperator.operator fun i j => quadraticRow (cols j) (primaryGenerator (rows i))‖ ^ 2 ≤ sieveNorm M N All goals completed! 🐙theorem energy_bound (M N : ℝ) (a : idealRange N → ℂ) : (∑ I : idealRange M, ‖∑ J : idealRange N, quadraticRow J.val (primaryGenerator I.val) * a J‖ ^ 2) ≤ sieveNorm M N * ∑ J, ‖a J‖ ^ 2 := FiniteSieveOperator.energy_bound (matrix M N) aend CanonicalQuadraticSieveendend OAI