MomentLossParameters.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem335.LowerParameters.first_moment_loss_exp_lower line 10
Source documentation
The first-moment loss can be expressed at the common square-root scale.
```
theorem first_moment_loss_exp_lower {n : ℕ} (hn : 16 ≤ n) :
    Real.exp (-64 * Real.sqrt (n : ℝ)) ≤
      Real.exp (-64 / Real.sqrt (n : ℝ)) := by
…
```
theorem OAI.Problem335.LowerParameters.u_layer_correction_le_exp line 20
Source documentation
The actual U-layer correction has square-root exponential cost.
```
theorem u_layer_correction_le_exp {n : ℕ} (hn : 16 ≤ n)
    (hbeta : beta n ≤ 2 / Real.sqrt (n : ℝ)) :
    (1 + beta n) ^ m n ≤ Real.exp (2 * Real.sqrt (n : ℝ)) := by
…
```
Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.m

theorem OAI.Problem335.LowerParameters.second_moment_loss_exp_upper line 42

Source documentation

Consolidation of occupation, U-layer, and balanced-word losses.

theorem second_moment_loss_exp_upper {n : ℕ} (hn : 16 ≤ n)
    (hbeta : beta n ≤ 2 / Real.sqrt (n : ℝ)) :
    Real.exp (64 / Real.sqrt (n : ℝ)) * (1 + beta n) ^ m n *
      Real.exp (8 * Real.sqrt (n : ℝ)) ≤
      Real.exp (74 * Real.sqrt (n : ℝ)) := by
…

Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.m