ReciprocalBox.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Geometry of the reciprocal box used by the affine certificate.

theorem OAI.Problem326.mem_interior_coordinate_box_iff line 15
Source documentation
The interior of a finite coordinate box is obtained by making every coordinate inequality strict.
```
theorem mem_interior_coordinate_box_iff
    {ι : Type uIota} [Finite ι] {a b x : ι → ℝ} :
    x ∈ interior (Icc a b) ↔ ∀ i, a i < x i ∧ x i < b i := by
…
```

theorem OAI.Problem326.mem_interior_reciprocal_box_iff line 23

Source documentation

A positive state has every logarithmic exponent strictly between -1 and 1 exactly when it belongs to the interior of the reciprocal box.

theorem mem_interior_reciprocal_box_iff
    {ι : Type uIota} [Finite ι] {x : ι → ℝ} {h : ℝ}
    (hh : 0 < h) (hh1 : h < 1) (hx : ∀ i, 0 < x i) :
    x ∈ interior (Icc (fun _ => h) (fun _ => h⁻¹)) ↔
      ∀ i, |Real.log (x i) / Real.log h| < 1 := by
…

theorem OAI.Problem326.isCompact_reciprocal_box line 32
Source documentation
Closed reciprocal boxes in finitely many real coordinates are compact.
```
theorem isCompact_reciprocal_box {ι : Type uIota} [Finite ι] (h : ℝ) :
    IsCompact (Icc (fun _ : ι => h) (fun _ => h⁻¹)) := by
…
```

theorem OAI.Problem326.reciprocal_box_log_coordinates line 39

Source documentation

Every point in a positive reciprocal box is positive, and its unique logarithmic exponents lie in the closed unit cube.

theorem reciprocal_box_log_coordinates
    {ι : Type uIota} {x : ι → ℝ} {h : ℝ} (hh : 0 < h) (hh1 : h < 1)
    (hx : x ∈ Icc (fun _ => h) (fun _ => h⁻¹)) :
    (∀ i, 0 < x i) ∧
      (∀ i, |Real.log (x i) / Real.log h| ≤ 1) ∧
      (∀ i, h ^ (Real.log (x i) / Real.log h) = x i) := by
…

theorem OAI.Problem326.reciprocal_box_frontier_coordinate line 54

Source documentation

A boundary point of the reciprocal box has a logarithmic coordinate of absolute value one. This is the boundary obstruction used to exclude an active zero-slope label.

theorem reciprocal_box_frontier_coordinate
    {ι : Type uIota} [Finite ι] {x : ι → ℝ} {h : ℝ}
    (hh : 0 < h) (hh1 : h < 1)
    (hx : x ∈ frontier (Icc (fun _ => h) (fun _ => h⁻¹))) :
    ∃ i, |Real.log (x i) / Real.log h| = 1 := by
…