SmallParameter.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Simultaneous small-parameter choice for the affine trapping construction.

theorem OAI.Problem326.exists_small_parameter line 15

Source documentation

The final small parameter is chosen only after the positive gap is fixed. The rate type may be empty; the rate inequalities are then vacuous.

theorem exists_small_parameter {ι : Type uIota} {η : Type uEta} [Fintype ι] [Fintype η]
    (c : ι → ℝ) (κ : η → ℝ) {H h₀ : ℝ}
    (hH : 0 < H) (hh₀ : 0 < h₀) (hκ : ∀ e, 0 < κ e) :
    ∃ h : ℝ, 0 < h ∧ h < h₀ ∧ h < 1 ∧
      (∀ i, |c i / Real.log h| < H) ∧
      ∀ e, h ^ H * (∑ e, κ e) < κ e := by
…

theorem OAI.Problem326.rpow_log_ratio line 44
Source documentation
Logarithmic coordinates reconstruct a positive state for a base in (0,1).
```
theorem rpow_log_ratio {h x : ℝ} (hh : 0 < h) (hh1 : h < 1) (hx : 0 < x) :
    h ^ (Real.log x / Real.log h) = x := by
…
```

theorem OAI.Problem326.exists_initial_exponent_parameter line 51

Source documentation

Simultaneous initial-exponent and rate separation with explicit reconstruction.

theorem exists_initial_exponent_parameter {ι : Type uIota} {η : Type uEta} [Fintype ι] [Fintype η]
    (x₀ : ι → ℝ) (κ : η → ℝ) {H h₀ : ℝ}
    (hx₀ : ∀ i, 0 < x₀ i) (hH : 0 < H) (hh₀ : 0 < h₀) (hκ : ∀ e, 0 < κ e) :
    ∃ (h : ℝ) (p : ι → ℝ), 0 < h ∧ h < h₀ ∧ h < 1 ∧
      (∀ i, |p i| < H) ∧ (∀ i, h ^ (p i) = x₀ i) ∧
      ∀ e, h ^ H * (∑ e, κ e) < κ e := by
…

theorem OAI.Problem326.tendsto_log_coordinate_div_log line 75
Source documentation
The logarithmic exponent of a fixed coordinate tends to zero when the base tends to zero from the right. Positivity of the coordinate is not needed for this limit (but is needed to reconstruct it from its exponent).
```
theorem tendsto_log_coordinate_div_log (x : ℝ) :
    Tendsto (fun h : ℝ => Real.log x / Real.log h) (𝓝[>] (0 : ℝ)) (𝓝 0) :=
…
```
theorem OAI.Problem326.tendsto_positive_rpow_nhdsGT_zero line 80
Source documentation
A positive fixed power tends to zero, including on the positive side.
```
theorem tendsto_positive_rpow_nhdsGT_zero {H : ℝ} (hH : 0 < H) :
    Tendsto (fun h : ℝ => h ^ H) (𝓝[>] (0 : ℝ)) (𝓝 0) := by
…
```

theorem OAI.Problem326.exists_small_parameter_for_rates line 89

Source documentation

Choose one small parameter after all slopes and their positive separation have already been fixed. All coordinate and reaction constraints hold simultaneously; an empty reaction type causes no exceptional case.

theorem exists_small_parameter_for_rates
    {ι : Type uIota} {E : Type uE} [Finite ι] [Fintype E]
    (x0 : ι → ℝ) (κ : E → ℝ) {h0 H : ℝ}
    (hh0 : 0 < h0) (hH : 0 < H) (hκ : ∀ e, 0 < κ e) :
    ∃ h : ℝ, 0 < h ∧ h < h0 ∧ h < 1 ∧
      (∀ i, |Real.log (x0 i) / Real.log h| < H) ∧
      (∀ e, h ^ H * (∑ f, κ f) < κ e) := by
…

theorem OAI.Problem326.rpow_log_coordinate line 119
Source documentation
Positive coordinates are recovered exactly from their logarithmic exponents for a base strictly between zero and one.
```
theorem rpow_log_coordinate {h x : ℝ}
    (hh : 0 < h) (hh1 : h < 1) (hx : 0 < x) :
    h ^ (Real.log x / Real.log h) = x := by
…
```
theorem OAI.Problem326.abs_log_coordinate_lt_one_iff line 126
Source documentation
The open symmetric exponent interval describes the interior of the positive reciprocal box in each coordinate.
```
theorem abs_log_coordinate_lt_one_iff {h x : ℝ}
    (hh : 0 < h) (hh1 : h < 1) (hx : 0 < x) :
    |Real.log x / Real.log h| < 1 ↔ h < x ∧ x < h⁻¹ := by
…
```
theorem OAI.Problem326.abs_log_coordinate_le_one_iff line 137
Source documentation
The closed symmetric exponent interval describes the closed positive reciprocal box in each coordinate.
```
theorem abs_log_coordinate_le_one_iff {h x : ℝ}
    (hh : 0 < h) (hh1 : h < 1) (hx : 0 < x) :
    |Real.log x / Real.log h| ≤ 1 ↔ h ≤ x ∧ x ≤ h⁻¹ := by
…
```