Trilinear Hilbert transform: TsideF_le

theorem TrilinearHT.Auto.TsideF_le {κ : LocalKernelClass} {c₀ : ℕ} (A : ActiveSetup κ c₀) (P K : ℕ) (u : Option (Fin 4)) (Lp Jm : ℕ) {E : ℝ} (cc : ℕ) (kk : ℝ) (Vl : Fin 4 → ℝ) {ρ V0 : ℝ} (hS : A.S = 2) (hP : 1 ≤ P) (hLp : 1 ≤ Lp) (hE : 0 ≤ E) (hVl : ∀ (l : Fin 4), 0 ≤ Vl l ∧ Vl l ≤ V0) (hρ : 0 < ρ) : TsideF A P K u Lp Jm 1 E cc kk Vl ρ ≤ 10 ^ 14 * (1 + localFormUniformConstant κ) ^ 2 * ↑Lp ^ 4 * (1 + ↑Jm) ^ 2 * (1 + ↑K) ^ 2 * (Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * kk)) ^ 2) + E + V0 + 1) / ρ

A crude polynomial bound for the side cap T_c at C_F = 1, S = 2: T_c ≤ 10¹⁴ (1 + L₀)² L_p⁴ (1 + J_m)² (1 + K)² (G₀ + E + V₀ + 1) / ρ.

theorem TrilinearHT.Auto.rpow_le_one_add {x a : ℝ} (hx : 0 ≤ x) (ha0 : 0 ≤ a) (ha1 : a ≤ 1) : x ^ a ≤ 1 + x

A power with exponent in [0, 1] of a nonnegative number is at most 1 + x.

theorem TrilinearHT.Auto.T2F_le (K : ℕ) (u : Option (Fin 4)) (cc : ℕ) (kk : ℝ) (Vl : Fin 4 → ℝ) {ρ₂ V0 : ℝ} (hVl : ∀ (l : Fin 4), 0 ≤ Vl l ∧ Vl l ≤ V0) (hρ : 0 < ρ₂) : T2F K u cc kk Vl ρ₂ ≤ 4 * (↑K * (20 * Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * kk)) ^ 2) + 32) + ↑K * V0) / ρ₂

The two-side cap at C_F = 1: T₂ ≤ 4 (K (20 G₀ + 32) + K V₀) / ρ₂.

theorem TrilinearHT.Auto.natLog_floor_le {x : ℝ} (hx : 1 ≤ x) : ↑(Nat.log 2 ⌊x⌋₊) ≤ 2 * Real.log x

log₂ of the integer part of x ≥ 1, as a natural logarithm, is at most 2 log x.

theorem TrilinearHT.Auto.card_upperHeights_le (J : ℕ) (δ : ℝ) : ↑(ModeComponents.upperHeights J δ).card ≤ ↑J + 1

The number of upper heights is at most J + 1.

theorem TrilinearHT.Auto.card_fourTypesF_le (S : ModeSchedule) {B : ℝ} (hB : 1 ≤ B) (hD1 : 1 ≤ S.Dstar) (hD : Real.log S.Dstar ≤ B) : ↑(fourTypesF S).card ≤ (3 * B) ^ 8

The number of role types is at most (3B)^8 when log D_* ≤ B, B ≥ 1.

theorem TrilinearHT.Auto.fourCcF_nonneg (S : ModeSchedule) (hD1 : 1 ≤ S.Dstar) (hH1 : 1 ≤ S.H) : 0 ≤ fourCcF S

The four-core frequency constant of a schedule with D_*, H ≥ 1 is nonnegative.

theorem TrilinearHT.Auto.fourCcF_le (S : ModeSchedule) {B : ℝ} (hB : 2 ≤ B) (hd : ↑S.dmax + 5 ≤ B) (hD1 : 1 ≤ S.Dstar) (hH1 : 1 ≤ S.H) (hD : Real.log S.Dstar ≤ B) (hH : Real.log S.H ≤ B) : fourCcF S ≤ 10 ^ 28 * B ^ 21

The four-core frequency constant of a schedule is at most 10^{28} B^{21} when d_max + 5, log D_* and log H are at most B.

noncomputable def TrilinearHT.Auto.K1c : ℝ

The constant K₁ = 2⁴/(1 - 4(2δ_*)^{1/4}) at δ_* = 1/1024.

Equations

• TrilinearHT.Auto.K1c = 2 ^ 4 / (1 - 4 * (2 * (1 / 1024)) ^ (1 / 4))

theorem TrilinearHT.Auto.K1c_pos : 0 < K1c

noncomputable def TrilinearHT.Auto.C4c (κ : LocalKernelClass) : ℝ

The constant of the four-core bound coreM4F.

Equations

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

noncomputable def TrilinearHT.Auto.C3c (κ : LocalKernelClass) : ℝ

The constant of the three-core bound coreM3F.

Equations

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

theorem TrilinearHT.Auto.bandC_nonneg' (p : ℝ) (J : ℕ) : 0 ≤ ActiveSetup.BasicFamilies.FamParams.SideInput.bandC p J

theorem TrilinearHT.Auto.C4c_nonneg (κ : LocalKernelClass) : 0 ≤ C4c κ

theorem TrilinearHT.Auto.C3c_nonneg (κ : LocalKernelClass) : 0 ≤ C3c κ

theorem TrilinearHT.Auto.coreM4F_le (κ : LocalKernelClass) (S : ModeSchedule) {B L U ε Kc : ℝ} (hB : 2 ≤ B) (hd : ↑S.dmax + 5 ≤ B) (hD1 : 1 ≤ S.Dstar) (hH1 : 1 ≤ S.H) (hD : Real.log S.Dstar ≤ B) (hH : Real.log S.H ≤ B) (hJ : ↑S.Jstar + 1 ≤ B) (hL0 : 0 ≤ Real.logb 2 (U / ε) + 1) (hL : Real.logb 2 (U / ε) + 1 ≤ L) (hKc : 1 ≤ Kc) : coreM4F κ S (1 / 1024) 3 U ε Kc ≤ C4c κ * B ^ 30 * L ^ 4 * Kc ^ 2

The four-core bound at δ_* = 1/1024, J = 3: M₄ ≤ C B^{30} L⁴ K² when J_* + 1, d_max + 5, log D_*, log H are at most B and log₂(U/ε) + 1 ≤ L.

