Ported for Lean Pool: imports relocated and code adapted to Lean/Mathlib v4.34.0.

Core Aleksandrov Jet Infrastructure (JetsAndFTC)

Part of the core Aleksandrov jet infrastructure development. Split from Core.lean; see the umbrella module docstring.

def ViscositySolns.StrictLocalMax {n : ℕ} (f : Point n → ℝ) (x0 : Point n) : Prop

A strict local maximum point.

In quantified mathematical form, StrictLocalMax f x0 means that there is a neighborhood U of x0 such that, for every x ∈ U, if x ≠ x0, then f x < f x0.

Equations

• ViscositySolns.StrictLocalMax f x0 = ∃ U ∈ nhds x0, ∀ x ∈ U, x ≠ x0 → f x < f x0

def ViscositySolns.linearPerturbation {n : ℕ} (f : Point n → ℝ) (p : Point n) : Point n → ℝ

The function obtained by adding the linear term p · x.

Equations

• ViscositySolns.linearPerturbation f p x = f x + p ⬝ᵥ x

theorem ViscositySolns.hasFDerivAt_linearPerturbation {n : ℕ} {f : Point n → ℝ} {x p q : Point n} (hf : HasFDerivAt f (gradientLinearMap p) x) : HasFDerivAt (linearPerturbation f q) (gradientLinearMap (p + q)) x

The derivative of a linear perturbation.

In quantified mathematical form, if f is differentiable at x with gradient p, then the function y ↦ f y + q · y is differentiable at x with gradient p + q.

noncomputable def ViscositySolns.gradientLinearMapCLM {n : ℕ} : Point n →L[ℝ] Point n →L[ℝ] ℝ

The coordinate-gradient-to-Fréchet-derivative map as a continuous linear map.

This is the inverse direction to linearMapGradientCLM: it sends a coordinate vector p to the continuous linear functional v ↦ p · v.

Equations

• ViscositySolns.gradientLinearMapCLM = ∑ i : Fin n, (ContinuousLinearMap.smulRightL ℝ (ViscositySolns.Point n) ℝ) (ContinuousLinearMap.proj i) ∘SL ContinuousLinearMap.proj i

@[simp]

theorem ViscositySolns.gradientLinearMapCLM_apply {n : ℕ} (p : Point n) : gradientLinearMapCLM p = gradientLinearMap p

theorem ViscositySolns.gradient_add_eq_zero_of_isLocalMax_linearPerturbation_hasFDerivAt {n : ℕ} {f : Point n → ℝ} {x p q : Point n} (hmax : IsLocalMax (linearPerturbation f q) x) (hf : HasFDerivAt f (gradientLinearMap p) x) : p + q = 0

At a local maximum point of a differentiable linear perturbation, the gradient of the original function is the negative perturbing vector.

In quantified mathematical form, if x is a local maximum of y ↦ f y + q · y, and f is differentiable at x with gradient p, then p + q = 0.

def ViscositySolns.HasSecondOrderJet {n : ℕ} (f : Point n → ℝ) (x p : Point n) (X : Hessian n) : Prop

Second-order differentiability expressed through ordinary superjets and subjets.

In quantified mathematical form, HasSecondOrderJet f x p X means that (p, X) belongs both to the superjet and to the subjet of f at x, relative to all of R^n.

Equations

• ViscositySolns.HasSecondOrderJet f x p X = ({ gradient := p, hessian := X } ∈ ViscositySolns.Superjet Set.univ f x ∧ { gradient := p, hessian := X } ∈ ViscositySolns.Subjet Set.univ f x)

