PlateauCertificate.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem326.AffineActive line 12

Source documentation

Pairwise comparison formulation of activity in a finite affine family.

def AffineActive {d : ℕ} {Λ : Type uLambda}
    (r : Λ → Fin d → ℝ) (c : Λ → ℝ) (x : Fin d → ℝ) (j : Λ) : Prop :=
…

theorem OAI.Problem326.exists_affineActive line 17

Source documentation

Every finite nonempty affine family has an active label, including at ties.

theorem exists_affineActive {d : ℕ} {Λ : Type uLambda} [Fintype Λ] [Nonempty Λ]
    (r : Λ → Fin d → ℝ) (c : Λ → ℝ) (x : Fin d → ℝ) :
    ∃ j, AffineActive r c x j := by
…

Mentions: OAI.Problem326.AffineActive

theorem OAI.Problem326.affineActive_slope_eq_zero line 26

Source documentation

Coordinate sign gaps force any initially active slope to vanish.

theorem affineActive_slope_eq_zero {d : ℕ} {Λ : Type uLambda}
    (r : Λ → Fin d → ℝ) (c : Λ → ℝ) (x p : Fin d → ℝ) {H : ℝ}
    (hp : ∀ i, |p i| < H)
    (hgap : ∀ j, AffineActive r c x j → ∀ i, r j i ≠ 0 → H ≤ |p i|)
    {j : Λ} (hj : AffineActive r c x j) : r j = 0 := by
…

Mentions: OAI.Problem326.AffineActive

theorem OAI.Problem326.constant_branch_plateau line 37

Source documentation

The plateau cut out by a constant active branch contains the initial point. This also records that plateau membership is exactly activity of that branch.

theorem constant_branch_plateau {d : ℕ} {Λ : Type uLambda}
    (r : Λ → Fin d → ℝ) (c : Λ → ℝ) (x₀ : Fin d → ℝ)
    {j : Λ} (hr : r j = 0) (hj : AffineActive r c x₀ j) :
    x₀ ∈ {x | ∀ k, c j ≤ dot (r k) x + c k} ∧
      ∀ x, (∀ k, c j ≤ dot (r k) x + c k) ↔ AffineActive r c x j := by
…

Mentions: OAI.Problem326.AffineActive, OAI.Problem326.dot

theorem OAI.Problem326.constant_branch_not_active_on_boundary line 53

Source documentation

A zero-slope branch cannot be active at an exponent-box boundary point when the active-label approximation has radius strictly below one there.

theorem constant_branch_not_active_on_boundary {d : ℕ} {Λ : Type uLambda}
    (r : Λ → Fin d → ℝ) (c : Λ → ℝ) (X : (Fin d → ℝ) → (Fin d → ℝ))
    (E : (Fin d → ℝ) → ℝ) (hE : E 0 ≤ 1 / 2)
    {j : Λ} (hr : r j = 0) {p : Fin d → ℝ}
    (hboundary : ∃ i, |p i| = 1)
    (happrox : AffineActive r c (X p) j → ∀ i, |p i - r j i| < E (r j)) :
    ¬ AffineActive r c (X p) j := by
…

Mentions: OAI.Problem326.AffineActive

theorem OAI.Problem326.exists_constant_plateau_certificate line 67

Source documentation

Combined algebraic certificate used before the geometric trapping step.

theorem exists_constant_plateau_certificate {d : ℕ} {Λ : Type uLambda}
    [Fintype Λ] [Nonempty Λ]
    (r : Λ → Fin d → ℝ) (c : Λ → ℝ) (x₀ p₀ : Fin d → ℝ) {H : ℝ}
    (hp₀ : ∀ i, |p₀ i| < H)
    (hgap : ∀ j, AffineActive r c x₀ j → ∀ i, r j i ≠ 0 → H ≤ |p₀ i|) :
    ∃ j : Λ, r j = 0 ∧
      x₀ ∈ {x | ∀ k, c j ≤ dot (r k) x + c k} ∧
      ∀ x, (∀ k, c j ≤ dot (r k) x + c k) ↔ AffineActive r c x j := by
…

Mentions: OAI.Problem326.AffineActive, OAI.Problem326.dot