theorem TrilinearHT.Auto.coreM3F_le (κ : LocalKernelClass) (S : ModeSchedule) (Iw : ℕ) (l : Fin 4) {B L U ε Kc IB : ℝ} (hB : 2 ≤ B) (hd : ↑S.dmax + 5 ≤ B) (hD1 : 1 ≤ S.Dstar) (hH1 : 1 ≤ S.H) (hD : Real.log S.Dstar ≤ B) (hH : Real.log S.H ≤ B) (hJ : ↑S.Jstar + 1 ≤ B) (hL0 : 0 ≤ Real.logb 2 (U / ε) + 1) (hL : Real.logb 2 (U / ε) + 1 ≤ L) (hKc : 1 ≤ Kc) (hI : ↑Iw + 1 ≤ IB) : coreM3F κ S (1 / 1024) 3 1 Iw U ε Kc l ≤ C3c κ * B ^ 30 * IB * L ^ 4 * Kc ^ 2

The three-core bound at δ_* = 1/1024, J = 3, A = 1: M₃ ≤ C B^{30} I L⁴ K² when moreover I_w + 1 ≤ I.

theorem TrilinearHT.Auto.nearBndF_le (κ : LocalKernelClass) {c₀ : ℕ} (A : ActiveSetup κ c₀) {q : ℝ} (hq2 : 2 < q) (hq3 : q < 3) (P K : ℕ) (u : Option (Fin 4)) (Nd N Lp Jm : ℕ) {Mp C₀ ρ : ℝ} (Γa Γb : Fin 4 → ℝ) (ΓU : ℝ) (a b e : Fin 4) {Γ : ℝ} (hMp : 0 ≤ Mp) (hC₀ : 0 ≤ C₀) (hρ : 0 < ρ) (hρ1 : ρ < 1) (hΓa : ∀ (a : Fin 4), 0 ≤ Γa a ∧ Γa a ≤ Γ) (hΓb : ∀ (b : Fin 4), 0 ≤ Γb b ∧ Γb b ≤ Γ) (hΓU : 0 ≤ ΓU ∧ ΓU ≤ Γ) : nearBndF κ A hq2 hq3 P K u Nd N Lp Jm Mp C₀ ρ Γa Γb ΓU a b e ≤ 4 * ((nbCM κ hq2 hq3 + nbCUM κ hq2 hq3) * (1 + finiteDepthConstant κ q Nd) * (1 + Real.log (↑K + 2)) * (↑K + 2) ^ (2 * (q - 2) / (q - 1)) * (64 * (2 * C₀) * (2 * C₀))) * (hullCutConstant (ρ / 2) * ↑(N + 1) * (1 + Real.log (2 + ↑(N + 1) * ↑(N + 1) * (↑(ActiveSetup.BasicFamilies.FamParams.SideLeafM.nOs Lp Jm).card * Mp * ↑A.famVtxBound)))) * Γ / √↑P * dyadicGridLength A.G A.R.1

The near-band bound of a leaf with stack energies at most Γ (Γ_a, Γ_b, Γ_U ≤ Γ).

theorem TrilinearHT.Auto.leaf_raw_le {T cB eB Np τ fc η R nearS M Ee cM4 cM3 cE L0 B η₀ τ₃ P tT tC tM XE : ℝ} (hT0 : 0 ≤ T) (hT : T ≤ tT) (hcB0 : 0 ≤ cB) (hcB : cB ≤ tC) (heB0 : 0 ≤ eB) (heB : eB ≤ tC) (hNp : Np ≤ B ^ 2) (hτ0 : 0 ≤ τ) (hτ : τ ≤ 2 * η₀) (hfc0 : 0 ≤ fc) (hfc : fc ≤ 64 * B * (P + 1) ^ 2 * τ₃) (hη0 : 0 ≤ η) (hR : 0 ≤ R) (hL0 : 0 ≤ L0) (hB : 1 ≤ B) (hη₀ : 0 ≤ η₀) (hτ₃ : 0 ≤ τ₃) (hME : √(4 * M) * √Ee ≤ XE) (htM0 : 0 ≤ tM) (hcM : cM4 + cM3 ≤ tM) : 6 * 256 * Np * (τ + fc) * T * R + 6 * nearS + η ^ (1 - (1 - 1 / 1200)) * (T ^ ((1 - 1 / 1200) / 2) * T ^ ((1 - 1 / 1200) / 2) * T ^ ((1 - 1 / 1200) / 2) * R) + 82 * (81 * (L0 * (cB + eB + √T) ^ 3) * (√(4 * M) * √Ee)) + 82 * (η ^ (1 - (1 - 1 / 1200)) * (81 * L0 * max cB √T) ^ (1 - 1 / 1200) * (T ^ ((1 - 1 / 1200) / 2) * T ^ ((1 - 1 / 1200) / 2) * T ^ ((1 - 1 / 1200) / 2) * R)) + (η ^ (1 / 1200) * (R * (cM4 + cM3)) + cE) ≤ (196608 * B ^ 3 * tT + 83 * (1 + 81 * L0 * (tC + √tT)) * (1 + tT) ^ 3 + tM) * (η ^ (1 / 1200) + η₀ + (P + 1) ^ 2 * τ₃) * R + 6 * nearS + 6642 * L0 * (2 * tC + √tT) ^ 3 * XE + cE

The arithmetic collapse of the right side of leaf_bound at p = 1 - 1/1200: the side cap T ≤ t_T, the core and error sizes ≤ t_C, the path count N_p ≤ B², the far constant ≤ 64 B (P+1)² τ₃, the core bounds ≤ t_M and the error product ≤ X_E give (196608 B³ t_T + 83 (1 + 81 L₀ (t_C + √t_T)) (1 + t_T)³ + t_M) (η^{1/1200} + η₀ + (P+1)² τ₃) |R| plus the near bands and the absolute errors.

theorem TrilinearHT.Auto.near_lambda_le (K : ℕ) (hK : 1 ≤ K) {Y : ℝ} (hY : 0 ≤ Y) : (1 + Real.log (↑K + 2)) * ↑(Nat.log 2 K + 1 + 1) * (1 + Real.log (2 + ↑(Nat.log 2 K + 1 + 1) * ↑(Nat.log 2 K + 1 + 1) * Y)) * ↑(Nat.log 2 K + 1) ^ 3 ≤ 80 * (2 + Real.log (↑K + 2)) ^ 6 * (1 + Real.log (2 + Y))

