OAI/Analysis/MassAction/AffineLocalBand.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem326.Affine.minimumCoordinate line 14

   Source documentation

   The least coordinate in a positive-dimensional exponent vector.

   def minimumCoordinate {d : ℕ} (hd : 0 < d) (p : Fin d → ℝ) : ℝ :=
   …

2. theorem OAI.Problem326.Affine.continuous_minimumCoordinate line 17
3. theorem OAI.Problem326.Affine.hasMinimum_minimumCoordinate line 21
4. theorem OAI.Problem326.Affine.minimumCoordinate_eq_of_hasMinimum line 28
5. theorem OAI.Problem326.Affine.minimumCoordinate_mem_Icc line 36
6. theorem OAI.Problem326.Affine.isCompact_cube_localBand line 42
7. theorem OAI.Problem326.Affine.exists_local_band_of_approximatesAtMinimum line 49

   Source documentation

   Approximation at a fixed minimum level extends to a band of nearby minimum levels. Approximating sequences themselves may leave the exponent cube.

   theorem exists_local_band_of_approximatesAtMinimum
       {d : ℕ} (hd : 0 < d) (Λ : Finset (Label d)) (a b t : ℝ)
       (E : (Fin d → ℝ) → ℝ) (happrox : 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₀ →
         |minimumCoordinate hd 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.minimumCoordinate, OAI.Problem326.Affine.Active, OAI.Problem326.Affine.powerPoint

8. theorem OAI.Problem326.Affine.approximatesAtMinimum_nearby line 84

   Source documentation

   Convenient family-level interface for gluing: the same finite family approximates at every minimum level in an open interval about t.

   theorem approximatesAtMinimum_nearby
       {d : ℕ} (hd : 0 < d) (Λ : Finset (Label d)) (a b t : ℝ)
       (E : (Fin d → ℝ) → ℝ) (happrox : ApproximatesAtMinimum Λ a b t E) :
       ∃ ρ : ℝ, 0 < ρ ∧ ∀ s ∈ Ioo (t - ρ) (t + ρ),
         ApproximatesAtMinimum Λ a b s E := by
   …

   Mentions: OAI.Problem326.Affine.Label, OAI.Problem326.Affine.ApproximatesAtMinimum