Trilinear Hilbert transform: three_path_total #
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_path_total
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCA : 1 ≤ CA)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ0 : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
(hdD : ↑D.S.dmax ≤ D.S.Dstar)
(qG : bf.Grp → ℕ)
(hqG : ∀ (G : bf.Grp), 1 ≤ qG G ∧ qG G ≤ D.S.Q0)
(J : ℕ)
(hJ : 1 ≤ J)
(Aw Iw : ℕ)
(hIw : 2 ^ Iw ≤ 2 * D.U0)
(l : Fin 4)
(T : Finset (ℤ × ℤ))
(gs : ℤ × ℤ → Finset bf.Grp)
(z : bf.Grp → ChartTag)
(hGc :
∀ I ∈ T,
∀ G ∈ gs I, (∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) ∧ (∀ (j : Fin 4), (D.Ms j G).zc = z G) ∧ (z G).dim ≤ D.S.dmax)
(H : Finset ℕ)
(hH : ∀ h ∈ H, h ≤ D.SP.Jst)
(rep : ℕ → (G : bf.Grp) → (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md)
(hrep : ∀ h ∈ H, ∀ I ∈ T, ∀ G ∈ gs I, ∀ (j : Fin 4), (D.withQ0 (qG G)).RepOK G j h T (rep h G j))
(anc :
(I : ℤ × ℤ) →
(G : bf.Grp) →
D.AncNe3 G I l →
ℕ →
(j : Fin 4) →
j ≠ l →
Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(hanc :
∀ (h : ℕ) (hh : h ∈ H) (I : ℤ × ℤ) (hI : I ∈ T) (G : bf.Grp) (hG : G ∈ gs I) (hA : D.AncNe3 G I l) (j : Fin 4)
(hj : j ≠ l) (F : Finset ((D.withQ0 (qG G)).Ms j G).Md) (hF : F ∈ (D.withQ0 (qG G)).goodCls G I j h),
anc I G hA h j hj F = (D.withQ0 (qG G)).repAnchor G I j h (rep h G j) ⋯ hF)
{U ε : ℝ}
(hε : 0 < ε)
(hεU : ε ≤ U)
(hU :
∀ I ∈ T,
∀ G ∈ gs I,
∀ h ∈ H, ∀ (j : Fin 4), j ≠ l → ∀ F ∈ (D.withQ0 (qG G)).goodCls G I j h, (D.withQ0 (qG G)).clsSize G I j F ≤ U)
(hUs :
∀ I ∈ T,
∀ G ∈ gs I,
√((dyadicGridLength A.G I.1)⁻¹ * ∫ (y : ℝ) in dyadicGridLeft A.G I.1 I.2..dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1, ‖augPhys ((D.withQ0 (qG G)).toLeaf.sv l G I) y‖ ^ 2) ≤ U)
{K K₁ : ℝ}
(hK : 0 ≤ K)
(hK₁ : 0 ≤ K₁)
(y : ℝ)
(hcap :
∀ h ∈ H,
10 ≤ h →
∀ (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)),
0 < c.1 →
c.1 ≤ 1 →
1 ≤ c.2.1 →
(∀ (i : Fin 4), 0 < threeAmp l c i) →
(∀ (j : Fin 4), ε ≤ threeAmp l c j ∧ threeAmp l c j ≤ U ∧ ∃ (k : ℤ), threeAmp l c j = 2 ^ k) →
∀ (κ : Fin 4 → ℕ × ℕ),
(∀ (i : Fin 4) (hi : i ≠ l),
∑ G ∈ pathGroups T gs y,
↑((D.withQ0 (qG G)).threeUsedReps G h y l (pathCell A.G T y)
(fun (s : ℤ) => anc (pathCell A.G T y s) G) Iw c κ (pathDepths T gs y G) i hi).card ≤ K * threeAmp l c i ^ (-2)) ∧ ∑ G ∈ pathGroups T gs y,
∑ s ∈ pathDepths T gs y G, (D.withQ0 (qG G)).sideWeight G l (pathCell A.G T y) c.2.2.2.1 s ≤ K * threeAmp l c l ^ (-2))
:
∑ I ∈ T with y ∈ dyadicGridCell A.G I.1 I.2,
∑ x ∈ gs I ×ˢ H ×ˢ D.threeTypes l,
(K₁ * ((↑H.card)⁻¹ * ∑ c ∈ (D.withQ0 (qG x.1)).threeRetBinsA x.1 I y l (anc I x.1) Iw x.2.1 ε,
threeBinVal κ' J Aw l c * (D.withQ0 (qG x.1)).threeCntA x.1 I y l (anc I x.1) Iw x.2.1 c x.2.2)) ^ (1 - 1 / 300 / 4) ≤ ↑H.card * ↑(D.threeTypes l).card * ((K₁ * (8 * entryCU κ' J Aw * 2 ^ (Aw + 4) * 12 ^ 3)) ^ (1 - 1 / 300 / 4) * (D.fourCc * K ^ (2 - 1 / 300 / 2)) * ((↑Iw + 1) * ((Real.logb 2 (U / ε) + 1) ^ 4 * bandC (1 - 1 / 300 / 4) J)))
Blueprint lines 2783-2817 at one point y for three cores with side role l: the powered
retained principal
quantities of the cells of the path of y (over their groups, the heights and the role types) sum
to at most |H| |types| (K₁ C_J 2 · 12⁴)^p C_c K^{2-c/2} (log₂(U/ε) + 1)⁴ C_band.
theorem
TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_core_final_side
{κ' : LocalKernelClass}
{c₀ : ℕ}
{A : ActiveSetup κ' c₀}
{bf : A.BasicFamilies}
{fp : bf.FamParams}
(D : fp.SideInput)
{Cj CA CT CK : ℕ}
{δs W : ℝ}
(hV : D.S.Valid Cj CA CT CK δs W)
(hCA : 1 ≤ CA)
(hCT : 4 ≤ CT)
(hd2 : 2 ≤ D.S.dmax)
(hD : 2 ≤ D.S.Dstar)
(hB : 2 ≤ D.S.Bstar)
(hQ0 : 1 ≤ D.S.Q0)
(hSP : D.SP = D.S.sideParams δs)
(hdD : ↑D.S.dmax ≤ D.S.Dstar)
(qG : bf.Grp → ℕ)
(hqG : ∀ (G : bf.Grp), 1 ≤ qG G ∧ qG G ≤ D.S.Q0)
(J : ℕ)
(hJ : 1 ≤ J)
(Aw Iw : ℕ)
(hIw : 2 ^ Iw ≤ 2 * D.U0)
(l : Fin 4)
(R : ℤ × ℤ)
(T : Finset (ℤ × ℤ))
(hT : ∀ I ∈ T, dyadicGridCell A.G I.1 I.2 ⊆ dyadicGridCell A.G R.1 R.2)
(gs : ℤ × ℤ → Finset bf.Grp)
(z : bf.Grp → ChartTag)
(hGc :
∀ I ∈ T,
∀ G ∈ gs I, (∀ (j : Fin 4), 8 * (D.Ms j G).Λ ≤ D.S.Ξ) ∧ (∀ (j : Fin 4), (D.Ms j G).zc = z G) ∧ (z G).dim ≤ D.S.dmax)
(H : Finset ℕ)
(hH : ∀ h ∈ H, h ≤ D.SP.Jst)
(rep : ℕ → (G : bf.Grp) → (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md)
(hrep : ∀ h ∈ H, ∀ I ∈ T, ∀ G ∈ gs I, ∀ (j : Fin 4), (D.withQ0 (qG G)).RepOK G j h T (rep h G j))
(anc :
(I : ℤ × ℤ) →
(G : bf.Grp) →
D.AncNe3 G I l →
ℕ →
(j : Fin 4) →
j ≠ l →
Finset (D.Ms j G).Md → ↥((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))))
(hanc :
∀ (h : ℕ) (hh : h ∈ H) (I : ℤ × ℤ) (hI : I ∈ T) (G : bf.Grp) (hG : G ∈ gs I) (hA : D.AncNe3 G I l) (j : Fin 4)
(hj : j ≠ l) (F : Finset ((D.withQ0 (qG G)).Ms j G).Md) (hF : F ∈ (D.withQ0 (qG G)).goodCls G I j h),
anc I G hA h j hj F = (D.withQ0 (qG G)).repAnchor G I j h (rep h G j) ⋯ hF)
(hcard :
∀ I ∈ T,
∀ G ∈ gs I,
∀ (j : Fin 4), ↑((D.Ms j G).alive (ancAt A.G (D.preAt I) (A.blkStart D.S.K I.1 - 4 * ↑D.S.K))).card ≤ D.S.Dstar)
{U ε : ℝ}
(hε : 0 < ε)
(hεU : ε ≤ U)
(hU :
∀ I ∈ T,
∀ G ∈ gs I,
∀ h ∈ H, ∀ (j : Fin 4), j ≠ l → ∀ F ∈ (D.withQ0 (qG G)).goodCls G I j h, (D.withQ0 (qG G)).clsSize G I j F ≤ U)
(hUs :
∀ I ∈ T,
∀ G ∈ gs I,
√((dyadicGridLength A.G I.1)⁻¹ * ∫ (y : ℝ) in dyadicGridLeft A.G I.1 I.2..dyadicGridLeft A.G I.1 I.2 + dyadicGridLength A.G I.1, ‖augPhys ((D.withQ0 (qG G)).toLeaf.sv l G I) y‖ ^ 2) ≤ U)
{K K₁ : ℝ}
(hK : 0 ≤ K)
(hK₁ : 0 ≤ K₁)
(hcap :
∀ (y : ℝ),
∀ h ∈ H,
10 ≤ h →
∀ (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)),
0 < c.1 →
c.1 ≤ 1 →
1 ≤ c.2.1 →
(∀ (i : Fin 4), 0 < threeAmp l c i) →
(∀ (j : Fin 4), ε ≤ threeAmp l c j ∧ threeAmp l c j ≤ U ∧ ∃ (k : ℤ), threeAmp l c j = 2 ^ k) →
∀ (κ : Fin 4 → ℕ × ℕ),
(∀ (i : Fin 4) (hi : i ≠ l),
∑ G ∈ pathGroups T gs y,
↑((D.withQ0 (qG G)).threeUsedReps G h y l (pathCell A.G T y)
(fun (s : ℤ) => anc (pathCell A.G T y s) G) Iw c κ (pathDepths T gs y G) i
hi).card ≤ K * threeAmp l c i ^ (-2)) ∧ ∑ G ∈ pathGroups T gs y,
∑ s ∈ pathDepths T gs y G, (D.withQ0 (qG G)).sideWeight G l (pathCell A.G T y) c.2.2.2.1 s ≤ K * threeAmp l c l ^ (-2))
(Λ3 Err : ℤ × ℤ → bf.Grp → ℝ)
(hErr : ∀ (I : ℤ × ℤ) (G : bf.Grp), 0 ≤ Err I G)
(hP :
∀ I ∈ T,
∀ G ∈ gs I,
∀ y ∈ dyadicGridCell A.G I.1 I.2,
Λ3 I G ≤ K₁ * ∑ h ∈ H, (↑H.card)⁻¹ * (D.withQ0 (qG G)).threeBinSumA J Aw Iw G I y l (anc I G) h + Err I G)
(CI : ℤ × ℤ → ℝ)
(hCI : ∀ I ∈ T, CI I ≤ ∑ G ∈ gs I, Λ3 I G)
{η : ℝ}
(hη : 0 ≤ η)
:
∑ I ∈ T, dyadicGridLength A.G I.1 * min η (CI I) ≤ η ^ (1 - (1 - 1 / 300 / 4)) * (dyadicGridLength A.G R.1 * (↑H.card * ↑(D.threeTypes l).card * ((K₁ * (8 * entryCU κ' J Aw * 2 ^ (Aw + 4) * 12 ^ 3)) ^ (1 - 1 / 300 / 4) * (D.fourCc * K ^ (2 - 1 / 300 / 2)) * ((↑Iw + 1) * ((Real.logb 2 (U / ε) + 1) ^ 4 * bandC (1 - 1 / 300 / 4) J))))) + ∑ I ∈ T,
dyadicGridLength A.G I.1 * ∑ G ∈ gs I,
(Err I G + K₁ * (8 * entryCU κ' J Aw * 2 ^ (Aw + 4) * 12 ^ 3 * ε * U ^ 3 * (D.S.Dstar ^ 3 * (↑Iw + 1))))
Blueprint eq:core-final (lines 2808-2817) for the three-core patterns with side role l on
the side states:
let T be the retained cells under the root R with their groups g(I), the anchors the
hereditary representatives, and assume the principal bounds of eq:principal-core
(‖Λ_{I,G}‖ ≤ K₁ × the height-averaged bin sum + err_{I,G}), the retained amplitudes σ ≤ U,
at most D_* alive modes, and the path caps of eq:top-count along every retained path.
Removing the negligible amplitudes (< ε), eq:min-power with subadditivity of x^p, the path
estimates (three_path_total) and eq:path give, with p = 1 - 1/1200,
Σ_I |I| min(η, C_I) ≤ η^{1/1200} |R| M_p + Σ_I |I| Σ_G (err_{I,G} + K₁ · negligible),
where M_p = |H| |types| (K₁ C₃)^p C_c K^{2-c/2} (I_w + 1) (log₂(U/ε) + 1)⁴ C_band is polynomial
in the parameters (P^{C₄}).
theorem
TrilinearHT.Auto.core_final_patterns
(G : RealDyadicGrid)
(T : Finset (ℤ × ℤ))
{τ : Type u_1}
(P : Finset τ)
(x : τ → ℤ × ℤ → ℝ)
(hx : ∀ t ∈ P, ∀ I ∈ T, 0 ≤ x t I)
(CI : ℤ × ℤ → ℝ)
(hCI : ∀ I ∈ T, CI I ≤ ∑ t ∈ P, x t I)
{η : ℝ}
(hη : 0 ≤ η)
:
∑ I ∈ T, dyadicGridLength G I.1 * min η (CI I) ≤ ∑ t ∈ P, ∑ I ∈ T, dyadicGridLength G I.1 * min η (x t I)
Blueprint eq:core-final over the patterns with at least three cores: if the core quantity of
each cell is at most the sum of the pattern quantities x_τ(I) ≥ 0, then
Σ_I |I| min(η, C_I) ≤ Σ_τ Σ_I |I| min(η, x_τ(I)), so the bounds for the four-core pattern and the
three-core patterns (four_core_final_side, three_core_final_side) add up.