Trilinear Hilbert transform: four_path_total

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_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) (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.AncNe G I → ℕ → (j : Fin 4) → 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.AncNe G I) (j : Fin 4) (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 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), ∀ F ∈ (D.withQ0 (qG G)).goodCls G I j h, (D.withQ0 (qG G)).clsSize G I j F ≤ 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 < c.2.2 i) → (∀ (j : Fin 4), ε ≤ c.2.2 j ∧ c.2.2 j ≤ U ∧ ∃ (k : ℤ), c.2.2 j = 2 ^ k) → ∀ (κ : Fin 4 → ℕ × ℕ) (i : Fin 4), ∑ G ∈ pathGroups T gs y, ↑((D.withQ0 (qG G)).fourUsedReps G h y (pathCell A.G T y) (fun (s : ℤ) => anc (pathCell A.G T y s) G) c κ (pathDepths T gs y G) i).card ≤ K * c.2.2 i ^ (-2)) : ∑ I ∈ T with y ∈ dyadicGridCell A.G I.1 I.2, ∑ x ∈ gs I ×ˢ H ×ˢ D.fourTypes, (K₁ * ((↑H.card)⁻¹ * ∑ c ∈ (D.withQ0 (qG x.1)).fourRetBinsA x.1 I y (anc I x.1) x.2.1 ε, fourBinVal κ' J c * (D.withQ0 (qG x.1)).fourCntA x.1 I y (anc I x.1) x.2.1 c x.2.2)) ^ (1 - 1 / 300 / 4) ≤ ↑H.card * ↑D.fourTypes.card * ((K₁ * (fourKC κ' J * 2 * 12 ^ 4)) ^ (1 - 1 / 300 / 4) * (D.fourCc * K ^ (2 - 1 / 300 / 2)) * ((Real.logb 2 (U / ε) + 1) ^ 4 * bandC (1 - 1 / 300 / 4) J))

Blueprint lines 2783-2817 at one point y for four cores: 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.fourBinVal_nonneg_of_mem {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (anc : ℕ → (j : Fin 4) → 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)))) (h : ℕ) {c : ℝ × ℝ × (Fin 4 → ℝ)} (hc : c ∈ Finset.image (D.fourBinOf G I xs anc h) (D.fourTested G I xs anc h)) : 0 ≤ fourBinVal κ' J c

Occupied four-core bins have nonnegative values.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourBinVal_nonneg_of_memA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J : ℕ) {G : bf.Grp} {I : ℤ × ℤ} {xs : ℝ} {anc : D.AncNe G I → ℕ → (j : Fin 4) → 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)))} {h : ℕ} {ε : ℝ} {c : ℝ × ℝ × (Fin 4 → ℝ)} (hc : c ∈ D.fourRetBinsA G I xs anc h ε) : 0 ≤ fourBinVal κ' J c