The polylogarithmic factors of the near bands at block length K ≥ 1 with N = ⌊log₂ K⌋ + 1: (1 + log(K+2)) (N+1) (1 + log(2 + (N+1)² Y)) N³ ≤ 80 λ⁶ (1 + log(2 + Y)), λ = 2 + log(K + 2).

theorem TrilinearHT.Auto.one_add_log_two_mul_sq_le {k : ℝ} (hk : 1 ≤ k) : (1 + Real.log (2 * k)) ^ 2 ≤ 4 * k

(1 + log 2k)² ≤ 4k for k ≥ 1.

theorem TrilinearHT.Auto.le_exp_one_add_log_sq {k : ℝ} (hk : 1 ≤ k) : k ≤ Real.exp ((1 + Real.log (2 * k)) ^ 2)

k ≤ exp((1 + log 2k)²) for k ≥ 1.

theorem TrilinearHT.Auto.two_pow_le_of_fuel {n c : ℕ} {k : ℝ} (hk : 1 ≤ k) (h : ↑(2 * n + 2) ≤ ↑c * (Real.log k + 1)) : 2 ^ n ≤ (3 * k) ^ c

The fuel bound 2 n + 2 ≤ c (log k + 1) gives 2^n ≤ (3k)^c.

noncomputable def TrilinearHT.Auto.leafBnd (Cl : ℕ) (kD : ℝ) (P k cc : ℕ) (η η₀ τ₃ δ CN Cq q R : ℝ) : ℝ

The explicit leaf bound of leaf_estimate (the form of eq:before-absorption on one leaf): C u^C G^C (η^{1/1200} + η₀ + (P+1)² τ₃ + e^{C k^c} (√δ + e^{-k_D})) |R| + C e^{-k} |R| plus the near-band term C (1 + C_N) C_q (C u^C + 2)^{2(q-2)/(q-1)} (2 + log(C u^C + 2))⁶ G^C P^{-1/2} |R|, with u = k_D P and G = exp((1 + log 2k)²).

Equations

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

Steps of leaf_final. Each lemma below is one step of that proof, stated over the hypotheses and local definitions (as lets) of the proof that it uses, so that it is elaborated in a small local context instead of the long context of the whole proof.

theorem TrilinearHT.Auto.leaf_final_hKB (Msch : ℝ) : 0 < Msch → ∀ (CΛ eΛ Cb : ℕ) (S : ModeSchedule) (Λ : ℝ), 0 ≤ Λ → ↑S.K ≤ Msch * Λ ^ 16 → 16 * eΛ ≤ Cb → (⌈Msch⌉₊ + 1) * CΛ ^ 16 ≤ Cb → ∀ (u : ℝ), Λ ≤ ↑CΛ * u ^ eΛ → 1 ≤ u → ∀ (B : ℝ), (∀ (c : ℝ) (e : ℕ), 0 ≤ c → c ≤ ↑Cb → e ≤ Cb → c * u ^ e ≤ B) → Msch ≤ ↑(⌈Msch⌉₊ + 1) → 1 ≤ ↑CΛ → ↑S.K ≤ B

Step hKB of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hHB (Msch : ℝ) : 0 < Msch → ∀ (CΛ eΛ Cb : ℕ) (S : ModeSchedule) (Λ : ℝ), 0 ≤ Λ → Real.log S.H ≤ Msch * Λ ^ 12 → 16 * eΛ ≤ Cb → (⌈Msch⌉₊ + 1) * CΛ ^ 16 + 1 ≤ Cb → ∀ (u : ℝ), Λ ≤ ↑CΛ * u ^ eΛ → 1 ≤ u → ∀ (B : ℝ), (∀ (c : ℝ) (e : ℕ), 0 ≤ c → c ≤ ↑Cb → e ≤ Cb → c * u ^ e ≤ B) → 1 ≤ ↑CΛ → Real.log S.H + 1 ≤ B

Step hHB of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hIwB (Cg Cb : ℕ) (S : ModeSchedule) (Iw : ℕ) : Iw = ⌊Real.logb 2 (S.Dstar ^ 250)⌋₊ → 500 * Cg + 1 ≤ Cb → ∀ (u : ℝ), Real.log S.Dstar ≤ ↑Cg * u ^ Cg → 1 ≤ u → ∀ (B : ℝ), (∀ (c : ℝ) (e : ℕ), 0 ≤ c → c ≤ ↑Cb → e ≤ Cb → c * u ^ e ≤ B) → 1 ≤ S.Dstar → 0 ≤ Real.log S.Dstar → ↑Iw + 1 ≤ B

Step hIwB of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hJmB (Cb k cc : ℕ) : 1 ≤ cc → ∀ (famFuel : ℕ), ↑(2 * famFuel + 2) ≤ ↑cc * (Real.log ↑k + 1) → 1 ≤ ↑k → cc + 1 ≤ Cb → ↑k ≤ ↑k ^ cc → ∀ (B : ℝ), (∀ (c : ℝ), 0 ≤ c → c ≤ ↑Cb → c * ↑k ^ cc ≤ B) → 1 ≤ ↑k ^ cc → ↑(2 * famFuel + 2) + 1 ≤ B

Step hJmB of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hVl0B (k cc : ℕ) (S : ModeSchedule) (Vl0 : ℝ) : Vl0 = 24 * (↑⌊180 * ↑S.dmax * Real.log (2 * S.Dm) / (1 / 1024)⌋₊ + 1) * (Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * ↑k)) ^ 2) + 2 * 1 / S.Dstar ^ 394) → ∀ (B : ℝ), 1 ≤ B → ∀ (G : ℝ), 1 ≤ G → Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * ↑k)) ^ 2) ≤ G → 1 ≤ S.Dstar → 2 ≤ S.Dm → ↑S.dmax + 5 ≤ B → Real.log (2 * S.Dm) ≤ B → Vl0 ≤ 14000000 * B ^ 2 * G

Step hVl0B of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hT (κ : LocalKernelClass) (cT : ℝ) (k cc famFuel : ℕ) (E ρ : ℝ) : 0 ≤ E → 0 < ρ → ∀ (S : ModeSchedule), 1 ≤ S.K → ∀ (Vl0 TT : ℝ), TT ≤ 10 ^ 14 * (1 + localFormUniformConstant κ) ^ 2 * ↑(2 ^ famFuel) ^ 4 * (1 + ↑(2 * famFuel + 2)) ^ 2 * (1 + ↑S.K) ^ 2 * (Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2) + E + Vl0 + 1) / ρ → cT = 10 ^ 22 * (1 + localFormUniformConstant κ) ^ 2 → ∀ (B : ℝ), 2 ≤ B → 1 ≤ B → ∀ (G : ℝ), 1 ≤ G → Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2) ≤ G → ↑S.K ≤ B → E ≤ B → ρ⁻¹ ≤ B → ↑(2 ^ famFuel) ≤ B → ↑(2 * famFuel + 2) + 1 ≤ B → 0 ≤ Vl0 → Vl0 ≤ 14000000 * B ^ 2 * G → TT ≤ cT * B ^ 11 * G

