OAI/Algebra/DepthFive/PathMassParameters.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.card_bool_layer_variables line 14

   Source documentation

   A Boolean layer choice includes all square-matrix coordinates in that layer.

   theorem card_bool_layer_variables {n : ℕ} (side : Fin n → Bool) (ε : Bool) :
       Fintype.card {x : Fin n × Fin n × Fin n // side x.1 = ε} =
         (Finset.univ.filter (fun t : Fin n => side t = ε)).card * n ^ 2 := by
   …

2. theorem OAI.Problem335.immPath_source_mass_lower_parameters line 22

   Source documentation

   Uniform per-path first-moment estimate at the canonical lower-bound parameters. Its only partition hypotheses are the two selected layer counts.

   theorem immPath_source_mass_lower_parameters {n : ℕ} (hn : 16 ≤ n)
       (side : Fin n → Bool)
       (hk : (Finset.univ.filter (fun t : Fin n => side t = true)).card = k n)
       (hm : (Finset.univ.filter (fun t : Fin n => side t = false)).card = m n)
       [Fintype (Index (fun x : Fin n × Fin n × Fin n => side x.1) (a n) (b n))]
       (p : List (Fin n × Fin n × Fin n))
       (hp : p ∈ immPaths n (by omega)) :
       Real.exp (-64 / Real.sqrt (n : ℝ)) *
         (((a n : ℝ) / v n) ^ k n * (1 + (b n : ℝ) / u n) ^ m n) ≤
         (∑ d : Index (fun x : Fin n × Fin n × Fin n => side x.1) (a n) (b n),
           ((p.map (occupationAmplitude (fun x => side x.1) d.val)).prod) ^ 2) /
           (Fintype.card (Index (fun x : Fin n × Fin n × Fin n => side x.1)
   …

   Mentions: OAI.Problem335.immPaths, OAI.Problem335.occupationAmplitude

3. theorem OAI.Problem335.immPath_source_sum_lower_parameters line 77

   Source documentation

   Unnormalized actual source sum. This form is directly summable over paths in the first-trace identity, and requires no additional source-nonemptiness premise.

   theorem immPath_source_sum_lower_parameters {n : ℕ} (hn : 16 ≤ n)
       (side : Fin n → Bool)
       (hk : (Finset.univ.filter (fun t : Fin n => side t = true)).card = k n)
       (hm : (Finset.univ.filter (fun t : Fin n => side t = false)).card = m n)
       [Fintype (Index (fun x : Fin n × Fin n × Fin n => side x.1) (a n) (b n))]
       (p : List (Fin n × Fin n × Fin n))
       (hp : p ∈ immPaths n (by omega)) :
       (Fintype.card (Index (fun x : Fin n × Fin n × Fin n => side x.1)
         (a n) (b n)) : ℝ) * Real.exp (-64 / Real.sqrt (n : ℝ)) *
         (((a n : ℝ) / v n) ^ k n * (1 + (b n : ℝ) / u n) ^ m n) ≤
         ∑ d : Index (fun x : Fin n × Fin n × Fin n => side x.1) (a n) (b n),
           ((p.map (occupationAmplitude (fun x => side x.1) d.val)).prod) ^ 2 := by
   …

   Mentions: OAI.Problem335.immPaths, OAI.Problem335.occupationAmplitude