Retained four-core bins with anchors depending on AncNe G I have nonnegative values.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.four_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) (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.AncNe G I → ℕ → (j : Fin 4) → 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.AncNe G I) (j : Fin 4) (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 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), ∀ F ∈ (D.withQ0 (qG G)).goodCls G I j h, (D.withQ0 (qG G)).clsSize G I j F ≤ 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 < c.2.2 i) → (∀ (j : Fin 4), ε ≤ c.2.2 j ∧ c.2.2 j ≤ U ∧ ∃ (k : ℤ), c.2.2 j = 2 ^ k) → ∀ (κ : Fin 4 → ℕ × ℕ) (i : Fin 4), ∑ G ∈ pathGroups T gs y, ↑((D.withQ0 (qG G)).fourUsedReps G h y (pathCell A.G T y) (fun (s : ℤ) => anc (pathCell A.G T y s) G) c κ (pathDepths T gs y G) i).card ≤ K * c.2.2 i ^ (-2)) (Λ4 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, Λ4 I G ≤ K₁ * ∑ h ∈ H, (↑H.card)⁻¹ * (D.withQ0 (qG G)).fourBinSumA J G I y (anc I G) h + Err I G) (CI : ℤ × ℤ → ℝ) (hCI : ∀ I ∈ T, CI I ≤ ∑ G ∈ gs I, Λ4 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.fourTypes.card * ((K₁ * (fourKC κ' J * 2 * 12 ^ 4)) ^ (1 - 1 / 300 / 4) * (D.fourCc * K ^ (2 - 1 / 300 / 2)) * ((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₁ * (2 * fourKC κ' J * 12 ^ 4 * ε * U ^ 3 * D.S.Dstar ^ 4))

Blueprint eq:core-final (lines 2808-2817) for the four-core patterns 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 (four_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₁ · 2 C_J 12⁴ ε U³ D_*^4), where M_p = |H| |types| (K₁ C_J 2 · 12⁴)^p C_c K^{2-c/2} (log₂(U/ε) + 1)⁴ C_band is polynomial in the parameters (P^{C₄}).

theorem TrilinearHT.Auto.three_bins_sum_le {p : ℝ} (hp : 0 < p) (J : ℕ) (hJ : 1 ≤ J) (l : Fin 4) (Iw : ℕ) {ε U : ℝ} (hε : 0 < ε) (hεU : ε ≤ U) (B : Finset (ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ))) (hB : ∀ c ∈ B, (∃ (k : ℤ), c.1 = 2 ^ k) ∧ c.1 ≤ 1 ∧ (∃ (k : ℤ), c.2.1 = 2 ^ k) ∧ 1 ≤ c.2.1 ∧ c.2.2.1 ≤ Iw ∧ c.2.2.2.2 l = 1 ∧ ∀ (j : Fin 4), ε ≤ (fun (j : Fin 4) => if j = l then c.2.2.2.1 else c.2.2.2.2 j) j ∧ (fun (j : Fin 4) => if j = l then c.2.2.2.1 else c.2.2.2.2 j) j ≤ U ∧ ∃ (k : ℤ), (fun (j : Fin 4) => if j = l then c.2.2.2.1 else c.2.2.2.2 j) j = 2 ^ k) : ∑ c ∈ B, c.1 ^ p * (c.2.1 ^ J)⁻¹ ^ p * (1 + Real.log (8 * c.2.1 / c.1)) ^ 4 ≤ (↑Iw + 1) * ((Real.logb 2 (U / ε) + 1) ^ 4 * ∑' (t : ℕ × ℕ), (2 ^ (-p)) ^ t.1 * (2 ^ (-(↑J * p))) ^ t.2 * (4 ^ 4 * (1 + ↑t.1 + ↑t.2) ^ 4))

The sum over occupied three-core bins c = (μ, ν, i, b, σ) (shells i ≤ I_w, dyadic bands μ ≤ 1 ≤ ν, dyadic amplitudes threeAmp in [ε, U] for a fixed side role l): the powered kernel factors with the logarithmic coefficient sum to at most (I_w + 1) (log₂(U/ε) + 1)⁴ times the convergent band series.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeBinVal_eq {κ' : LocalKernelClass} (J Aw : ℕ) (l : Fin 4) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) : threeBinVal κ' J Aw l c = 8 * entryCU κ' J Aw * 2 ^ (Aw + 4) * 12 ^ 3 * (c.1 * (c.2.1 ^ J)⁻¹ * (2 ^ c.2.2.1)⁻¹ ^ (Aw + 1)) * ∏ j : Fin 4, threeAmp l c j

The three-core bin value factors as 8 C_{J,A} 2^{A+4} 12³ · μ ν^{-J} Λ^{-(A+1)} · Π threeAmp.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.dyadicBand_clsSize_empty {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (j : Fin 4) : dyadicBand (D.clsSize G I j ∅) = 1

The class size of the empty class is 0, so its band is 1.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeTested_eq_empty {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : ℕ → (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)))) (X : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Iw : ℕ) {h : ℕ} (hh : h < D.SP.Δ) : D.threeTested G I xs l anc X Iw h = ∅

Below the height Δ there are no tested three-core tuples.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeTypes {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (l : Fin 4) : Finset (Fin 4 → ℕ × ℕ)

The core role types with the side role normalized to (0, 0).

Equations

• D.threeTypes l = {κ ∈ D.fourTypes | κ l = (0, 0)}

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.card_bin_eq_sum_types3 {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : ℕ → (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)))) (X : ↥(ColumnL2 (bf.Lab ⊕ Fin fp.Mc))) (Iw h : ℕ) (hcard : ∀ (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) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) : ↑{q ∈ D.threeTested G I xs l anc X Iw h | D.threeBinOf G I xs l anc X h q = c}.card = ∑ κ ∈ D.threeTypes l, ↑{q ∈ D.threeTested G I xs l anc X Iw h | D.threeBinOf G I xs l anc X h q = c ∧ ∀ (j : Fin 4), j ≠ l → D.classTypeOf G I j h (q.1 j) = κ j}.card

The tested three-core tuples and shells of a bin split by their core role types.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeRetBins {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : ℕ → (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)))) (Iw h : ℕ) (ε : ℝ) : Finset (ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ))

The retained occupied three-core bins (all amplitudes of threeAmp at least ε).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeCnt {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : ℕ → (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)))) (Iw h : ℕ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) : ℝ

