SourcePredictionParameters.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Numerical parameters for the source prediction comparison. All thresholds are uniform in the top family, phase dimension and mass.

theorem OAI.LipschitzHilbert.eventually_source_mass_error_small line 15
theorem OAI.LipschitzHilbert.eventually_source_path_errors_small line 36
Source documentation
Both relative errors used by the actual path comparison are smaller than the chosen prediction error, uniformly in the block length.
```
theorem eventually_source_path_errors_small (D : ℝ) (hD : 0 ≤ D) :
    ∀ᶠ L : ℝ in atTop, ∀ (Kw Z : ℝ) (steps : ℕ),
      1 ≤ Kw → 0 ≤ Z → Z ≤ 2*L^2 → (steps:ℝ) ≤ L^2 →
      let δ := (5*D/Kw)/Real.sqrt (SourceParameters.step L)
…
```
Mentions: OAI.LipschitzHilbert.SourceParameters.step

theorem OAI.LipschitzHilbert.prediction_budget_of_subpower line 65

Source documentation

A single small positive power controls the path comparison, the convex blend and the mesh/mixture error.

theorem prediction_budget_of_subpower {G V F : ℝ}
    (hG : 1 ≤ G) (hV0 : 0 ≤ V) (hV : V ≤ G^(1/128:ℝ)) (hF : 0 ≤ F)
    (hsmall : 96 ≤ G^(7/128:ℝ)) (hcost : 27650+F ≤ G^(3/128:ℝ)) :
    Real.exp (48*V*G^(-(1/8:ℝ))) ≤ 2 ∧
      96*V*G^(-(1/8:ℝ)) ≤ G^(-(1/16:ℝ)) ∧
      27648*V^2*G^(-(1/8:ℝ))+(2+F)*V*G^(-(1/16:ℝ)) ≤ G^(-(1/32:ℝ)) := by
…

theorem OAI.LipschitzHilbert.eventually_source_prediction_parameters line 122

Source documentation

The source values p=sqrt L, epsilon=G^(-1/8) and theta=G^(-1/16) meet the complete dominant-comparison budget.

theorem eventually_source_prediction_parameters (C F : ℝ) (_hC : 0 ≤ C) (hF : 0 ≤ F) :
    ∀ᶠ L : ℝ in atTop, ∀ D N : ℝ,
      1 ≤ D → 0 < N → Real.log N ≤ 2*L →
      let p := Real.sqrt L
…

theorem OAI.LipschitzHilbert.balanced_prediction_cost_le_dominant line 169
Source documentation
The balanced branch fits inside the same error budget as the dominant branch, so the final marked-cell exponent is common to both.
```
theorem balanced_prediction_cost_le_dominant {p K ε θ : ℝ}
    (hp : 1 ≤ p) (hK : 1 ≤ K) (hε : 0 ≤ ε) :
    6*p*ε*K+2*θ*(p*K) ≤
      12*24^2*p^2*(2*K)^2*ε+θ*(p*(2*K)) := by
…
```