InverseJetBounds.lean`

20 declarations, 0 contain sorry, 0 declared as axioms

Higher derivatives of inverse fields

The resolvent identity subtracts the value of the original field at the base point before the higher product estimate is applied. Its zeroth derivative is then zero, so the inverse recurrence has no occurrence of the current unknown derivative on the right. These are actual iterated Fréchet derivatives in a real Banach algebra, including bounded operators.

theorem OAI.RegularPointCoordinates.inverse_field_resolvent line 29

Source documentation

The resolvent identity in the order needed for a one-sided inverse.

theorem inverse_field_resolvent {J K : X → A} {s : Set X} {x : X}
    (hleft : K x * J x = 1)
    (hright : ∀ y ∈ s, J y * K y = 1) :
    Set.EqOn K (fun y => K x - K x * ((J y - J x) * K y)) s := by
…

theorem OAI.RegularPointCoordinates.iteratedFDerivWithin_sub_basepoint line 41

Source documentation

At positive orders, subtracting the value at the base point does not change the iterated derivative.

theorem iteratedFDerivWithin_sub_basepoint {J : X → A} {s : Set X} {x : X}
    {n : ℕ} (hJ : ContDiffWithinAt ℝ n J s x)
    (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) (hn : n ≠ 0) :
    iteratedFDerivWithin ℝ n (fun y => J y - J x) s x =
      iteratedFDerivWithin ℝ n J s x := by
…

theorem OAI.RegularPointCoordinates.norm_iteratedFDerivWithin_inverse_field_le line 53

Source documentation

A higher inverse derivative is bounded by strictly lower inverse derivatives. The smoothness and inverse identities are explicit.

theorem norm_iteratedFDerivWithin_inverse_field_le
    {J K : X → A} {s : Set X} {x : X} {n : ℕ}
    (hJ : ContDiffOn ℝ n J s) (hK : ContDiffOn ℝ n K s)
    (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) (hn : 0 < n)
    (hleft : K x * J x = 1) (hright : ∀ y ∈ s, J y * K y = 1) :
    ‖iteratedFDerivWithin ℝ n K s x‖ ≤ ‖K x‖ *
      ∑ i ∈ Finset.Icc 1 n, (n.choose i : ℝ) *
        ‖iteratedFDerivWithin ℝ i J s x‖ *
        ‖iteratedFDerivWithin ℝ (n - i) K s x‖ := by
…

theorem OAI.RegularPointCoordinates.contDiffOn_ringInverse_field line 112

Source documentation

A unit-valued smooth field has a smooth inverse field on the same set.

theorem contDiffOn_ringInverse_field [CompleteSpace A]
    {J : X → A} {s : Set X} {n : ℕ∞ω}
    (hJ : ContDiffOn ℝ n J s) (hunit : ∀ y ∈ s, IsUnit (J y)) :
    ContDiffOn ℝ n (fun y => Ring.inverse (J y)) s := by
…

theorem OAI.RegularPointCoordinates.norm_iteratedFDerivWithin_ringInverse_le line 123

Source documentation

The preceding recurrence for the genuine inverse in a Banach algebra.

theorem norm_iteratedFDerivWithin_ringInverse_le [CompleteSpace A]
    {J : X → A} {s : Set X} {x : X} {n : ℕ}
    (hJ : ContDiffOn ℝ n J s) (hunit : ∀ y ∈ s, IsUnit (J y))
    (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) (hn : 0 < n) :
    ‖iteratedFDerivWithin ℝ n (fun y => Ring.inverse (J y)) s x‖ ≤
      ‖Ring.inverse (J x)‖ * ∑ i ∈ Finset.Icc 1 n, (n.choose i : ℝ) *
        ‖iteratedFDerivWithin ℝ i J s x‖ *
        ‖iteratedFDerivWithin ℝ (n - i) (fun y => Ring.inverse (J y)) s x‖ := by
…

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_ringInverse_le line 138

Source documentation

The pointwise recurrence requires invertibility only at the base point: continuity supplies an invertible neighborhood.

theorem norm_iteratedFDeriv_ringInverse_le [CompleteSpace A]
    {J : X → A} {x : X} {n : ℕ}
    (hJ : ContDiffAt ℝ n J x) (hunit : IsUnit (J x)) (hn : 0 < n) :
    ‖iteratedFDeriv ℝ n (fun y => Ring.inverse (J y)) x‖ ≤
      ‖Ring.inverse (J x)‖ * ∑ i ∈ Finset.Icc 1 n, (n.choose i : ℝ) *
        ‖iteratedFDeriv ℝ i J x‖ *
        ‖iteratedFDeriv ℝ (n - i) (fun y => Ring.inverse (J y)) x‖ := by
…

def OAI.RegularPointCoordinates.jetCoefficientScale line 157
Source documentation
Exponential and factorial scaling for the coefficient of order m.
```
def jetCoefficientScale (B : ℝ) (m : ℕ) : ℝ :=
…
```
theorem OAI.RegularPointCoordinates.jetCoefficientScale_pos line 160
theorem OAI.RegularPointCoordinates.jetCoefficientScale_zero line 165
theorem OAI.RegularPointCoordinates.choose_mul_jetCoefficientScale line 170
Source documentation
Binomial coefficients exactly cancel the factorial scaling; there is no loss in the exponential base.
```
theorem choose_mul_jetCoefficientScale {B : ℝ} {m i : ℕ} (hi : i ≤ m) :
    (m.choose i : ℝ) * jetCoefficientScale B i * jetCoefficientScale B (m - i) =
      jetCoefficientScale B m := by
