OAI/Analysis/MassAction/UniformAffineData.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem326.Affine.FullCertificate.uniform_affine_data line 13

   Source documentation

   Reindex the fixed finite label set by Fin n, as required by the network barrier construction. This theorem is definitionally the uniform approximation interface there, with the active comparison expanded.

   theorem FullCertificate.uniform_affine_data {d : ℕ}
       {E : (Fin d → ℝ) → ℝ} (hE : ∀ r, 0 < E r)
       (C : FullCertificate d (-1) 1 E) :
       ∃ n : ℕ, 0 < n ∧ ∃ (r : Fin n → Fin d → ℝ)
         (c : Fin n → ℝ → ℝ) (h₀ : ℝ), 0 < h₀ ∧
         ∀ h : ℝ, 0 < h → h < h₀ → ∀ p : Fin d → ℝ,
           (∀ i, |p i| ≤ 1) → ∀ j : Fin n,
             (∀ k : Fin n,
               dot (r j) (fun i => h ^ p i) + c j h ≤
                 dot (r k) (fun i => h ^ p i) + c k h) →
             ∀ i, |p i - r j i| < E (r j) := by
   …

   Mentions: OAI.Problem326.Affine.FullCertificate, OAI.Problem326.dot

2. theorem OAI.Problem326.Affine.uniform_affine_data_of_full_certificates line 46

   Source documentation

   The full affine-certificate theorem supplies the network's entire arbitrary-positive-tolerance uniform approximation interface.

   theorem uniform_affine_data_of_full_certificates {d : ℕ}
       (hfull : ∀ E : (Fin d → ℝ) → ℝ, (∀ r, 0 < E r) →
         Nonempty (FullCertificate d (-1) 1 E)) :
       ∀ E : (Fin d → ℝ) → ℝ, (∀ r, 0 < E r) →
         ∃ n : ℕ, 0 < n ∧ ∃ (r : Fin n → Fin d → ℝ)
           (c : Fin n → ℝ → ℝ) (h₀ : ℝ), 0 < h₀ ∧
           ∀ h : ℝ, 0 < h → h < h₀ → ∀ p : Fin d → ℝ,
             (∀ i, |p i| ≤ 1) → ∀ j : Fin n,
               (∀ k : Fin n,
                 dot (r j) (fun i => h ^ p i) + c j h ≤
                   dot (r k) (fun i => h ^ p i) + c k h) →
               ∀ i, |p i - r j i| < E (r j) := by
   …

   Mentions: OAI.Problem326.Affine.FullCertificate, OAI.Problem326.dot