Step hT of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hT2 (k cc : ℕ) (ρ : ℝ) : 0 < ρ → ∀ (S : ModeSchedule) (Vl0 T2v : ℝ), T2v ≤ 4 * (↑S.K * (20 * Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2) + 32) + ↑S.K * Vl0) / ρ → ∀ (B : ℝ), 2 ≤ B → 1 ≤ B → ∀ (G : ℝ), 1 ≤ G → Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2) ≤ G → ↑S.K ≤ B → 0 ≤ Vl0 → Vl0 ≤ 14000000 * B ^ 2 * G → 1 / ρ ≤ B → T2v ≤ 60000000 * B ^ 4 * G

Step hT2 of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hsT2 (T2v B G : ℝ) : 1 ≤ G → T2v ≤ 60000000 * B ^ 4 * G → √T2v ≤ 7746 * B ^ 2 * G

Step hsT2 of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hlogU (g : ℕ) (cT : ℝ) (Cb k cc : ℕ) (cb : ℝ) : 2 ≤ cb → Real.log (2 * cb) ≤ ↑k ^ cc → ∀ (S : ModeSchedule), 2 ≤ S.Dstar → ∀ (TT : ℝ), 0 ≤ TT → ∀ (U : ℝ), U = max (2 * (cb + 2) * S.Dstar ^ 2) √TT → ∀ (B : ℝ), 20 ≤ ↑Cb → 2 ≤ B → 1 ≤ B → (∀ (c : ℝ), 0 ≤ c → c ≤ ↑Cb → c * ↑k ^ cc ≤ B) → ∀ (X : ℝ), 0 ≤ X → X ≤ 4 * ↑k → ∀ (G : ℝ), G = Real.exp (↑g * X) → 1 ≤ G → 1 ≤ S.Dstar → Real.log S.Dstar ≤ B → ↑k ≤ B → 0 < U → TT ≤ cT * B ^ 11 * G → 1 ≤ cT → 1 ≤ cT * B ^ 11 * G → Real.log U ≤ (17 + 4 * ↑g + Real.log cT) * B

Step hlogU of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hlogMV (Cb k cc Mp V : ℕ) (MV : ℝ) : MV = ↑Mp * ↑V → ∀ (B : ℝ), 20 ≤ ↑Cb → 1 ≤ B → (∀ (c : ℝ), 0 ≤ c → c ≤ ↑Cb → c * ↑k ^ cc ≤ B) → ↑Mp ≤ Real.exp (↑k ^ cc) → ↑V ≤ 5 * Real.exp (↑k ^ cc) → 0 ≤ MV → Real.log (1 + MV) ≤ 4 * B

Step hlogMV of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hlogUε (g : ℕ) (cT : ℝ) (k : ℕ) (S : ModeSchedule) : 2 ≤ S.Dstar → ∀ (U MV ε B : ℝ), 2 ≤ B → 1 ≤ B → Real.log S.Dstar ≤ B → ↑k ≤ B → 16 ≤ U → 0 ≤ MV → 1 ≤ cT → U / ε = U ^ 4 * S.Dstar ^ 5 * Real.exp ↑k * (1 + MV) → Real.log U ≤ (17 + 4 * ↑g + Real.log cT) * B → Real.log (1 + MV) ≤ 4 * B → Real.log (U / ε) ≤ (78 + 16 * ↑g + 4 * Real.log cT) * B

Step hlogUε of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hcL0 (g : ℕ) (cT cL : ℝ) : cL = 159 + 32 * ↑g + 8 * Real.log cT → 1 ≤ cT → 0 ≤ cL

Step hcL0 of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hMtB (cL : ℝ) (k cc : ℕ) (ρ : ℝ) : 0 < ρ → ∀ (S : ModeSchedule) (Vl0 U ε Mt B : ℝ), 1 ≤ B → ∀ (G : ℝ), 1 ≤ G → ↑S.K ≤ B → ↑S.Jstar + 1 ≤ B → 0 ≤ Vl0 → Vl0 ≤ 14000000 * B ^ 2 * G → 1 / ρ ≤ B → 0 ≤ cL → have Gq := Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * ↑k)) ^ 2); Gq ≤ G → have Ts := Finset.range (Nat.log 2 ⌊S.Dstar⌋₊ + 1) ×ˢ Finset.range (Nat.log 2 ⌊S.Dstar⌋₊ + 1); Mt = 24 * (2 * Gq + 2 * ↑S.K * Vl0) * ↑(Finset.range (S.Jstar + 1) ×ˢ Ts ×ˢ dyThr ε U S.Dstar).card / ρ → ↑Ts.card ≤ (3 * B) ^ 2 → ↑(dyThr ε U S.Dstar).card ≤ cL * B + 2 → Mt ≤ 7000000000 * B ^ 7 * G * (cL * B + 2)

Step hMtB of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hKcB (cT cL cK TT : ℝ) : 0 ≤ TT → ∀ (Mt : ℝ), cK = (1 + 7 * 10 ^ 9 + cT) * (cL + 2) → ∀ (B : ℝ), 1 ≤ B → ∀ (G : ℝ), 1 ≤ G → TT ≤ cT * B ^ 11 * G → 1 ≤ cT → 0 ≤ cL → Mt ≤ 7000000000 * B ^ 7 * G * (cL * B + 2) → 0 ≤ Mt → have Kc := max (max 1 Mt) TT; Kc ≤ cK * B ^ 12 * G

Step hKcB of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hcMtot (κ : LocalKernelClass) (cL cK cMc TT Mt cM4 cM3 : ℝ) : cMc = (C4c κ + 4 * C3c κ) * cL ^ 4 * cK ^ 2 → ∀ (B : ℝ), 1 ≤ B → ∀ (G : ℝ), have Kc := max (max 1 Mt) TT; 1 ≤ Kc → Kc ≤ cK * B ^ 12 * G → cM4 ≤ C4c κ * B ^ 30 * (cL * B) ^ 4 * Kc ^ 2 → cM3 ≤ 4 * (C3c κ * B ^ 30 * B * (cL * B) ^ 4 * Kc ^ 2) → cM4 + cM3 ≤ cMc * B ^ 59 * G ^ 2

