OAI/Analysis/MassAction/AffineNeighborhood.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem326.Affine.coordinateMinimum line 15
2. theorem OAI.Problem326.Affine.continuous_coordinateMinimum line 18
3. theorem OAI.Problem326.Affine.hasMinimum_coordinateMinimum line 22
4. theorem OAI.Problem326.Affine.hasMinimum_iff_coordinateMinimum_eq line 28
5. theorem OAI.Problem326.Affine.isCompact_cube line 39
6. theorem OAI.Problem326.Affine.ApproximatesAtMinimum.exists_nearby line 48

   Source documentation

   Activity that approximates at a fixed minimum continues to approximate for every limiting minimum in a positive band.

   theorem ApproximatesAtMinimum.exists_nearby [NeZero d]
       {Λ : Finset (Label d)} {a b t : ℝ} {E : (Fin d → ℝ) → ℝ}
       (hΛ : ApproximatesAtMinimum Λ a b t E) :
       ∃ ρ : ℝ, 0 < ρ ∧ ∀ L ∈ Λ,
         ∀ (h : ℕ → ℝ) (p : ℕ → (Fin d → ℝ)) (p₀ : Fin d → ℝ),
         (∀ n, 0 < h n) → Tendsto h atTop (𝓝 0) →
         Tendsto p atTop (𝓝 p₀) → Cube a b p₀ →
         |coordinateMinimum p₀ - t| < ρ →
         (∀ n, Active Λ L (h n) (powerPoint (h n) (p n))) →
         ‖p₀ - L.slope‖ < E L.slope := by
   …

   Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.ApproximatesAtMinimum, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.coordinateMinimum, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.powerPoint

7. def OAI.Problem326.Affine.ApproximatesOnCube line 78

   Source documentation

   The full sequential conclusion of the affine approximation lemma.

   def ApproximatesOnCube (Λ : Finset (Label d))
       (a b : ℝ) (E : (Fin d → ℝ) → ℝ) : Prop :=
   …

   Mentions: OAI.Problem326.Affine.Label

8. theorem OAI.Problem326.Affine.ApproximatesOnCube.uniform_activity line 87

   Source documentation

   Uniform-activity corollary for the exact affine-label interface.

   theorem ApproximatesOnCube.uniform_activity
       {Λ : Finset (Label d)} {a b : ℝ} {E : (Fin d → ℝ) → ℝ}
       (hΛ : ApproximatesOnCube Λ a b E) :
       ∃ δ : ℝ, 0 < δ ∧ ∀ h, 0 < h → h < δ →
         ∀ p, Cube a b p → ∀ L ∈ Λ,
         Active Λ L h (powerPoint h p) → ‖p - L.slope‖ < E L.slope := by
   …

   Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.ApproximatesOnCube, OAI.Problem326.Affine.Cube, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.powerPoint