theorem ViscositySolns.HasSecondOrderExpansionWithin.hasSecondOrderJet {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (h : HasSecondOrderExpansionWithin Set.univ f x { gradient := p, hessian := X }) : HasSecondOrderJet f x p X

A second-order expansion gives the corresponding ordinary two-sided jet.

This is the bridge from the classical Taylor-expansion conclusion of Aleksandrov's theorem to the jet language used by the maximum-principle formalization.

theorem ViscositySolns.HasSecondOrderExpansionWithin.hasSecondOrderJet_of_mem_nhds {n : ℕ} {C : Set (Point n)} {f : Point n → ℝ} {x : Point n} {J : Jet n} (hC : C ∈ nhds x) (h : HasSecondOrderExpansionWithin C f x J) : HasSecondOrderJet f x J.gradient J.hessian

A second-order expansion on a set which is a neighborhood of the base point gives the corresponding ordinary two-sided jet.

def ViscositySolns.HasSomeSecondOrderJet {n : ℕ} (f : Point n → ℝ) (x : Point n) : Prop

The set of points where a function has some second-order jet.

In quantified mathematical form, HasSomeSecondOrderJet f x means that there exist p : R^n and a Hermitian matrix X such that (p, X) belongs both to the ordinary superjet and to the ordinary subjet of f at x.

Equations

• ViscositySolns.HasSomeSecondOrderJet f x = ∃ (p : ViscositySolns.Point n) (X : ViscositySolns.Hessian n), Matrix.IsHermitian X ∧ ViscositySolns.HasSecondOrderJet f x p X

theorem ViscositySolns.HasSecondOrderJet.congr_of_eventuallyEq {n : ℕ} {f g : Point n → ℝ} {x p : Point n} {X : Hessian n} (hfg : f =ᶠ[nhds x] g) (h : HasSecondOrderJet f x p X) : HasSecondOrderJet g x p X

Ordinary two-sided jets depend only on the germ of the function at the base point.

theorem ViscositySolns.HasSomeSecondOrderJet.congr_of_eventuallyEq {n : ℕ} {f g : Point n → ℝ} {x : Point n} (hfg : f =ᶠ[nhds x] g) (h : HasSomeSecondOrderJet f x) : HasSomeSecondOrderJet g x

Existence of an ordinary two-sided jet depends only on the germ of the function at the base point.

theorem ViscositySolns.bilinearMapHessian_isHermitian_of_isSymmetricBilinear {n : ℕ} {D2 : Point n →L[ℝ] Point n →L[ℝ] ℝ} (hD2sym : IsSymmetricBilinear D2) : Matrix.IsHermitian (bilinearMapHessian D2)

A symmetric continuous bilinear map has a Hermitian coordinate Hessian.

theorem ViscositySolns.HasSecondOrderExpansionWithin.hasSomeSecondOrderJet {n : ℕ} {f : Point n → ℝ} {x p : Point n} {X : Hessian n} (h : HasSecondOrderExpansionWithin Set.univ f x { gradient := p, hessian := X }) (hHerm : Matrix.IsHermitian X) : HasSomeSecondOrderJet f x

A second-order expansion with Hermitian Hessian gives existence of some ordinary two-sided jet.

theorem ViscositySolns.HasSecondOrderExpansionWithin.hasSomeSecondOrderJet_of_isSymmetricBilinear {n : ℕ} {f : Point n → ℝ} {x : Point n} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} (h : HasSecondOrderExpansionWithin Set.univ f x (Jet.ofDerivatives Dφ D2φ)) (hD2sym : IsSymmetricBilinear D2φ) : HasSomeSecondOrderJet f x

A second-order expansion whose Fréchet second derivative is symmetric gives an ordinary two-sided jet.

theorem ViscositySolns.HasSecondOrderExpansionWithin.hasSomeSecondOrderJet_of_isSymmetricBilinear_of_mem_nhds {n : ℕ} {C : Set (Point n)} {f : Point n → ℝ} {x : Point n} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} (hC : C ∈ nhds x) (h : HasSecondOrderExpansionWithin C f x (Jet.ofDerivatives Dφ D2φ)) (hD2sym : IsSymmetricBilinear D2φ) : HasSomeSecondOrderJet f x

A second-order expansion on a neighborhood set whose Fréchet second derivative is symmetric gives an ordinary two-sided jet.

theorem ViscositySolns.HasSomeSecondOrderJet.of_frechetLittleO {n : ℕ} {f : Point n → ℝ} {x : Point n} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} (hD2sym : IsSymmetricBilinear D2φ) (hTaylor : (fun (z : Point n) => f z - frechetSecondOrderModel x (f x) Dφ D2φ z) =o[nhds x] fun (z : Point n) => ‖z - x‖ ^ 2) : HasSomeSecondOrderJet f x

A Fréchet second-order little-oh remainder gives an ordinary two-sided jet.

This is the final target shape for the source proof's a.e. line-integration argument: once the Taylor remainder is known to be o(‖z - x‖²), the jet conclusion follows without requiring differentiability on a whole neighborhood.