Step hcMtot of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hME (κ : LocalKernelClass) (k cc : ℕ) (cb Nl : ℝ) (Mp V : ℕ) : 2 ≤ cb → 4 ≤ Nl → ∀ (dB : ℕ), 1 ≤ dB → ∀ (δ R : ℝ), 0 < δ → δ ≤ 1 / 8 → 0 < R → ∀ (S : ModeSchedule) (Iw : ℕ) (U ε cE : ℝ), cE ≤ (16 * fourErrC κ 3 * ((S.Dstar ^ 100)⁻¹ * S.Dstar ^ 10) + K1c * (2 * fourKC κ 3 * 12 ^ 4 * ε * U ^ 3 * S.Dstar ^ 4) + 4 * (81 * threeErrC κ 3 1 * ((S.Dstar ^ 100)⁻¹ * S.Dstar ^ 10) * U + K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3 * ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1))))) * (↑(Mp * V) * R) → ∀ (Ee : ℝ), 0 ≤ Ee → Ee ≤ (8 * ↑dB * δ + 2 * δ ^ 2) * (4 * Nl * cb ^ 2 * 1) * ↑(4 * (Mp * V)) * R → 0 ≤ Nl → ∀ (E1 : ℝ), E1 = Real.exp (↑k ^ cc) → 1 ≤ E1 → ↑Mp ≤ E1 → ↑V ≤ 5 * E1 → cb ≤ E1 → Nl ≤ E1 → ↑dB ≤ E1 → √(4 * (↑(Mp * V) * R)) * √Ee ≤ 288 * Real.exp (4 * ↑k ^ cc) * √δ * R

Step hME of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hQe0 (κ : LocalKernelClass) (S : ModeSchedule) : 2 ≤ S.Dstar → ∀ (Iw : ℕ) (U ε : ℝ), 16 ≤ U → 0 < ε → ∀ (ι : ℝ), 0 ≤ ι → have Qe := 16 * fourErrC κ 3 * ι + K1c * (2 * fourKC κ 3 * 12 ^ 4 * ε * U ^ 3 * S.Dstar ^ 4) + 4 * (81 * threeErrC κ 3 1 * ι * U + K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3 * ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1)))); Qe = 16 * fourErrC κ 3 * ι + K1c * (2 * fourKC κ 3 * 12 ^ 4 * ε * U ^ 3 * S.Dstar ^ 4) + 4 * (81 * threeErrC κ 3 1 * ι * U + K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3 * ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1)))) → 0 ≤ Qe

Step hQe0 of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hε4 (k : ℕ) (S : ModeSchedule) : 2 ≤ S.Dstar → ∀ (U MV ε : ℝ), ε = (U ^ 3 * S.Dstar ^ 5 * Real.exp ↑k * (1 + MV))⁻¹ → 1 ≤ S.Dstar → 16 ≤ U → 0 ≤ MV → ε * U ^ 3 * S.Dstar ^ 4 * MV ≤ Real.exp (-↑k)

Step hε4 of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hε3 (k : ℕ) (S : ModeSchedule) : 2 ≤ S.Dstar → ∀ (Iw : ℕ) (U MV ε : ℝ), ε = (U ^ 3 * S.Dstar ^ 5 * Real.exp ↑k * (1 + MV))⁻¹ → 16 ≤ U → 0 ≤ MV → ↑Iw + 1 ≤ 501 * S.Dstar ^ 2 → ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1)) * MV ≤ 501 * Real.exp (-↑k)

Step hε3 of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hE14 (k cc : ℕ) : 1 ≤ cc → 2 ≤ ↑k → 1 ≤ ↑k → ∀ (E1 : ℝ), E1 = Real.exp (↑k ^ cc) → 4 ≤ E1

Step hE14 of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hιU (cb : ℝ) : 2 ≤ cb → ∀ (S : ModeSchedule) (TT U : ℝ), U = max (2 * (cb + 2) * S.Dstar ^ 2) √TT → ∀ (ι : ℝ), 0 ≤ ι → ι ≤ S.Dstar⁻¹ → ι * S.Dstar ^ 2 ≤ S.Dstar⁻¹ → ι * U ≤ S.Dstar⁻¹ * (2 * (cb + 2) + √TT)

Step hιU of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hsTT (cT TT B : ℝ) : 1 ≤ B → ∀ (G : ℝ), 1 ≤ G → TT ≤ cT * B ^ 11 * G → 1 ≤ cT → √TT ≤ √cT * B ^ 6 * G

Step hsTT of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hQeMV (κ : LocalKernelClass) (cT ce2 : ℝ) (k cc : ℕ) (kD cb : ℝ) : 2 ≤ cb → ∀ (S : ModeSchedule) (Iw : ℕ) (TT U MV ε : ℝ), ce2 = K1c * (2 * fourKC κ 3 * 12 ^ 4) + 4 * (K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3)) * 501 → ∀ (B : ℝ), 2 ≤ B → 1 ≤ B → ∀ (G : ℝ), 1 ≤ G → 2 * cb ≤ Real.exp (↑k ^ cc) → 0 ≤ MV → ∀ (E1 : ℝ), E1 = Real.exp (↑k ^ cc) → 1 ≤ E1 → cb ≤ E1 → S.Dstar⁻¹ ≤ Real.exp (-kD) → ∀ ι ≤ S.Dstar⁻¹, have Qe := 16 * fourErrC κ 3 * ι + K1c * (2 * fourKC κ 3 * 12 ^ 4 * ε * U ^ 3 * S.Dstar ^ 4) + 4 * (81 * threeErrC κ 3 1 * ι * U + K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3 * ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1)))); Qe = 16 * fourErrC κ 3 * ι + K1c * (2 * fourKC κ 3 * 12 ^ 4 * ε * U ^ 3 * S.Dstar ^ 4) + 4 * (81 * threeErrC κ 3 1 * ι * U + K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3 * ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1)))) → MV ≤ 5 * E1 ^ 2 → ε * U ^ 3 * S.Dstar ^ 4 * MV ≤ Real.exp (-↑k) → ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1)) * MV ≤ 501 * Real.exp (-↑k) → 4 ≤ E1 → ι * U ≤ S.Dstar⁻¹ * (2 * (cb + 2) + √TT) → √TT ≤ √cT * B ^ 6 * G → Qe * MV ≤ 5 * (16 * fourErrC κ 3 + 648 * threeErrC κ 3 1 + 324 * threeErrC κ 3 1 * √cT) * Real.exp (3 * ↑k ^ cc) * B ^ 6 * G * Real.exp (-kD) + ce2 * Real.exp (-↑k)

