Taylor.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.HarmonicCounterexample.PulseTaylor.quadratic_remainder line 18

Source documentation

Two applications of the mean value theorem, retaining the derivative remainder needed for C1 control of a slow pulse.

theorem quadratic_remainder {f f' f'' : ℝ → ℝ} {C : ℝ}
    (hC : 0 ≤ C)
    (hf : ∀ x ∈ Icc (1/2:ℝ) (3/2),HasDerivAt f (f' x) x)
    (hf' : ∀ x ∈ Icc (1/2:ℝ) (3/2),HasDerivAt f' (f'' x) x)
    (hb : ∀ x ∈ Icc (1/2:ℝ) (3/2),|f'' x| ≤ C) :
    ∀ q ∈ Icc (1/2:ℝ) (3/2),
      |f q-f 1-(q-1)*f' 1| ≤ C*(q-1)^2 ∧ |f' q-f' 1| ≤ C*|q-1| := by
…

theorem OAI.HarmonicCounterexample.PulseTaylor.rpow_remainder line 56
Source documentation
The scalar power appearing in the genuine Berger angular operator has a uniform quadratic value remainder AND a uniform linear derivative remainder.
```
theorem rpow_remainder (r : ℝ) : ∃ C : ℝ,0 ≤ C ∧
    ∀ q ∈ Icc (1/2:ℝ) (3/2),
      |q^r-1-r*(q-1)| ≤ C*(q-1)^2 ∧
      |r*q^(r-1)-r| ≤ C*|q-1| := by
…
```
def OAI.HarmonicCounterexample.PulseTaylor.angular line 97
Source documentation
The exact Berger angular coefficient, with b=B_l Id and D=D_J². Here r=1/m, and the outer scalar a^{-2} is applied separately.
```
def angular (r : ℝ) (b D : E) (q : ℝ) : E :=
…
```
Mentions: OAI.HarmonicCounterexample.b
def OAI.HarmonicCounterexample.PulseTaylor.angularD line 100
lemma OAI.HarmonicCounterexample.PulseTaylor.angular_eq_berger line 103
lemma OAI.HarmonicCounterexample.PulseTaylor.angular_hasDerivAt line 111
lemma OAI.HarmonicCounterexample.PulseTaylor.angular_one line 119
lemma OAI.HarmonicCounterexample.PulseTaylor.angularD_one line 120
theorem OAI.HarmonicCounterexample.PulseTaylor.angular_remainder line 125
Source documentation
Genuine uniform C1 Taylor control of the angular operator, rather than an endpoint assertion or a formal Taylor expansion taken as an axiom.
```
theorem angular_remainder (r : ℝ) (b D : E) : ∃ C : ℝ,0 ≤ C ∧
    ∀ q ∈ Icc (1/2:ℝ) (3/2),
      ‖angular r b D q-b-(q-1) • (r • b+D)‖ ≤ C*(q-1)^2 ∧
      ‖angularD r b D q-(r • b+D)‖ ≤ C*|q-1| := by
…
```
Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.PulseTaylor.angular, OAI.HarmonicCounterexample.PulseTaylor.angularD
lemma OAI.HarmonicCounterexample.PulseTaylor.scaled_value_error line 177
Source documentation
Separation of the slowly varying scale from the small pulse. In the source α=a(t)^{-2}, β=a_*^{-2}, δ=z/T.
```
lemma scaled_value_error {F b L : E} {α β δ C : ℝ}
    (hF : ‖F-b-δ • L‖ ≤ C*δ^2) :
    ‖α • F-α • b-(β*δ) • L‖ ≤
      |α| *C*δ^2+|α-β| *|δ| *‖L‖ := by
…
```
Mentions: OAI.HarmonicCounterexample.b
lemma OAI.HarmonicCounterexample.PulseTaylor.scaled_deriv_error line 189

theorem OAI.HarmonicCounterexample.PulseTaylor.berger_slow_pulse_remainders line 217

Source documentation

Uniform value AND parameter-direction remainders for the exact slowly scaled Berger operator. No coefficient approximation is a hypothesis.

theorem berger_slow_pulse_remainders (r : ℝ) (b D : E) {M Z : ℝ}
    (hM : 0 ≤ M) (hZ : 0 ≤ Z) :
    ∃ C : ℝ,0 ≤ C ∧ ∀ α β δ τ z zh : ℝ,
      0 ≤ δ → 0 ≤ τ → |α| ≤ M → |α-β| ≤ δ → |z| ≤ Z → |zh| ≤ Z →
      1+τ*z ∈ Set.Icc (1/2:ℝ) (3/2) →
      ‖α • angular r b D (1+τ*z)-α • b-(β*τ*z) • (r • b+D)‖ ≤ C*(δ*τ+τ^2) ∧
      ‖(τ*zh) • (α • angularD r b D (1+τ*z)-β • (r • b+D))‖ ≤ C*(δ*τ+τ^2) := by
…

Mentions: OAI.HarmonicCounterexample.b, OAI.HarmonicCounterexample.PulseTaylor.angular, OAI.HarmonicCounterexample.PulseTaylor.angularD