…
```
Mentions: OAI.RegularPointCoordinates.jetCoefficientScale

theorem OAI.RegularPointCoordinates.normalized_inverse_jet_recurrence line 186

Source documentation

A binomial inverse recurrence becomes the convolution recurrence after division by its exact exponential-factorial scaling.

theorem normalized_inverse_jet_recurrence {B H : ℝ} {j k : ℕ → ℝ}
    (hB : 0 < B) (hH : 0 ≤ H) (hk : ∀ m, 0 ≤ k m)
    (hj : ∀ m, 0 < m → j m ≤ factorialMajorant m * jetCoefficientScale B m)
    (hrec : ∀ m, 0 < m → k m ≤ H * ∑ i ∈ Finset.Icc 1 m,
      (m.choose i : ℝ) * j i * k (m - i))
    {m : ℕ} (hm : 0 < m) :
    k m / jetCoefficientScale B m ≤ H * ∑ i ∈ Finset.Icc 1 m,
      factorialMajorant i * (k (m - i) / jetCoefficientScale B (m - i)) := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

theorem OAI.RegularPointCoordinates.normalized_inverse_jet_hasMajorant line 216

Source documentation

The normalized inverse recurrence has the form required by the factorial majorant, including its zeroth-order endpoint.

theorem normalized_inverse_jet_hasMajorant {B D : ℝ} {j k : ℕ → ℝ}
    (hB : 0 < B) (hD : 0 ≤ D) (hk : ∀ m, 0 ≤ k m)
    (hkzero : k 0 ≤ Real.sqrt D)
    (hj : ∀ m, 0 < m → j m ≤ factorialMajorant m * jetCoefficientScale B m)
    (hrec : ∀ m, 0 < m → k m ≤ Real.sqrt D * ∑ i ∈ Finset.Icc 1 m,
      (m.choose i : ℝ) * j i * k (m - i)) :
    HasInverseMajorantRecurrence factorialMajorant
      (fun m => k m / jetCoefficientScale B m) D := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale, OAI.RegularPointCoordinates.HasInverseMajorantRecurrence

theorem OAI.RegularPointCoordinates.inverse_jet_uniform_bound line 250

Source documentation

Uniform inverse bounds for every order, with exactly the original exponential base and one order-independent constant.

theorem inverse_jet_uniform_bound {D : ℝ} (hD : 1 ≤ D) :
    ∃ C : ℝ, Real.sqrt D ≤ C ∧ 2 * D ≤ C ∧ ∀ B : ℝ, 0 < B → ∀ j k : ℕ → ℝ,
      (∀ m, 0 ≤ k m) → k 0 ≤ Real.sqrt D →
      (∀ m, 0 < m → j m ≤ factorialMajorant m * jetCoefficientScale B m) →
      (∀ m, 0 < m → k m ≤ Real.sqrt D * ∑ i ∈ Finset.Icc 1 m,
        (m.choose i : ℝ) * j i * k (m - i)) →
      ∀ m, k m ≤ C * factorialMajorant m * jetCoefficientScale B m := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

theorem OAI.RegularPointCoordinates.clm_apply_factorialMajorant_bound line 267

Source documentation

Applying a field of operators preserves the same factorial weights. This is the product estimate used for the coordinate increment.

theorem clm_apply_factorialMajorant_bound
    {F G : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
    [NormedAddCommGroup G] [NormedSpace ℝ G]
    {f : X → F →L[ℝ] G} {g : X → F} {s : Set X} {x : X}
    {B C D : ℝ} {m : ℕ} (hB : 0 < B) (hC : 0 ≤ C) (hD : 0 ≤ D)
    (hf : ContDiffOn ℝ m f s) (hg : ContDiffOn ℝ m g s)
    (hs : UniqueDiffOn ℝ s) (hx : x ∈ s)
    (hfbound : ∀ i, i ≤ m → ‖iteratedFDerivWithin ℝ i f s x‖ ≤
      C * factorialMajorant i * jetCoefficientScale B i)
    (hgbound : ∀ i, i ≤ m → ‖iteratedFDerivWithin ℝ i g s x‖ ≤
      D * factorialMajorant i * jetCoefficientScale B i) :
    ‖iteratedFDerivWithin ℝ m (fun y => f y (g y)) s x‖ ≤
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

theorem OAI.RegularPointCoordinates.ringInverse_iteratedFDerivWithin_uniform_bound line 314

Source documentation

Actual higher derivatives of the inverse of a unit-valued Banach algebra field satisfy the factorial majorant without changing B. The same constant works for every field, set, and base point.

theorem ringInverse_iteratedFDerivWithin_uniform_bound [CompleteSpace A]
    {D : ℝ} (hD : 1 ≤ D) :
    ∃ C : ℝ, Real.sqrt D ≤ C ∧ 2 * D ≤ C ∧
      ∀ (B : ℝ), 0 < B → ∀ (J : X → A) (s : Set X) (x : X),
      (∀ m : ℕ, ContDiffOn ℝ m J s) → (∀ y ∈ s, IsUnit (J y)) →
      UniqueDiffOn ℝ s → x ∈ s → ‖Ring.inverse (J x)‖ ≤ Real.sqrt D →
      (∀ m, 0 < m → ‖iteratedFDerivWithin ℝ m J s x‖ ≤
        factorialMajorant m * jetCoefficientScale B m) →
      ∀ m, ‖iteratedFDerivWithin ℝ m (fun y => Ring.inverse (J y)) s x‖ ≤
        C * factorialMajorant m * jetCoefficientScale B m := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

theorem OAI.RegularPointCoordinates.ringInverse_iteratedFDeriv_uniform_bound line 342

Source documentation

Pointwise form of the manuscript's inverse majorant: only smoothness and invertibility at the point are assumed, and the constant is uniform in both the order and the exponential base.

theorem ringInverse_iteratedFDeriv_uniform_bound [CompleteSpace A]
    {D : ℝ} (hD : 1 ≤ D) :
    ∃ C : ℝ, Real.sqrt D ≤ C ∧ 2 * D ≤ C ∧
      ∀ (B : ℝ), 0 < B → ∀ (J : X → A) (x : X),
      (∀ m : ℕ, ContDiffAt ℝ m J x) → IsUnit (J x) →
      ‖Ring.inverse (J x)‖ ≤ Real.sqrt D →
      (∀ m, 0 < m → ‖iteratedFDeriv ℝ m J x‖ ≤
        factorialMajorant m * jetCoefficientScale B m) →
      ∀ m, ‖iteratedFDeriv ℝ m (fun y => Ring.inverse (J y)) x‖ ≤
        C * factorialMajorant m * jetCoefficientScale B m := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale

theorem OAI.RegularPointCoordinates.norm_iteratedFDerivWithin_inverseTranspose line 372

Source documentation

Taking the transpose preserves every iterated derivative norm.

theorem norm_iteratedFDerivWithin_inverseTranspose
    (J : X → E →L[ℝ] E) {s : Set X} {x : X}
    (hs : UniqueDiffOn ℝ s) (hx : x ∈ s) (m : ℕ) :
    ‖iteratedFDerivWithin ℝ m (fun y => operatorInverseTranspose (J y)) s x‖ =
      ‖iteratedFDerivWithin ℝ m (fun y => Ring.inverse (J y)) s x‖ := by
…

Mentions: OAI.RegularPointCoordinates.operatorInverseTranspose

theorem OAI.RegularPointCoordinates.norm_iteratedFDeriv_inverseTranspose line 380

theorem OAI.RegularPointCoordinates.inverseTranspose_iteratedFDerivWithin_uniform_bound line 389

Source documentation

The all-order inverse-transpose estimate uses the same constant and the same exponential base as the inverse estimate.

theorem inverseTranspose_iteratedFDerivWithin_uniform_bound
    {D : ℝ} (hD : 1 ≤ D) :
    ∃ C : ℝ, Real.sqrt D ≤ C ∧ 2 * D ≤ C ∧
      ∀ (B : ℝ), 0 < B → ∀ (J : X → E →L[ℝ] E) (s : Set X) (x : X),
      (∀ m : ℕ, ContDiffOn ℝ m J s) → (∀ y ∈ s, IsUnit (J y)) →
      UniqueDiffOn ℝ s → x ∈ s → ‖Ring.inverse (J x)‖ ≤ Real.sqrt D →
      (∀ m, 0 < m → ‖iteratedFDerivWithin ℝ m J s x‖ ≤
        factorialMajorant m * jetCoefficientScale B m) →
      ∀ m, ‖iteratedFDerivWithin ℝ m (fun y => operatorInverseTranspose (J y)) s x‖ ≤
        C * factorialMajorant m * jetCoefficientScale B m := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale, OAI.RegularPointCoordinates.operatorInverseTranspose

theorem OAI.RegularPointCoordinates.inverseTranspose_iteratedFDeriv_uniform_bound line 408

Source documentation

Pointwise inverse-transpose majorant, with the same constant as the inverse and no loss of exponential base.

theorem inverseTranspose_iteratedFDeriv_uniform_bound
    {D : ℝ} (hD : 1 ≤ D) :
    ∃ C : ℝ, Real.sqrt D ≤ C ∧ 2 * D ≤ C ∧
      ∀ (B : ℝ), 0 < B → ∀ (J : X → E →L[ℝ] E) (x : X),
      (∀ m : ℕ, ContDiffAt ℝ m J x) → IsUnit (J x) →
      ‖Ring.inverse (J x)‖ ≤ Real.sqrt D →
      (∀ m, 0 < m → ‖iteratedFDeriv ℝ m J x‖ ≤
        factorialMajorant m * jetCoefficientScale B m) →
      ∀ m, ‖iteratedFDeriv ℝ m (fun y => operatorInverseTranspose (J y)) x‖ ≤
        C * factorialMajorant m * jetCoefficientScale B m := by
…

Mentions: OAI.RegularPointCoordinates.factorialMajorant, OAI.RegularPointCoordinates.jetCoefficientScale, OAI.RegularPointCoordinates.operatorInverseTranspose