Step hQeMV of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hcMcn (κ : LocalKernelClass) (cL cK cMc : ℝ) : cMc = (C4c κ + 4 * C3c κ) * cL ^ 4 * cK ^ 2 → 0 ≤ cMc

Step hcMcn of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hCjg1 (k cc famFuel : ℕ) : have Cjg := (↑(2 * famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)); Cjg = (↑(2 * famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)) → 1 ≤ Cjg

Step hCjg1 of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hOsk (k cc famFuel : ℕ) (Os : Finset (Fin 4 × Fin 4 × ℕ × ℕ × ℕ × ℕ)) : Os = ActiveSetup.BasicFamilies.FamParams.SideLeafM.nOs (2 ^ famFuel) (2 * famFuel + 2) → ↑(2 * famFuel + 2) ≤ ↑cc * ↑k → 2 ^ famFuel ≤ 3 ^ cc * ↑k ^ cc → ↑Os.card ≤ 80 * 9 ^ cc * ↑cc * ↑k ^ (2 * cc + 1)

Step hOsk of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hhull (k cc : ℕ) : 2 ≤ ↑k → ∀ (ρ : ℝ), 0 < ρ → ρ⁻¹ ≤ ↑k ^ cc → hullCutConstant (ρ / 64 / 2) ≤ 65536 * ↑k ^ (2 * cc)

Step hhull of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hlogY (k cc Mp V : ℕ) (Os : Finset (Fin 4 × Fin 4 × ℕ × ℕ × ℕ × ℕ)) (E1 : ℝ) : E1 = Real.exp (↑k ^ cc) → 1 ≤ E1 → ↑Mp ≤ E1 → ↑V ≤ 5 * E1 → ↑k ^ cc ≤ ↑k ^ (2 * cc + 1) → 1 ≤ ↑k ^ (2 * cc + 1) → ↑Os.card ≤ 80 * 9 ^ cc * ↑cc * ↑k ^ (2 * cc + 1) → 0 ≤ ↑Os.card → have Yn := ↑Os.card * ↑Mp * ↑V; Yn = ↑Os.card * ↑Mp * ↑V → 0 ≤ Yn → 1 + Real.log (2 + Yn) ≤ (8 + 80 * 9 ^ cc * ↑cc) * ↑k ^ (2 * cc + 1)

Step hlogY of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hCjgk (g k cc famFuel : ℕ) : 1 ≤ ↑k → ↑g = 8192 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 8 → ∀ (X : ℝ), X = (1 + Real.log (2 * ↑k)) ^ 2 → ∀ (G : ℝ), (∀ c ≤ ↑g, Real.exp (c * X) ≤ G) → have Cjg := (↑(2 * famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)); Cjg = (↑(2 * famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)) → ↑(2 * famFuel + 2) ≤ ↑cc * ↑k → 1 ≤ ↑cc → Cjg ≤ 4 * ↑cc ^ 2 * ↑k ^ 2 * G

Step hCjgk of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hWk (k cc : ℕ) (Nl : ℝ) (dB : ℕ) : ↑dB ≤ ↑k ^ cc → ∀ E ≤ ↑k ^ cc, ∀ (S : ModeSchedule), S.dmax = 2 * dB + 2 → S.Dm = max 2 Nl → ∀ (Vl0 : ℝ), 1 ≤ ↑k → ∀ (G : ℝ), 1 ≤ G → 1 ≤ ↑k ^ cc → 1 ≤ S.Dstar → Real.log (max 2 Nl) ≤ ↑k ^ cc → 2 ≤ S.Dm → have Gq := Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * ↑k)) ^ 2); Gq ≤ G → Vl0 = 24 * (↑⌊180 * ↑S.dmax * Real.log (2 * S.Dm) / (1 / 1024)⌋₊ + 1) * (Gq + 2 * 1 / S.Dstar ^ 394) → Gq = Real.exp ((6144 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + 4) * (1 + Real.log (2 * ↑k)) ^ 2) → have G0e := Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2); G0e ≤ G → have W := G0e + Vl0 + E + 1; W = G0e + Vl0 + E + 1 → W ≤ 170000000 * ↑k ^ (2 * cc) * G

Step hWk of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hQk (g : ℕ) (cQ : ℝ) (k cc : ℕ) : 1 ≤ cc → 2 ≤ ↑k → ∀ (Mp V famFuel : ℕ) (E ρ : ℝ), 0 < ρ → ρ < 1 → ∀ (Vl0 : ℝ) (Os : Finset (Fin 4 × Fin 4 × ℕ × ℕ × ℕ × ℕ)), cQ = 65536 * (8 + 80 * 9 ^ cc * ↑cc) * (80 * 9 ^ cc * ↑cc) * (4 * ↑cc ^ 2) * (17 * 10 ^ 7) → 1 ≤ ↑k → ∀ (X : ℝ), X = (1 + Real.log (2 * ↑k)) ^ 2 → ∀ (G : ℝ), G = Real.exp (↑g * X) → 1 ≤ G → have Cjg := (↑(2 * famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)); 1 ≤ Cjg → have G0e := Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2); have W := G0e + Vl0 + E + 1; 1 ≤ W → ↑Os.card ≤ 80 * 9 ^ cc * ↑cc * ↑k ^ (2 * cc + 1) → hullCutConstant (ρ / 64 / 2) ≤ 65536 * ↑k ^ (2 * cc) → have Yn := ↑Os.card * ↑Mp * ↑V; 0 ≤ Yn → 1 + Real.log (2 + Yn) ≤ (8 + 80 * 9 ^ cc * ↑cc) * ↑k ^ (2 * cc + 1) → Cjg ≤ 4 * ↑cc ^ 2 * ↑k ^ 2 * G → W ≤ 170000000 * ↑k ^ (2 * cc) * G → have Qk := hullCutConstant (ρ / 64 / 2) * (1 + Real.log (2 + Yn)) * ↑Os.card * Cjg * W; Qk = hullCutConstant (ρ / 64 / 2) * (1 + Real.log (2 + Yn)) * ↑Os.card * Cjg * W → 0 ≤ cQ → Qk ≤ cQ * Real.exp X ^ (8 * cc + 4 + 2 * g)

