ThreePrimeCubicStability.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.ThreePrimeCubicStability.norm_cube_sub_cube_le line 12
Source documentation
Exact polynomial factorization gives a norm estimate without choosing common upper bounds for the two arguments.
```
theorem norm_cube_sub_cube_le (z w : ℂ) :
    ‖z ^ 3 - w ^ 3‖ ≤ ‖z - w‖ * (‖z‖ ^ 2 + ‖z‖ * ‖w‖ + ‖w‖ ^ 2) := by
…
```

theorem OAI.Problem337.ThreePrimeCubicStability.norm_cube_sub_cube_le_of_bounds line 24

Source documentation

Asymmetric uniform error estimate for two cubic expressions.

theorem norm_cube_sub_cube_le_of_bounds (z w : ℂ) {E M N : ℝ}
    (hE : 0 ≤ E) (hM : 0 ≤ M) (_hN : 0 ≤ N)
    (hdiff : ‖z - w‖ ≤ E) (hz : ‖z‖ ≤ M) (hw : ‖w‖ ≤ N) :
    ‖z ^ 3 - w ^ 3‖ ≤ E * (M ^ 2 + M * N + N ^ 2) := by
…

theorem OAI.Problem337.ThreePrimeCubicStability.norm_cubic_error_integral_le line 38

Source documentation

Cubic approximation error integrated over an arbitrary finite-measure set. No measurability or integrability is silently assumed: the Bochner norm bound is valid also when the displayed integral is defined by zero.

theorem norm_cubic_error_integral_le {α : Type*} [MeasurableSpace α]
    {μ : Measure α} {s : Set α} (hs : μ s < ∞)
    (F G ψ : α → ℂ) {E M N : ℝ}
    (hE : 0 ≤ E) (hM : 0 ≤ M) (hN : 0 ≤ N)
    (hdiff : ∀ x ∈ s, ‖F x - G x‖ ≤ E)
    (hF : ∀ x ∈ s, ‖F x‖ ≤ M) (hG : ∀ x ∈ s, ‖G x‖ ≤ N)
    (hψ : ∀ x ∈ s, ‖ψ x‖ ≤ 1) :
    ‖∫ x in s, (F x ^ 3 - G x ^ 3) * ψ x ∂μ‖ ≤
      E * (M ^ 2 + M * N + N ^ 2) * (μ s).toReal := by
…

Mentions: OAI.Problem337.F

theorem OAI.Problem337.ThreePrimeCubicStability.norm_cubic_error_integral_le_common line 58

Source documentation

A common amplitude bound gives the standard 3 E M² cubic error.

theorem norm_cubic_error_integral_le_common {α : Type*} [MeasurableSpace α]
    {μ : Measure α} {s : Set α} (hs : μ s < ∞)
    (F G ψ : α → ℂ) {E M : ℝ} (hE : 0 ≤ E) (hM : 0 ≤ M)
    (hdiff : ∀ x ∈ s, ‖F x - G x‖ ≤ E)
    (hF : ∀ x ∈ s, ‖F x‖ ≤ M) (hG : ∀ x ∈ s, ‖G x‖ ≤ M)
    (hψ : ∀ x ∈ s, ‖ψ x‖ ≤ 1) :
    ‖∫ x in s, (F x ^ 3 - G x ^ 3) * ψ x ∂μ‖ ≤
      3 * E * M ^ 2 * (μ s).toReal := by
…

Mentions: OAI.Problem337.F

theorem OAI.Problem337.ThreePrimeCubicStability.norm_cubic_integral_sub_le line 71

Source documentation

When the two cubic integrands are integrable, the error estimate controls the difference of their integrals, as required by major-arc approximation.

theorem norm_cubic_integral_sub_le {α : Type*} [MeasurableSpace α]
    {μ : Measure α} {s : Set α} (hs : μ s < ∞)
    (F G ψ : α → ℂ) {E M : ℝ} (hE : 0 ≤ E) (hM : 0 ≤ M)
    (hFi : IntegrableOn (fun x => F x ^ 3 * ψ x) s μ)
    (hGi : IntegrableOn (fun x => G x ^ 3 * ψ x) s μ)
    (hdiff : ∀ x ∈ s, ‖F x - G x‖ ≤ E)
    (hF : ∀ x ∈ s, ‖F x‖ ≤ M) (hG : ∀ x ∈ s, ‖G x‖ ≤ M)
    (hψ : ∀ x ∈ s, ‖ψ x‖ ≤ 1) :
    ‖(∫ x in s, F x ^ 3 * ψ x ∂μ) - (∫ x in s, G x ^ 3 * ψ x ∂μ)‖ ≤
      3 * E * M ^ 2 * (μ s).toReal := by
…

Mentions: OAI.Problem337.F

theorem OAI.Problem337.ThreePrimeCubicStability.norm_cubic_interval_error_le line 86

Source documentation

Oriented-interval version of cubic stability, independent of endpoint order.

theorem norm_cubic_interval_error_le (F G ψ : ℝ → ℂ) (a b : ℝ)
    {E M : ℝ} (hE : 0 ≤ E) (hM : 0 ≤ M)
    (hdiff : ∀ x ∈ Set.uIoc a b, ‖F x - G x‖ ≤ E)
    (hF : ∀ x ∈ Set.uIoc a b, ‖F x‖ ≤ M)
    (hG : ∀ x ∈ Set.uIoc a b, ‖G x‖ ≤ M)
    (hψ : ∀ x ∈ Set.uIoc a b, ‖ψ x‖ ≤ 1) :
    ‖∫ x in a..b, (F x ^ 3 - G x ^ 3) * ψ x‖ ≤
      3 * E * M ^ 2 * |b - a| := by
…

Mentions: OAI.Problem337.F