FixedMinimum.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.Problem326.Affine.Label line 14
def OAI.Problem326.Affine.Label.value line 18
def OAI.Problem326.Affine.Active line 21
def OAI.Problem326.Affine.Cube line 25
def OAI.Problem326.Affine.HasMinimum line 28
def OAI.Problem326.Affine.powerPoint line 31
def OAI.Problem326.Affine.ApproximatesAtMinimum line 35
Source documentation
The sequential condition required of a family at one fixed minimum level.
```
def ApproximatesAtMinimum {d : ℕ} (Λ : Finset (Label d))
    (a b t : ℝ) (E : (Fin d → ℝ) → ℝ) : Prop :=
…
```
Mentions: OAI.Problem326.Affine.Label
lemma OAI.Problem326.Affine.active_mono line 43
lemma OAI.Problem326.Affine.active_singleton line 48

lemma OAI.Problem326.Affine.active_iff_common_shift line 58

Source documentation

Comparison activity is insensitive to a common additive shift.

lemma active_iff_common_shift {ι : Type uIota} (s : Finset ι) (v : ι → ℝ)
    (i : ι) (c : ℝ) :
    (∀ j ∈ s, v i + c ≤ v j + c) ↔ (∀ j ∈ s, v i ≤ v j) := by
…

lemma OAI.Problem326.Affine.exists_active line 63

lemma OAI.Problem326.Affine.exists_common_pos_lt line 70

Source documentation

A finite collection of positive tolerances admits one strict common bound.

lemma exists_common_pos_lt {ι : Type uIota} (s : Finset ι) (E : ι → ℝ)
    (hE : ∀ i ∈ s, 0 < E i) (u : ℝ) (hu : 0 < u) :
    ∃ δ : ℝ, 0 < δ ∧ δ < u ∧ ∀ i ∈ s, δ < E i := by
…

lemma OAI.Problem326.Affine.exists_threshold line 90
Source documentation
The choice of the next type threshold in the fixed-minimum induction. The upper endpoint can itself be the preceding threshold, giving a decreasing sequence while only querying finitely many tolerance values.
```
lemma exists_threshold {ι : Type uIota} (s : Finset ι) (E : ι → ℝ)
    (hE : ∀ i ∈ s, 0 < E i) {t u : ℝ} (htu : t < u) :
    ∃ β : ℝ, t < β ∧ β < u ∧ ∀ i ∈ s, β - t < E i := by
…
```
lemma OAI.Problem326.Affine.eq_const_of_minimum_at_upper line 98
lemma OAI.Problem326.Affine.eq_const_of_minimum_one line 103

lemma OAI.Problem326.Affine.norm_sub_lt_of_support line 111

Source documentation

Final coordinate estimate for types with a further threshold.

lemma norm_sub_lt_of_support {d : ℕ} (U : Finset (Fin d))
    {p r : Fin d → ℝ} {t β ε : ℝ} (hε : 0 < ε)
    (hin : ∀ i ∈ U, |p i - r i| < ε)
    (hout : ∀ i ∉ U, r i = t ∧ t ≤ p i ∧ p i ≤ β)
    (hβ : β - t < ε) : ‖p - r‖ < ε := by
…

lemma OAI.Problem326.Affine.off_support_eq_minimum line 126

Source documentation

For the last type, the unique unraised coordinate realizes the minimum.

lemma off_support_eq_minimum {d : ℕ} (U : Finset (Fin d))
    {p : Fin d → ℝ} {t : ℝ} (hm : HasMinimum p t)
    (hin : ∀ i ∈ U, t < p i) (hcomp : ∀ i ∉ U, ∀ j ∉ U, i = j) :
    ∀ i ∉ U, p i = t := by
…

Mentions: OAI.Problem326.Affine.HasMinimum

lemma OAI.Problem326.Affine.singleton_approximates_one line 140
Source documentation
The singleton family verifies the fixed-minimum base case in dimension one.
```
lemma singleton_approximates_one (a b t : ℝ) (E : (Fin 1 → ℝ) → ℝ)
    (hE : 0 < E (fun _ => t)) :
    ApproximatesAtMinimum {⟨fun _ => t, fun _ => 0⟩} a b t E := by
…
```
Mentions: OAI.Problem326.Affine.ApproximatesAtMinimum
lemma OAI.Problem326.Affine.singleton_approximates_upper line 151
Source documentation
The other singleton base case works in every dimension at the upper corner.
```
lemma singleton_approximates_upper {d : ℕ} (a b : ℝ)
    (E : (Fin d → ℝ) → ℝ) (hE : 0 < E (fun _ => b)) :
    ApproximatesAtMinimum {⟨fun _ => b, fun _ => 0⟩} a b b E := by
…
```
Mentions: OAI.Problem326.Affine.ApproximatesAtMinimum