OAI/Algebra/DepthFive/BalancedWordSum.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem335.LowerParameters.balanced_word_sum_bound_of_product line 14

   Source documentation

   The full graph-word estimate for the actual balanced layer partition. All path-graph, endpoint, flip, and cardinality premises are discharged.

   lemma balanced_word_sum_bound_of_product {n : ℕ} (hn : 4 ≤ n + 1)
       (A B E : ℝ) (hA : 1 ≤ A) (hAN : A ≤ Real.sqrt ((n + 1 : ℕ) : ℝ))
       (hB : 0 ≤ B) (hE : E ≤ Real.sqrt ((n + 1 : ℕ) : ℝ))
       (hprod : ∀ w : Fin (n + 1) → Bool,
         A ^ ((Finset.univ.filter (fun i => balancedLayer hn i = true)).filter
           (fun i => w i = true)).card *
         B ^ ((Finset.univ \ Finset.univ.filter (fun i => balancedLayer hn i = true)).filter
           (fun i => w i = true)).card ≤
         Real.exp E * ((n + 1 : ℕ) : ℝ) ^ WordRuns.runCount w) :
       (∑ w : Fin (n + 1) → Bool,
         IsolatedWeight.weight (BalancedSchedule.internalEdges (n + 1))
           (Finset.univ.filter (fun i => balancedLayer hn i = true))
   …

   Mentions: OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.WordRuns.runCount, OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.BalancedSchedule.internalEdges

2. lemma OAI.Problem335.LowerParameters.balanced_word_sum_bound line 81

   Source documentation

   The canonical balanced schedule satisfies the complete corrected-word bound. The only premises are the scalar parameter inequalities.

   lemma balanced_word_sum_bound {n : ℕ} (hn : 4 ≤ n) {α β ε : ℝ}
       (hα : 0 < α) (hα1 : α ≤ 1) (hαN : α⁻¹ ≤ Real.sqrt (n : ℝ))
       (hβ : 0 ≤ β) (hβupper : β ≤ α ^ rho n * Real.exp ε)
       (hscale : α ^ (-(1 + rho n)) ≤ (n : ℝ))
       (hε : 0 ≤ ε) (hεN : ε * (n : ℝ) ≤ Real.sqrt (n : ℝ)) :
       (∑ w : Fin n → Bool,
         IsolatedWeight.weight (BalancedSchedule.internalEdges n)
           (Finset.univ.filter (fun i => balancedLayer hn i = true))
           BalancedSchedule.adjacent α⁻¹ β ((n : ℝ)⁻¹) w) ≤
         Real.exp (8 * Real.sqrt (n : ℝ)) := by
   …

   Mentions: OAI.Problem335.LowerParameters.rho, OAI.Problem335.IsolatedWeight.weight, OAI.Problem335.BalancedSchedule.internalEdges, OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.BalancedSchedule.adjacent