LowerBoundAssembly.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Circuit-size lower bounds from eventual rank and second-trace estimates for the normalized IMM matrix.

theorem OAI.Problem335.complex_depth_five_lower_bound_of_eventual_rank_lower line 18

Source documentation

An eventual lower bound for the configured IMM rank, together with the proved circuit upper bound, gives the exact complex circuit-size conclusion.

theorem complex_depth_five_lower_bound_of_eventual_rank_lower (C : ℝ)
    (hlower : ∀ᶠ n : ℕ in Filter.atTop,
      rankDimension n * Real.exp (-C * Real.sqrt (n : ℝ)) ≤
        rankData n (imm ℂ n)) :
    ∃ n0 : ℕ, ∀ n : ℕ, n0 ≤ n → ∀ c : Depth5Circuit ℂ n,
      circuitValue c = imm ℂ n →
      (n : ℝ) ^ (Real.sqrt (n : ℝ) / 400) ≤ (circuitSize c : ℝ) := by
…

Mentions: OAI.Problem335.imm, OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.circuitSize

theorem OAI.Problem335.complex_depth_five_lower_bound_of_eventual_second_trace line 47

Source documentation

The second-trace bound, together with the first-trace and circuit estimates, implies the complex circuit-size lower bound.

theorem complex_depth_five_lower_bound_of_eventual_second_trace (C : ℝ)
    (hsecond : ∀ᶠ n : ℕ in Filter.atTop, ∀ hn : 16 ≤ n,
      (((immNormalizedMatrix n
          (balancedLayer (Nat.le_trans (by decide : 4 ≤ 16) hn)) (a n) (b n)).conjTranspose *
        immNormalizedMatrix n
          (balancedLayer (Nat.le_trans (by decide : 4 ≤ 16) hn)) (a n) (b n)) ^ 2).trace.re ≤
        rankDimension n * rankMomentScale n ^ 2 *
          Real.exp (C * Real.sqrt (n : ℝ))) :
    ∃ n0 : ℕ, ∀ n : ℕ, n0 ≤ n → ∀ c : Depth5Circuit ℂ n,
      circuitValue c = imm ℂ n →
      (n : ℝ) ^ (Real.sqrt (n : ℝ) / 400) ≤ (circuitSize c : ℝ) := by
…

Mentions: OAI.Problem335.immNormalizedMatrix, OAI.Problem335.Depth5Circuit, OAI.Problem335.circuitValue, OAI.Problem335.imm, OAI.Problem335.circuitSize