OAI/Analysis/MassAction/NetworkApproximation.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.BarrierConstruction.uniformAffineApproximation_of_finite_labels line 12

   Source documentation

   Convert the canonical finite-label uniform approximation statement to the finite-index interface consumed by the network barrier construction.

   theorem uniformAffineApproximation_of_finite_labels {d : ℕ}
       (hlabels : ∀ E : (Fin d → ℝ) → ℝ, (∀ r, 0 < E r) →
         ∃ Λ : Finset (Affine.Label d), Λ.Nonempty ∧ ∃ h₀ : ℝ, 0 < h₀ ∧
           ∀ h : ℝ, 0 < h → h < h₀ → ∀ p : Fin d → ℝ,
             Affine.Cube (-1) 1 p → ∀ L : Affine.Label d,
               Affine.Active Λ L h (Affine.powerPoint h p) →
               ‖p - L.slope‖ < E L.slope) :
       UniformAffineApproximation d := by
   …

   Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.powerPoint, OAI.Problem326.BarrierConstruction.UniformAffineApproximation