ActualSecondMomentParameters.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Exact normalization and uniform numerical losses for the configured second trace. The actual trace-to-path inequality is deliberately an explicit premise.

theorem OAI.Problem335.LowerParameters.configured_pathMean_eq line 18
Source documentation
The path mean for the balanced partition uses exactly the configured numbers of differentiation and multiplication layers.
```
theorem configured_pathMean_eq {L : ℕ} (hn : 4 ≤ L + 1) :
    pathMean (balancedLayer hn)
      ((a (L + 1) : ℝ) / v (L + 1))
      ((b (L + 1) : ℝ) / u (L + 1)) =
    ((a (L + 1) : ℝ) / v (L + 1)) ^ k (L + 1) *
      (1 + (b (L + 1) : ℝ) / u (L + 1)) ^ m (L + 1) := by
…
```
Mentions: OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.u, OAI.Problem335.LowerParameters.k, OAI.Problem335.LowerParameters.m
theorem OAI.Problem335.LowerParameters.rankMomentScale_eq_pathMean line 28
Source documentation
The common first-moment scale is the path count times the path mean.
```
theorem rankMomentScale_eq_pathMean {L : ℕ} (hn : 4 ≤ L + 1) :
    rankMomentScale (L + 1) = ((L + 1 : ℕ) : ℝ) ^ L *
      pathMean (balancedLayer hn)
        ((a (L + 1) : ℝ) / v (L + 1))
        ((b (L + 1) : ℝ) / u (L + 1)) := by
…
```
Mentions: OAI.Problem335.LowerParameters.rankMomentScale, OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.u
theorem OAI.Problem335.LowerParameters.configured_word_loss_le_exp line 38
Source documentation
The U-layer correction and the balanced-word factor cost at most ten square-root units in the exponent, without an occupation upper-loss factor.
```
theorem configured_word_loss_le_exp {n : ℕ} (hn : 16 ≤ n)
    (hbeta : beta n ≤ 2 / Real.sqrt (n : ℝ)) :
    (1 + beta n) ^ m n * Real.exp (8 * Real.sqrt (n : ℝ)) ≤
      Real.exp (10 * Real.sqrt (n : ℝ)) := by
…
```
Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.m
theorem OAI.Problem335.LowerParameters.configured_second_scale_identity line 51
Source documentation
Rearrangement of the actual path normalization, including the square of its path-count factor.
```
theorem configured_second_scale_identity {L : ℕ} (hn : 4 ≤ L + 1)
    (W : ℝ) :
    rankDimension (L + 1) *
        pathMean (balancedLayer hn)
          ((a (L + 1) : ℝ) / v (L + 1))
          ((b (L + 1) : ℝ) / u (L + 1)) ^ 2 *
        (((L + 1 : ℕ) : ℝ) ^ (2 * L) * W) =
      rankDimension (L + 1) * rankMomentScale (L + 1) ^ 2 * W := by
…
```
Mentions: OAI.Problem335.LowerParameters.rankDimension, OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.u, OAI.Problem335.LowerParameters.rankMomentScale

theorem OAI.Problem335.LowerParameters.configured_second_bound_of_path_bound line 64

Source documentation

Numerical endpoint consumed by the actual trace-to-relaxed-path assembly. There is only one source-dimension factor.

theorem configured_second_bound_of_path_bound {L : ℕ} (hn : 16 ≤ L + 1)
    (hbeta : beta (L + 1) ≤ 2 / Real.sqrt ((L + 1 : ℕ) : ℝ))
    (T : ℝ)
    (hT : T ≤ rankDimension (L + 1) *
      pathMean (balancedLayer (show 4 ≤ L + 1 by omega))
        ((a (L + 1) : ℝ) / v (L + 1))
        ((b (L + 1) : ℝ) / u (L + 1)) ^ 2 *
      ((1 + beta (L + 1)) ^ m (L + 1) *
        ((L + 1 : ℕ) : ℝ) ^ (2 * L) *
        Real.exp (8 * Real.sqrt ((L + 1 : ℕ) : ℝ)))) :
    T ≤ rankDimension (L + 1) * rankMomentScale (L + 1) ^ 2 *
      Real.exp (10 * Real.sqrt ((L + 1 : ℕ) : ℝ)) := by
…

Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.rankDimension, OAI.Problem335.LowerParameters.balancedLayer, OAI.Problem335.LowerParameters.a, OAI.Problem335.LowerParameters.v, OAI.Problem335.LowerParameters.b, OAI.Problem335.LowerParameters.u, OAI.Problem335.LowerParameters.m, OAI.Problem335.LowerParameters.rankMomentScale

theorem OAI.Problem335.LowerParameters.exists_second_moment_parameter_cutoff line 91
Source documentation
A single absolute threshold discharges every numerical premise of the configured second-moment normalization.
```
theorem exists_second_moment_parameter_cutoff :
    ∃ N : ℕ, ∀ n : ℕ, N ≤ n →
      16 ≤ n ∧ beta n ≤ 2 / Real.sqrt (n : ℝ) ∧
        (1 + beta n) ^ m n * Real.exp (8 * Real.sqrt (n : ℝ)) ≤
          Real.exp (10 * Real.sqrt (n : ℝ)) := by
…
```
Mentions: OAI.Problem335.LowerParameters.beta, OAI.Problem335.LowerParameters.m