BlockEstimates.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.SeparableQuotient.RecordGrowth.div_rpow_tendsto_atTop line 12

Source documentation

The logarithmic parameter limit implies unboundedness above every smaller power.

lemma div_rpow_tendsto_atTop {a b : ℕ → ℝ} {p e : ℝ}
    (ha : ∀ n, 1 < a n) (hb : ∀ n, 0 < b n)
    (hA : Tendsto a atTop atTop)
    (hlog : Tendsto (fun n => Real.log (b n) / Real.log (a n)) atTop (𝓝 p))
    (he : e < p) : Tendsto (fun n => b n / (a n)^e) atTop atTop := by
…

lemma OAI.SeparableQuotient.RecordGrowth.exists_record line 32

Source documentation

A record ratio over a finite initial segment, with a prescribed large value of a(k), precisely as in the partition-block argument.

lemma exists_record (a : ℕ → ℝ) (e M : ℝ) (he : 0 ≤ e) (hM : 0 ≤ M)
    (hunbounded : ∀ R : ℝ, ∃ k : ℕ, 1 ≤ k ∧ R < a k / (k : ℝ)^e) :
    ∃ k : ℕ, 1 ≤ k ∧ M ≤ a k ∧
      ∀ l : ℕ, 1 ≤ l → l ≤ k → a l ≤ a k * ((l : ℝ)/(k : ℝ))^e := by
…

lemma OAI.SeparableQuotient.RecordGrowth.choose_exponent line 57
Source documentation
A slightly smaller reciprocal exponent can be chosen uniformly for all of the finitely many partition sizes under consideration.
```
lemma choose_exponent (s N : ℝ) (hs : 1 < s) (hN : 1 ≤ N) :
    ∃ e : ℝ, 0 < e ∧ e < 1/s ∧
      ∀ d : ℝ, 1 ≤ d → d ≤ N → d^(1-e) ≤ 2*d^(1-1/s) := by
…
```

lemma OAI.SeparableQuotient.RecordGrowth.sum_rpow_le_card line 83

Source documentation

The finite concave power bound (Hölder) in the unit-block partition proof.

lemma sum_rpow_le_card {ι : Type*} [Fintype ι] (w : ι → ℝ) (e : ℝ)
    (he : 0 < e) (he1 : e < 1) (hw : ∀ i, 0 ≤ w i) (hs : ∑ i, w i ≤ 1) :
    ∑ i, (w i)^e ≤ (Fintype.card ι : ℝ)^(1-e) := by
…

lemma OAI.SeparableQuotient.ActualSpace.blockSumSup_div_rpow_unbounded line 108

lemma OAI.SeparableQuotient.IntervalIncidence.partial_intersections_le_two line 145

Source documentation

Only the first and last members of a successive finite family can partly intersect one order-convex interval.

lemma partial_intersections_le_two (s : Finset α) (F : α → Finset β)
    (hF : ∀ i j, i < j → ∀ a ∈ F i, ∀ b ∈ F j, a < b)
    (I : Set β) (hI : Set.OrdConnected I) :
    (s.filter (fun i => (∃ a ∈ F i, a ∈ I) ∧ ¬ (↑(F i) : Set β) ⊆ I)).card ≤ 2 := by
…

lemma OAI.SeparableQuotient.IntervalIncidence.noncrossing_multichild_column_le_two line 168

Source documentation

A noncrossing incidence matrix has at most two multichild rows incident to each fixed child.

lemma noncrossing_multichild_column_le_two (s : Finset α) (t : Finset β) (R : α → β → Prop)
    (hR : ∀ i ∈ s, ∀ j ∈ s, i < j → ∀ a ∈ t, ∀ b ∈ t, R i a → R j b → a ≤ b)
    (a : β) (ha : a ∈ t) :
    (s.filter (fun i => R i a ∧ 2 ≤ (t.filter (R i)).card)).card ≤ 2 := by
…

lemma OAI.SeparableQuotient.IntervalIncidence.noncrossing_boundary_incidence line 197
lemma OAI.SeparableQuotient.ActualSpace.intervalProjection_fixed line 221
lemma OAI.SeparableQuotient.ActualSpace.intervalProjection_eq_zero line 232
lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.interval_norm_le line 243
lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.full_card_sum_le line 279
lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.subsum_record line 304
lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.partition_sum_record line 314
lemma OAI.SeparableQuotient.ActualSpace.UnitBlocks.normalized_partition line 340
theorem OAI.SeparableQuotient.ActualSpace.BlockSequence.exists_partition_unit line 377
Source documentation
The constant-eight interval partition estimate in any prescribed algebraic tail of a block sequence.
```
theorem BlockSequence.exists_partition_unit {f : Family} (z : BlockSequence f)
    (a N : ℕ) (hN : 1 ≤ N) :
    ∃ u : Γ →₀ ℝ, u ∈ z.tailSpan a ∧ ‖norming.includeFinite u‖ = 1 ∧
      PartitionBound (norming.includeFinite u) N 8 f.r := by
…
```
Mentions: OAI.SeparableQuotient.ActualSpace.BlockSequence, OAI.SeparableQuotient.ActualSpace.PartitionBound