Step hQk of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hcore (k cc Mp V famFuel : ℕ) (E ρ : ℝ) (S : ModeSchedule) (Vl0 Γ : ℝ) (Os : Finset (Fin 4 × Fin 4 × ℕ × ℕ × ℕ × ℕ)) : have Nb := Nat.log 2 S.K + 1; have n := ↑Nb; have Cjg := (↑(2 * famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)); 1 ≤ Cjg → have G0e := Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2); have W := G0e + Vl0 + E + 1; Γ ≤ 2000 * ↑Os.card * (n ^ 3 * Cjg) * W → 1 ≤ W → have Yn := ↑Os.card * ↑Mp * ↑V; have Qk := hullCutConstant (ρ / 64 / 2) * (1 + Real.log (2 + Yn)) * ↑Os.card * Cjg * W; Qk = hullCutConstant (ρ / 64 / 2) * (1 + Real.log (2 + Yn)) * ↑Os.card * Cjg * W → (1 + Real.log (↑S.K + 2)) * ↑(Nb + 1) * (1 + Real.log (2 + ↑(Nb + 1) * ↑(Nb + 1) * Yn)) * ↑Nb ^ 3 ≤ 80 * (2 + Real.log (↑S.K + 2)) ^ 6 * (1 + Real.log (2 + Yn)) → 0 ≤ hullCutConstant (ρ / 64 / 2) → 0 ≤ 1 + Real.log (↑S.K + 2) → 0 ≤ ↑(Nb + 1) → 0 ≤ 1 + Real.log (2 + ↑(Nb + 1) * ↑(Nb + 1) * Yn) → (1 + Real.log (↑S.K + 2)) * ↑(Nb + 1) * (1 + Real.log (2 + ↑(Nb + 1) * ↑(Nb + 1) * Yn)) * Γ * hullCutConstant (ρ / 64 / 2) ≤ 160000 * (2 + Real.log (↑S.K + 2)) ^ 6 * Qk

Step hcore of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hNEAR (κ : LocalKernelClass) (q : ℝ) (hq2 : 2 < q) (hq3 : q < 3) (Nd : ℕ) (Msch : ℝ) (g : ℕ) (cm ce ce2 cQ : ℝ) (CΛ Cb Cl k cc : ℕ) : 1 ≤ cc → ∀ (P Mp V famFuel : ℕ) (E ρ R : ℝ) (S : ModeSchedule) (Vl0 nearS Γ : ℝ) (Os : Finset (Fin 4 × Fin 4 × ℕ × ℕ × ℕ × ℕ)), 0 ≤ R → 20 ≤ Cb → (⌈Msch⌉₊ + 1) * CΛ ^ 16 + 1 ≤ Cb → ⌈cm * ↑Cb ^ 59 + ce * ↑Cb ^ 18 + ce2 + 3 * 10 ^ 11 * cQ⌉₊ + 59 * Cb + 4 * g + 8 * cc + 8 ≤ Cl → ∀ (u : ℝ), 1 ≤ u → ∀ (X : ℝ), 0 ≤ X → 0 ≤ cm → 0 ≤ ce → 0 ≤ ce2 → have Nb := Nat.log 2 S.K + 1; have Cjg := (↑(2 * famFuel + 2) + 1) ^ 2 * Real.exp (2 * (1024 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) * (1 + Real.log (2 * ↑k)) ^ 2)); 1 ≤ Cjg → have G0e := Real.exp ((4096 * (↑cc + 1) * (1024 * (↑cc + 1) + ↑cc + 7) + ↑cc ^ 2 + 3) * (1 + Real.log (2 * ↑k)) ^ 2); have W := G0e + Vl0 + E + 1; 1 ≤ W → have Yn := ↑Os.card * ↑Mp * ↑V; 0 ≤ Yn → have Qk := hullCutConstant (ρ / 64 / 2) * (1 + Real.log (2 + Yn)) * ↑Os.card * Cjg * W; Qk = hullCutConstant (ρ / 64 / 2) * (1 + Real.log (2 + Yn)) * ↑Os.card * Cjg * W → 0 ≤ cQ → Qk ≤ cQ * Real.exp X ^ (8 * cc + 4 + 2 * g) → have eq' := 2 * (q - 2) / (q - 1); nearS ≤ 64 * (4 * ((nbCM κ hq2 hq3 + nbCUM κ hq2 hq3) * (1 + finiteDepthConstant κ q Nd) * (1 + Real.log (↑S.K + 2)) * (↑S.K + 2) ^ eq' * (64 * (2 * (2 * √1)) * (2 * (2 * √1)))) * (hullCutConstant (ρ / 64 / 2) * ↑(Nb + 1) * (1 + Real.log (2 + ↑(Nb + 1) * ↑(Nb + 1) * Yn))) * Γ / √↑P * R) → have Kb := ↑Cl * u ^ Cl; (↑S.K + 2) ^ eq' ≤ (Kb + 2) ^ eq' → (2 + Real.log (↑S.K + 2)) ^ 6 ≤ (2 + Real.log (Kb + 2)) ^ 6 → 0 ≤ (↑S.K + 2) ^ eq' → 0 ≤ 1 + finiteDepthConstant κ q Nd → 0 ≤ nbCM κ hq2 hq3 + nbCUM κ hq2 hq3 → 0 ≤ √↑P → 0 ≤ hullCutConstant (ρ / 64 / 2) → (1 + Real.log (↑S.K + 2)) * ↑(Nb + 1) * (1 + Real.log (2 + ↑(Nb + 1) * ↑(Nb + 1) * Yn)) * Γ * hullCutConstant (ρ / 64 / 2) ≤ 160000 * (2 + Real.log (↑S.K + 2)) ^ 6 * Qk → 6 * nearS ≤ ↑Cl * (1 + finiteDepthConstant κ q Nd) * (nbCM κ hq2 hq3 + nbCUM κ hq2 hq3) * (Kb + 2) ^ eq' * (2 + Real.log (Kb + 2)) ^ 6 * Real.exp X ^ Cl / √↑P * R

Step hNEAR of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hceil (Msch : ℝ) (g : ℕ) (cm ce ce2 cQ : ℝ) (CΛ Cb Cl cc : ℕ) : 1 ≤ cc → (⌈Msch⌉₊ + 1) * CΛ ^ 16 + 1 ≤ Cb → ⌈cm * ↑Cb ^ 59 + ce * ↑Cb ^ 18 + ce2 + 3 * 10 ^ 11 * cQ⌉₊ + 59 * Cb + 4 * g + 8 * cc + 8 ≤ Cl → cm * ↑Cb ^ 59 + ce * ↑Cb ^ 18 + ce2 + 3 * 10 ^ 11 * cQ ≤ ↑Cl