theorem ViscositySolns.intervalIntegral_integral_sub_linear_isLittleO_of_tendsto_ae_nhds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E} (hfm : StronglyMeasurableAtFilter f (nhds 0) MeasureTheory.volume) (hf : Filter.Tendsto f (nhds 0 ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : (fun (t : ℝ) => (∫ (s : ℝ) in 0..t, f s) - t • c) =o[nhds 0] fun (t : ℝ) => t

One-dimensional FTC estimate used in the source proof's final Taylor step.

If a derivative-error field has an a.e. limit c at the base point, then its interval integral from 0 to t has first-order expansion with slope c.

theorem ViscositySolns.intervalIntegral_integral_isLittleO_of_tendsto_ae_zero_nhds {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} (hfm : StronglyMeasurableAtFilter f (nhds 0) MeasureTheory.volume) (hf : Filter.Tendsto f (nhds 0 ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds 0)) : (fun (t : ℝ) => ∫ (s : ℝ) in 0..t, f s) =o[nhds 0] fun (t : ℝ) => t

Zero-slope specialization of the a.e. FTC estimate.

theorem ViscositySolns.AbsolutelyContinuousOnInterval.integral_eq_sub_of_ae_hasDerivAt {F g : ℝ → ℝ} {a b : ℝ} (hF : AbsolutelyContinuousOnInterval F a b) (hg : ∀ᵐ (x : ℝ), x ∈ Set.uIcc a b → HasDerivAt F (g x) x) : ∫ (x : ℝ) in a..b, g x = F b - F a

FTC for an absolutely continuous one-dimensional function when the derivative is supplied as an a.e. HasDerivAt field.

This is the source proof's line-restriction identity in a reusable form: absolute continuity identifies the increment with the integral of the a.e. derivative field.

theorem ViscositySolns.absolutelyContinuous_sub_linear_isLittleO_of_ae_hasDerivAt_tendsto_ae_nhds {F g : ℝ → ℝ} {c : ℝ} (hAC : ∀ᶠ (t : ℝ) in nhds 0, AbsolutelyContinuousOnInterval F 0 t) (hderiv : ∀ᵐ (s : ℝ), HasDerivAt F (g s) s) (hgm : StronglyMeasurableAtFilter g (nhds 0) MeasureTheory.volume) (hg : Filter.Tendsto g (nhds 0 ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c)) : (fun (t : ℝ) => F t - F 0 - t • c) =o[nhds 0] fun (t : ℝ) => t

First-order little-oh consequence of the source proof's a.e. line-integration step.

If a line restriction is absolutely continuous on all sufficiently small intervals from 0 to t, has a.e. derivative field g, and g has an a.e. limit c at 0, then the line restriction has first-order expansion with slope c.

theorem ViscositySolns.norm_le_norm_right_of_mem_uIoc_zero {s t : ℝ} (hs : s ∈ Set.uIoc 0 t) : ‖s‖ ≤ ‖t‖

Points in the unordered interval from 0 to t have norm at most ‖t‖.

This elementary estimate is the geometric input that turns a pointwise o(s) derivative-error bound into a uniform bound on small line segments.

theorem ViscositySolns.isLittleO_id_uniform_uIoc_bound_nhds {g : ℝ → ℝ} (hg : g =o[nhds 0] fun (s : ℝ) => s) (c : ℝ) : c > 0 → ∀ᶠ (t : ℝ) in nhds 0, ∀ s ∈ Set.uIoc 0 t, ‖g s‖ ≤ c * ‖t‖

Uniform small-segment form of a one-dimensional o(id) bound.

If g(s) = o(s) at 0, then for every c > 0 and all sufficiently small endpoints t, the bound ‖g s‖ ≤ c * ‖t‖ holds throughout the unordered interval Ι 0 t.

theorem ViscositySolns.absolutelyContinuous_sub_const_isLittleO_sq_of_ae_hasDerivAt_bound {F g : ℝ → ℝ} (hAC : ∀ᶠ (t : ℝ) in nhds 0, AbsolutelyContinuousOnInterval F 0 t) (hderiv : ∀ᵐ (s : ℝ), HasDerivAt F (g s) s) (hbound : ∀ c > 0, ∀ᶠ (t : ℝ) in nhds 0, ∀ s ∈ Set.uIoc 0 t, ‖g s‖ ≤ c * ‖t‖) : (fun (t : ℝ) => F t - F 0) =o[nhds 0] fun (t : ℝ) => t ^ 2

Quadratic little-oh consequence of the source proof's a.e. line-integration step.

If a line restriction is absolutely continuous on all sufficiently small intervals from 0 to t, has a.e. derivative field g, and the derivative error is uniformly bounded by c * ‖t‖ on the unordered interval from 0 to t for every small c, then the line increment is o(t²).

theorem ViscositySolns.absolutelyContinuous_sub_const_isLittleO_sq_of_ae_hasDerivAt_isLittleO {F g : ℝ → ℝ} (hAC : ∀ᶠ (t : ℝ) in nhds 0, AbsolutelyContinuousOnInterval F 0 t) (hderiv : ∀ᵐ (s : ℝ), HasDerivAt F (g s) s) (hg : g =o[nhds 0] fun (s : ℝ) => s) : (fun (t : ℝ) => F t - F 0) =o[nhds 0] fun (t : ℝ) => t ^ 2

Direct quadratic little-oh consequence of the a.e. FTC line-integration step.

If a line restriction is absolutely continuous on sufficiently small intervals, has a.e. derivative field g, and g(t) = o(t) at 0, then the line increment is o(t²).

theorem ViscositySolns.LipschitzOnWith.absolutelyContinuousOnInterval_comp_segment {n : ℕ} {F : Point n → ℝ} {x0 v : Point n} {K : NNReal} (hF : LipschitzOnWith K F Set.univ) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => F (x0 + t • v)) 0 1

A Lipschitz function restricted to an affine line segment is absolutely continuous.

This is the basic regularity input for the source proof's segment integration step: local Lipschitz control in the ambient coordinate space gives absolute continuity of one-dimensional restrictions.

theorem ViscositySolns.LipschitzOnWith.absolutelyContinuousOnInterval_comp_segment_of_subset {n : ℕ} {F : Point n → ℝ} {x0 v : Point n} {K : NNReal} {s : Set (Point n)} (hF : LipschitzOnWith K F s) (hseg : ∀ t ∈ Set.uIcc 0 1, x0 + t • v ∈ s) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => F (x0 + t • v)) 0 1

