OAI/Algebra/DepthFive/ConfiguredImmSecondMoment.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.LowerParameters.configured_layerMeanV line 13
2. theorem OAI.Problem335.LowerParameters.configured_layerMeanU line 19
3. theorem OAI.Problem335.LowerParameters.v_fraction line 26
4. theorem OAI.Problem335.LowerParameters.u_fraction line 31
5. theorem OAI.Problem335.LowerParameters.configured_imm_second_moment_upper line 37

   Source documentation

   The complete actual second-trace estimate for the canonical parameters.

   theorem configured_imm_second_moment_upper {n : ℕ} (hn : 16 ≤ n)
       (hbeta : beta n ≤ 2 / Real.sqrt (n : ℝ)) :
       let A := immNormalizedMatrix n (balancedLayer (show 4 ≤ n by omega)) (a n) (b n)
   …

   Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.immNormalizedMatrix, OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b

6. theorem OAI.Problem335.LowerParameters.eventually_configured_imm_second_moment_upper line 65

   Source documentation

   A single eventual statement supplies the actual matrix premise required by the final rank and circuit-size comparison.

   theorem eventually_configured_imm_second_moment_upper :
       ∀ᶠ n : ℕ in Filter.atTop, ∀ hn : 16 ≤ n,
         let A := immNormalizedMatrix n (balancedLayer (show 4 ≤ n by omega)) (a n) (b n)
   …

   Mentions: OAI.Problem335.immNormalizedMatrix, OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.b