BlockCritical.lean`

51 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.FKCRT.Inventory.stoppedWord_length_pos line 11
lemma OAI.FKCRT.Inventory.rawSeamWord_seamWord line 13
lemma OAI.FKCRT.Inventory.up_length_injective line 17
def OAI.FKCRT.Inventory.seamIntervals line 30
lemma OAI.FKCRT.Inventory.mem_seamIntervals line 31
lemma OAI.FKCRT.Inventory.sum_seamIntervals line 38
lemma OAI.FKCRT.Inventory.sum_ite_le_of_injection line 46
def OAI.FKCRT.Inventory.shortSeamSuccess line 62
lemma OAI.FKCRT.Inventory.shortSeamSuccess_measurable line 64
lemma OAI.FKCRT.Inventory.seam_count_le line 66
lemma OAI.FKCRT.Inventory.interval_expected_count line 97
theorem OAI.FKCRT.Inventory.emptyProb_partial_lower line 116
Source documentation
Counting the actual distinct stopped seam intervals gives quantitative quadratic-scale partial-sum lower bounds for the exact empty-word probabilities.
```
theorem emptyProb_partial_lower (P : Parameters) : ∃ (δ : ℝ) (A : ℕ),0<δ ∧ 0<A ∧ ∀ H : ℕ,
    δ*H ≤ ∑ N∈Finset.range (2*A*H^2+1),(N+1:ℝ)*emptyProb P (N+2) := by
…
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.emptyProb
lemma OAI.FKCRT.Analysis.log_lower_near_one line 160

theorem OAI.FKCRT.Analysis.quadratic_partial_abel_lower line 170

Source documentation

A square-root lower bound on quadratic partial sums implies the exact Abel square-root divergence, without an unproved Tauberian principle.

theorem quadratic_partial_abel_lower (b : ℕ → ℝ) (hb : ∀ n,0≤b n)
    (δ : ℝ) (hδ : 0<δ) (A : ℕ)
    (hpartial : ∀ H : ℕ,δ*H≤∑ n∈Finset.range (2*A*H^2+1),b n) :
    ∃ c : ℝ,0<c ∧ ∀ x : ℝ,(3:ℝ)/4≤x → x<1 →
      Summable (fun n => b n*x^n) → c/Real.sqrt (1-x)≤∑' n,b n*x^n := by
…

lemma OAI.FKCRT.Inventory.increment_sum_parity line 234
lemma OAI.FKCRT.Inventory.emptyReducing_even line 240
lemma OAI.FKCRT.Inventory.emptyProb_odd line 244
lemma OAI.FKCRT.Inventory.emptyProb_le_one line 252
lemma OAI.FKCRT.Inventory.empty_interval_pair_sum line 254
lemma OAI.FKCRT.Inventory.empty_even_partial_lower line 267
lemma OAI.FKCRT.Inventory.summable_empty_abel line 292
theorem OAI.FKCRT.Inventory.empty_abel_lower line 303
Source documentation
The exact genuine iid inventory empty-word coefficients satisfy the source Abel square-root lower bound; no map-counting identity is assumed here.
```
theorem empty_abel_lower (P : Parameters) : ∃ c : ℝ,0<c ∧ ∀ x : ℝ,(3:ℝ)/4≤x → x<1 →
    c/Real.sqrt (1-x)≤∑' n : ℕ,(n:ℝ)*emptyProb P (2*n)*x^n := by
…
```
Mentions: OAI.FKCRT.Inventory.Parameters, OAI.FKCRT.Inventory.emptyProb
def OAI.FKCRT.BlockCritical.geomPrefix line 319
def OAI.FKCRT.BlockCritical.triPrefix line 321
lemma OAI.FKCRT.BlockCritical.geomPrefix_nonneg line 323
lemma OAI.FKCRT.BlockCritical.geomPrefix_mul line 326
lemma OAI.FKCRT.BlockCritical.geomPrefix_le_nat line 334
lemma OAI.FKCRT.BlockCritical.geomPrefix_le_inv line 341
lemma OAI.FKCRT.BlockCritical.geomPrefix_one line 347
lemma OAI.FKCRT.BlockCritical.continuous_geomPrefix line 349
lemma OAI.FKCRT.BlockCritical.triPrefix_nonneg line 353
lemma OAI.FKCRT.BlockCritical.triPrefix_mul line 356
lemma OAI.FKCRT.BlockCritical.triPrefix_le_div line 368
lemma OAI.FKCRT.BlockCritical.square_eq_triPrefix line 375
lemma OAI.FKCRT.BlockCritical.continuous_triPrefix line 384
structure OAI.FKCRT.BlockCritical.Weights line 387
def OAI.FKCRT.BlockCritical.Weights.pgf line 392
lemma OAI.FKCRT.BlockCritical.Weights.summable_pgf line 394
lemma OAI.FKCRT.BlockCritical.Weights.pgf_nonneg line 400
lemma OAI.FKCRT.BlockCritical.Weights.pgf_le_one line 403
lemma OAI.FKCRT.BlockCritical.Weights.summable_geom line 408
lemma OAI.FKCRT.BlockCritical.Weights.geom_identity line 414
lemma OAI.FKCRT.BlockCritical.Weights.tendsto_pgf line 424