The number of tested three-core tuples and shells in the bin c with the core types κ.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeRetBinsA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : 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)))) (Iw h : ℕ) (ε : ℝ) : Finset (ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ))

The retained occupied three-core bins at a cell and group, with anchors depending on a proof of AncNe3 G I l (the alive sets of the core roles at the decision cell are nonempty); empty otherwise.

Equations

• D.threeRetBinsA G I xs l anc Iw h ε = if hA : D.AncNe3 G I l then D.threeRetBins G I xs l (anc hA) Iw h ε else ∅

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeCntA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : 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)))) (Iw h : ℕ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (κ : Fin 4 → ℕ × ℕ) : ℝ

The number of tested three-core tuples and shells in the bin c with the core types κ, with anchors depending on a proof of AncNe3 G I l; zero otherwise.

Equations

• D.threeCntA G I xs l anc Iw h c κ = if hA : D.AncNe3 G I l then D.threeCnt G I xs l (anc hA) Iw h c κ else 0

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeCntA_nonneg {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) {G : bf.Grp} {I : ℤ × ℤ} {xs : ℝ} {l : Fin 4} {anc : 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)))} {Iw h : ℕ} {c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)} {κ : Fin 4 → ℕ × ℕ} : 0 ≤ D.threeCntA G I xs l anc Iw h c κ

noncomputable def TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeBinSumA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (J Aw Iw : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : 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)))) (h : ℕ) : ℝ

The three-core bin sum Σ_c v(c) N_c of the tested tuples and shells at a cell, group and height (side role l, the principal quantity of eq:principal-core), with anchors depending on a proof of AncNe3 G I l; zero otherwise.

Equations

• One or more equations did not get rendered due to their size.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeBin_basic {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : ℕ → (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)))) (Iw h : ℕ) {c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)} (hc : c ∈ Finset.image (D.threeBinOf G I xs l anc (D.toLeaf.sv l G I) h) (D.threeTested G I xs l anc (D.toLeaf.sv l G I) Iw h)) : (∃ (k : ℤ), c.1 = 2 ^ k) ∧ c.1 ≤ 1 ∧ (∃ (k : ℤ), c.2.1 = 2 ^ k) ∧ 1 ≤ c.2.1 ∧ c.2.2.1 ≤ Iw ∧ c.2.2.2.2 l = 1 ∧ 0 < c.1 ∧ (∀ (i : Fin 4), 0 < threeAmp l c i) ∧ ∀ (i : Fin 4), ∃ (k : ℤ), threeAmp l c i = 2 ^ k

Occupied three-core bins are genuine and have nonnegative values.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeBinVal_nonneg_of_mem {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J Aw : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (xs : ℝ) (l : Fin 4) (anc : ℕ → (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)))) (Iw h : ℕ) {c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)} (hc : c ∈ Finset.image (D.threeBinOf G I xs l anc (D.toLeaf.sv l G I) h) (D.threeTested G I xs l anc (D.toLeaf.sv l G I) Iw h)) : 0 ≤ threeBinVal κ' J Aw l c

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.threeBinVal_nonneg_of_memA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J Aw : ℕ) {G : bf.Grp} {I : ℤ × ℤ} {xs : ℝ} {l : Fin 4} {anc : 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)))} {Iw h : ℕ} {ε : ℝ} {c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)} (hc : c ∈ D.threeRetBinsA G I xs l anc Iw h ε) : 0 ≤ threeBinVal κ' J Aw l c