Step hceil of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hCm (κ : LocalKernelClass) (cT cMc cm : ℝ) : ∀ (a : ℕ), cm = 196608 * cT + 83 * (1 + 81 * localFormUniformConstant κ * (30000 + √cT)) * (1 + cT) ^ 3 + cMc → ∀ (B : ℝ), 1 ≤ B → ∀ (G : ℝ), 1 ≤ G → 0 ≤ localFormUniformConstant κ → 0 ≤ cT → 0 ≤ cMc → 0 ≤ B → 0 ≤ G → √(cT * B ^ 11 * G) ≤ √cT * B ^ 6 * G → 1 ≤ B ^ 6 * G → B ^ 2 * G ≤ B ^ 6 * G → 196608 * B ^ 3 * (cT * B ^ 11 * G) + 83 * (1 + 81 * localFormUniformConstant κ * (30000 * B ^ 2 * G + √(cT * B ^ 11 * G))) * (1 + cT * B ^ 11 * G) ^ 3 + cMc * B ^ 59 * G ^ 2 ≤ cm * B ^ 59 * G ^ 4

Step hCm of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hClm (Msch : ℝ) (g : ℕ) (cm ce ce2 cQ : ℝ) (CΛ Cb Cl cc : ℕ) : 1 ≤ cc → (⌈Msch⌉₊ + 1) * CΛ ^ 16 + 1 ≤ Cb → ⌈cm * ↑Cb ^ 59 + ce * ↑Cb ^ 18 + ce2 + 3 * 10 ^ 11 * cQ⌉₊ + 59 * Cb + 4 * g + 8 * cc + 8 ≤ Cl → ∀ (u : ℝ), 1 ≤ u → ∀ (B : ℝ), B = ↑Cb * u ^ Cb → ∀ (X G : ℝ), 0 ≤ ce2 → 0 ≤ cQ → 1 ≤ Real.exp X → G = Real.exp X ^ g → 0 ≤ G → cm * ↑Cb ^ 59 + ce * ↑Cb ^ 18 + ce2 + 3 * 10 ^ 11 * cQ ≤ ↑Cl → 0 ≤ ce * ↑Cb ^ 18 → cm * B ^ 59 * G ^ 4 ≤ ↑Cl * u ^ Cl * Real.exp X ^ Cl

Step hClm of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hErr (κ : LocalKernelClass) (Msch : ℝ) (g : ℕ) (cT cm ce ce2 cQ : ℝ) (CΛ Cb Cl k cc : ℕ) : 1 ≤ cc → ∀ (kD : ℝ) (Mp V : ℕ) (δ R : ℝ) (S : ModeSchedule) (Iw : ℕ) (U MV ε cE : ℝ), ce = 6642 * localFormUniformConstant κ * (60000 + √cT) ^ 3 * 288 + 9 * (16 * fourErrC κ 3 + 648 * threeErrC κ 3 1 + 324 * threeErrC κ 3 1 * √cT) → 0 ≤ R → (⌈Msch⌉₊ + 1) * CΛ ^ 16 + 1 ≤ Cb → ⌈cm * ↑Cb ^ 59 + ce * ↑Cb ^ 18 + ce2 + 3 * 10 ^ 11 * cQ⌉₊ + 59 * Cb + 4 * g + 8 * cc + 8 ≤ Cl → ∀ (u : ℝ), 1 ≤ u → ∀ (B : ℝ), B = ↑Cb * u ^ Cb → 1 ≤ B → ∀ (X G : ℝ), 1 ≤ G → 1 ≤ ↑k ^ cc → 1 ≤ cT → ∀ (ι : ℝ), have Qe := 16 * fourErrC κ 3 * ι + K1c * (2 * fourKC κ 3 * 12 ^ 4 * ε * U ^ 3 * S.Dstar ^ 4) + 4 * (81 * threeErrC κ 3 1 * ι * U + K1c * (8 * entryCU κ 3 1 * 2 ^ (1 + 4) * 12 ^ 3 * ε * U ^ 3 * (S.Dstar ^ 3 * (↑Iw + 1)))); cE ≤ Qe * (↑(Mp * V) * R) → ↑(Mp * V) = MV → Qe * MV ≤ 5 * (16 * fourErrC κ 3 + 648 * threeErrC κ 3 1 + 324 * threeErrC κ 3 1 * √cT) * Real.exp (3 * ↑k ^ cc) * B ^ 6 * G * Real.exp (-kD) + ce2 * Real.exp (-↑k) → 0 ≤ localFormUniformConstant κ → 0 ≤ ce2 → 0 ≤ cQ → 1 ≤ Real.exp X → G = Real.exp X ^ g → 0 ≤ B → 0 ≤ G → cm * ↑Cb ^ 59 + ce * ↑Cb ^ 18 + ce2 + 3 * 10 ^ 11 * cQ ≤ ↑Cl → 0 ≤ cm * ↑Cb ^ 59 → 0 ≤ ce * ↑Cb ^ 18 → √(cT * B ^ 11 * G) ≤ √cT * B ^ 6 * G → 1 ≤ B ^ 6 * G → B ^ 2 * G ≤ B ^ 6 * G → 6642 * localFormUniformConstant κ * (2 * (30000 * B ^ 2 * G) + √(cT * B ^ 11 * G)) ^ 3 * (288 * Real.exp (4 * ↑k ^ cc) * √δ * R) + cE ≤ ↑Cl * u ^ Cl * Real.exp X ^ Cl * (Real.exp (↑Cl * ↑k ^ cc) * (√δ + Real.exp (-kD))) * R + ↑Cl * Real.exp (-↑k) * R

Step hErr of leaf_final, over the part of its context that it uses.

theorem TrilinearHT.Auto.leaf_final_hfc0 (P famFuel : ℕ) (τ₃ : ℝ) : 0 < τ₃ → ∀ (fc : ℝ), fc = (2 * ↑famFuel + 2) * ((↑P + 1) ^ 2 * (16 * τ₃ * 2 ^ 2)) → 0 ≤ (↑P + 1) ^ 2 → 0 ≤ fc

Step hfc0 of leaf_final, over the part of its context that it uses.