OAI/Analysis/MassAction/LayerSequence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.Affine.exists_layer_sequence line 15

   Source documentation

   Build the finite sequence of type families used at a fixed minimum. Each new threshold is chosen only after the preceding finite family, so arbitrary positive label-dependent tolerances are allowed. The family constructor may itself depend on the chosen threshold.

   theorem exists_layer_sequence {α : Type uAlpha} (n : ℕ) {t b : ℝ} (htb : t < b)
       (E : α → ℝ) (F₀ : Finset α) (hE₀ : ∀ a ∈ F₀, 0 < E a)
       (Good : ℕ → ℝ → Finset α → Prop)
       (hmake : ∀ k : ℕ, 0 < k → k ≤ n → ∀ β : ℝ, t < β → β < b →
         ∃ F : Finset α, Good k β F ∧ ∀ a ∈ F, 0 < E a) :
       ∃ (β : ℕ → ℝ) (F : ℕ → Finset α),
         β 0 = b ∧ F 0 = F₀ ∧
         (∀ k, t < β k ∧ β k ≤ b ∧ ∀ a ∈ F k, 0 < E a) ∧
         ∀ k < n, β (k + 1) < β k ∧
           (∀ a ∈ F k, β (k + 1) - t < E a) ∧
           Good (k + 1) (β (k + 1)) (F (k + 1)) := by
   …