Retained three-core bins with anchors depending on AncNe3 G I l have nonnegative values.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_principal_split {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J Aw Iw : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (y : ℝ) (l : Fin 4) (anc : ℕ → (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)))) (H : Finset ℕ) (hcard : ∀ (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 ε : ℝ} (hU0 : 0 ≤ U) (hε : 0 ≤ ε) (hU : ∀ h ∈ H, ∀ (j : Fin 4), j ≠ l → ∀ F ∈ D.goodCls G I j h, D.clsSize G I j F ≤ U) (hUs : √((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.toLeaf.sv l G I) y‖ ^ 2) ≤ U) : ∑ h ∈ H, (↑H.card)⁻¹ * ∑ c ∈ Finset.image (D.threeBinOf G I y l anc (D.toLeaf.sv l G I) h) (D.threeTested G I y l anc (D.toLeaf.sv l G I) Iw h), threeBinVal κ' J Aw l c * ↑{q ∈ D.threeTested G I y l anc (D.toLeaf.sv l G I) Iw h | D.threeBinOf G I y l anc (D.toLeaf.sv l G I) h q = c}.card ≤ ∑ h ∈ H, ∑ κ ∈ D.threeTypes l, (↑H.card)⁻¹ * ∑ c ∈ D.threeRetBins G I y l anc Iw h ε, threeBinVal κ' J Aw l c * D.threeCnt G I y l anc Iw h c κ + 8 * entryCU κ' J Aw * 2 ^ (Aw + 4) * 12 ^ 3 * ε * U ^ 3 * (D.S.Dstar ^ 3 * (↑Iw + 1))

The per-cell decomposition of eq:core-final for three cores (side role l).

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_principal_splitA {κ' : LocalKernelClass} {c₀ : ℕ} {A : ActiveSetup κ' c₀} {bf : A.BasicFamilies} {fp : bf.FamParams} (D : fp.SideInput) (hD : 2 ≤ D.S.Dstar) (J Aw Iw : ℕ) (G : bf.Grp) (I : ℤ × ℤ) (y : ℝ) (l : Fin 4) (anc : 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)))) (H : Finset ℕ) (hcard : ∀ (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 ε : ℝ} (hU0 : 0 ≤ U) (hε : 0 ≤ ε) (hU : ∀ h ∈ H, ∀ (j : Fin 4), j ≠ l → ∀ F ∈ D.goodCls G I j h, D.clsSize G I j F ≤ U) (hUs : √((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.toLeaf.sv l G I) y‖ ^ 2) ≤ U) : ∑ h ∈ H, (↑H.card)⁻¹ * D.threeBinSumA J Aw Iw G I y l anc h ≤ ∑ h ∈ H, ∑ κ ∈ D.threeTypes l, (↑H.card)⁻¹ * ∑ c ∈ D.threeRetBinsA G I y l anc Iw h ε, threeBinVal κ' J Aw l c * D.threeCntA G I y l anc Iw h c κ + 8 * entryCU κ' J Aw * 2 ^ (Aw + 4) * 12 ^ 3 * ε * U ^ 3 * (D.S.Dstar ^ 3 * (↑Iw + 1))

three_principal_split with anchors depending on a proof of AncNe3 G I l: without anchors both principal quantities vanish.

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.fourCc_nonneg {κ' : 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) (hd2 : 2 ≤ D.S.dmax) (hD : 2 ≤ D.S.Dstar) (hB : 2 ≤ D.S.Bstar) (hQ0 : 1 ≤ D.S.Q0) : 0 ≤ D.fourCc

theorem TrilinearHT.Auto.ActiveSetup.BasicFamilies.FamParams.SideInput.three_path_bin_bound {κ' : 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 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 : ℕ) (hh : 10 ≤ h) (hhJ : h ≤ D.SP.Jst) (rep : (G : bf.Grp) → (j : Fin 4) → ℕ → ℕ → ℤ × (ℤ × ℤ) × (D.Ms j G).Md → (D.Ms j G).Md) (hrep : ∀ I ∈ T, ∀ G ∈ gs I, ∀ (j : Fin 4), (D.withQ0 (qG G)).RepOK G j h T (rep 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 : ∀ (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 G j) ⋯ hF) (y : ℝ) (c : ℝ × ℝ × ℕ × ℝ × (Fin 4 → ℝ)) (hc : 0 < c.1 ∧ c.1 ≤ 1 ∧ 1 ≤ c.2.1) (hσ : ∀ (i : Fin 4), 0 < threeAmp l c i) (κ : Fin 4 → ℕ × ℕ) {K Q : ℝ} (hK : 0 ≤ K) (hQ : 0 ≤ Q) (hcap : ∀ (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)) (hcapl : ∑ 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)) : ∑ G ∈ pathGroups T gs y, ∑ s ∈ pathDepths T gs y G, (Q * threeBinVal κ' J Aw l c * (D.withQ0 (qG G)).threeCntA G (pathCell A.G T y s) y l (anc (pathCell A.G T y s) G) Iw h c κ) ^ (1 - 1 / 300 / 4) ≤ (Q * (8 * entryCU κ' J Aw * 2 ^ (Aw + 4) * 12 ^ 3)) ^ (1 - 1 / 300 / 4) * (c.1 ^ (1 - 1 / 300 / 4) * (c.2.1 ^ J)⁻¹ ^ (1 - 1 / 300 / 4)) * (D.fourCc * (1 + Real.log (8 * c.2.1 / c.1)) ^ 4 * K ^ (2 - 1 / 300 / 2))

Blueprint lines 2783-2806 at one point, height, core type tuple and three-core bin c (side role l): the powered principal quantities along the path of y sum to at most (Q C₃ μ ν^{-J})^p · C_c (1 + log(8ν/μ))⁴ · K^{2-c/2}, given the path caps of eq:top-count and the side cap at y (three_group_sum_side, three_coef_sched).