theorem OAI.FKCRT.BlockCritical.Weights.moments_of_quadratic line 436

Source documentation

A quadratic inverse gap is enough for the exact critical first moment and finite second moment. No analyticity past the endpoint or third moment occurs. The hypotheses are the normalized source inverse bound, not moment assumptions.

theorem Weights.moments_of_quadratic (p : Weights) {x : ℕ → ℝ}
    (hx : ∀ n,0≤x n ∧ x n<1) (ht : Tendsto x atTop (𝓝 1))
    {C : ℝ} (_hC : 0≤C)
    (hgap : ∀ n,0≤(p.pgf (x n))^2-x n ∧
      (p.pgf (x n))^2-x n≤C*(1-x n)^2) :
    HasSum (fun k : ℕ => (k:ℝ)*p.mass k) (1/2) ∧
      Summable (fun k : ℕ => (k:ℝ)^2*p.mass k) := by
…

Mentions: OAI.FKCRT.BlockCritical.Weights

lemma OAI.FKCRT.BlockCritical.Weights.mass_le_one line 551
def OAI.FKCRT.BlockCritical.Weights.abelMean line 555
lemma OAI.FKCRT.BlockCritical.Weights.summable_abelMean line 557
lemma OAI.FKCRT.BlockCritical.geomPrefix_lower line 565
lemma OAI.FKCRT.BlockCritical.Weights.abelMean_gap line 572
lemma OAI.FKCRT.BlockCritical.hasSum_of_pgf_limit line 583
Source documentation
Endpoint passage for nonnegative coefficients. This supplies the endpoint normalization of Phi from the actual interior substitution equation; it does not assume the desired probability normalization.
```
lemma hasSum_of_pgf_limit {b : ℕ → ℝ} (hb : ∀ k,0≤b k)
    {x t : ℕ → ℝ} (hx : ∀ n,0≤x n ∧ x n≤1)
    (hxt : Tendsto x atTop (𝓝 1)) (ht : Tendsto t atTop (𝓝 1))
    (heq : ∀ n,HasSum (fun k => b k*(x n)^k) (t n)) : HasSum b 1 := by
…
```

theorem OAI.FKCRT.BlockCritical.normalized_inverse_critical line 610

Source documentation

Source block:critical in normalized variables. Only the original nonnegative generating-function substitution and Abel lower bound are used. The mean/variance conclusions are proved, not included as assumptions.

theorem normalized_inverse_critical (p : Weights) {b : ℕ → ℝ}
    (hb : ∀ k,0≤b k) {x : ℕ → ℝ} (hx : ∀ n,0≤x n ∧ x n<1)
    (ht : Tendsto x atTop (𝓝 1))
    (heq : ∀ n,HasSum (fun k => b k*(x n*(p.pgf (x n))^2)^k) (p.pgf (x n)))
    {c : ℝ} (hc : 0<c)
    (hlower : ∀ n,c≤Real.sqrt (1-x n)*p.abelMean (x n)) :
    HasSum b 1 ∧ HasSum (fun k : ℕ => (k:ℝ)*b k) (1/2) ∧
      Summable (fun k : ℕ => (k:ℝ)^2*b k) := by
…

Mentions: OAI.FKCRT.BlockCritical.Weights