A local Lipschitz bound on a set containing the segment gives absolute continuity of the corresponding line restriction.

theorem ViscositySolns.LipschitzOnWith.absolutelyContinuousOnInterval_frechetResidual_comp_segment {n : ℕ} {F : Point n → ℝ} {x0 v : Point n} {K : NNReal} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} (hF : LipschitzOnWith K F Set.univ) : AbsolutelyContinuousOnInterval (fun (t : ℝ) => F (x0 + t • v) - frechetSecondOrderModel x0 (F x0) Dφ D2φ (x0 + t • v)) 0 1

The Taylor residual of a globally Lipschitz function is absolutely continuous on affine line segments.

The nonlinear part is supplied by the Lipschitz restriction lemma above; the quadratic Taylor model is C¹ after restricting to a line, hence absolutely continuous.

theorem ViscositySolns.LipschitzOnWith.eventually_absolutelyContinuousOnInterval_frechetResidual_segment {n : ℕ} {F : Point n → ℝ} {x0 : Point n} {K : NNReal} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} (hF : LipschitzOnWith K F Set.univ) : ∀ᶠ (z : Point n) in nhds x0, AbsolutelyContinuousOnInterval (fun (t : ℝ) => F (x0 + t • (z - x0)) - frechetSecondOrderModel x0 (F x0) Dφ D2φ (x0 + t • (z - x0))) 0 1

Eventually-nearby segment form of LipschitzOnWith.absolutelyContinuousOnInterval_frechetResidual_comp_segment.

theorem ViscositySolns.LipschitzOnWith.eventually_ac_frechetResidual_segment_of_mem_nhds {n : ℕ} {F : Point n → ℝ} {x0 : Point n} {K : NNReal} {s : Set (Point n)} {Dφ : Point n →L[ℝ] ℝ} {D2φ : Point n →L[ℝ] Point n →L[ℝ] ℝ} (hF : LipschitzOnWith K F s) (hs : s ∈ nhds x0) : ∀ᶠ (z : Point n) in nhds x0, AbsolutelyContinuousOnInterval (fun (t : ℝ) => F (x0 + t • (z - x0)) - frechetSecondOrderModel x0 (F x0) Dφ D2φ (x0 + t • (z - x0))) 0 1

Local Lipschitz control near the base point gives eventual absolute continuity of Taylor residuals on nearby segments.