OAI/Algebra/DepthFive/PathMassLowerBound.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem335.bidegree_first_moment_lower_bool line 14

   Source documentation

   Boolean-fiber form of the occupation lower estimate.

   theorem bidegree_first_moment_lower_bool {σ : Type*} [Fintype σ] [DecidableEq σ]
       (side : σ → Bool) (a b : ℕ) [Fintype (Index side a b)]
       [Nonempty {x // side x = true}] [Nonempty {x // side x = false}]
       (s : Finset {x // side x = true}) (z : Finset {x // side x = false})
       (ha : 0 < a) (hb : 0 < b) (hs : 2 * s.card ≤ a) (hz : 2 * z.card ≤ b) :
       Real.exp ((-(s.card : ℝ) ^ 2 / a -
           (s.card : ℝ) ^ 2 / (2 * Fintype.card {x // side x = true})) +
         (-(z.card : ℝ) ^ 2 / b -
           (z.card : ℝ) ^ 2 / (2 * Fintype.card {x // side x = false}))) *
         (((a : ℝ) / Fintype.card {x // side x = true}) ^ s.card *
           (1 + (b : ℝ) / Fintype.card {x // side x = false}) ^ z.card) ≤
         (∑ d : Index side a b,
   …

2. theorem OAI.Problem335.path_source_mass_lower line 42

   Source documentation

   Each squarefree Fock path has large average squared amplitude over the actual bidegree source. No independence of coordinates within a group is assumed.

   theorem path_source_mass_lower {σ : Type*} [Fintype σ] [DecidableEq σ]
       (side : σ → Bool) (a b : ℕ) [Fintype (Index side a b)]
       [Nonempty {x // side x = true}] [Nonempty {x // side x = false}]
       (p : List σ) (hp : p.Nodup) (ha : 0 < a) (hb : 0 < b)
       (hs : 2 * (selectedPathCoordinates side p true).card ≤ a)
       (hz : 2 * (selectedPathCoordinates side p false).card ≤ b) :
       Real.exp ((-((selectedPathCoordinates side p true).card : ℝ) ^ 2 / a -
           ((selectedPathCoordinates side p true).card : ℝ) ^ 2 /
             (2 * Fintype.card {x // side x = true})) +
         (-((selectedPathCoordinates side p false).card : ℝ) ^ 2 / b -
           ((selectedPathCoordinates side p false).card : ℝ) ^ 2 /
             (2 * Fintype.card {x // side x = false}))) *
   …

   Mentions: OAI.Problem335.selectedPathCoordinates

3. theorem OAI.Problem335.immPath_source_mass_lower line 68

   Source documentation

   Concrete IMM per-path first moment. The loss and geometric benchmark depend only on the selected layer counts, not on the chosen path.

   theorem immPath_source_mass_lower (n : ℕ) (hn : 0 < n)
       (side : Fin n → Bool) (a b : ℕ)
       [Fintype (Index (fun x : Fin n × Fin n × Fin n => side x.1) a b)]
       [Nonempty {x : Fin n × Fin n × Fin n // side x.1 = true}]
       [Nonempty {x : Fin n × Fin n × Fin n // side x.1 = false}]
       (p : List (Fin n × Fin n × Fin n)) (hp : p ∈ immPaths n hn)
       (ha : 0 < a) (hb : 0 < b)
       (hs : 2 * (Finset.univ.filter (fun t : Fin n => side t = true)).card ≤ a)
       (hz : 2 * (Finset.univ.filter (fun t : Fin n => side t = false)).card ≤ b) :
       Real.exp ((-((Finset.univ.filter (fun t : Fin n => side t = true)).card : ℝ) ^ 2 / a -
           ((Finset.univ.filter (fun t : Fin n => side t = true)).card : ℝ) ^ 2 /
             (2 * Fintype.card {x : Fin n × Fin n × Fin n // side x.1 = true})) +
   …

   Mentions: OAI.Problem335.immPaths