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

Second-order jets of separated functions (CilBounds)

Part of the development recording the ordinary two-sided jet consequences of writing a function on R^n × R^n as a separated difference. Split from SeparatedJets.lean; see the umbrella module docstring.

theorem ViscositySolns.closedSemijets_and_cilBounds_original_of_regularizedDoubledConvolution_normalized {n : ℕ} (hJensen : JensenContactSetPositiveMeasureOnClosedBallTheorem (n + n)) (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {epsilon mu : ℝ} (hlambda_nonneg : 0 ≤ epsilon⁻¹ + mu) (hlambda_ne : epsilon⁻¹ + mu ≠ 0) {K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u ((fun (x : Point n) => x0 + x) '' K)) (hv : LowerSemicontinuousOn v ((fun (y : Point n) => y0 + y) '' L)) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := 0, hessian := X } ∈ ClosedSuperjet K (normalizedLeftOfBlockGradient u x0 P) 0 ∧ { gradient := 0, hessian := Y } ∈ ClosedSubjet L (normalizedRightOfBlockGradient v y0 P) 0 ∧ -(epsilon⁻¹ + mu) • blockDiagonalIdentity n ≤ comparisonBlockDiagonal X Y ∧ comparisonBlockDiagonal X Y ≤ A + epsilon • (A * A)

Closed semijets for the translated affine-normalized functions with the CIL matrix bounds.

In quantified mathematical form, suppose that A is symmetric, ε > 0, A ≤ μ [I 0; 0 I], 0 ≤ ε⁻¹ + μ, and ε⁻¹ + μ ≠ 0. If (x0, y0) is a maximum point on the translated compact product of

u(x) - v(y) - doubledQuadraticExpansionAt(x0, y0, φ0, P, A)(x, y),

then there exist matrices X and Y such that

(0, X) ∈ \overline J^{2,+}_K u_norm(0),

(0, Y) ∈ \overline J^{2,-}_L v_norm(0),

and

-(ε⁻¹ + μ)[I 0; 0 I] ≤ [X 0; 0 -Y] ≤ A + εA².

theorem ViscositySolns.closedSemijets_and_cilBounds_original_of_selectedTwoSidedJets_normalized {n : ℕ} (hselected : SelectedTwoSidedJetsForRegularizedDoubledConvolutionTheorem n) {epsilon mu : ℝ} (hlambda_nonneg : 0 ≤ epsilon⁻¹ + mu) (hlambda_ne : epsilon⁻¹ + mu ≠ 0) {K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u ((fun (x : Point n) => x0 + x) '' K)) (hv : LowerSemicontinuousOn v ((fun (y : Point n) => y0 + y) '' L)) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := 0, hessian := X } ∈ ClosedSuperjet K (normalizedLeftOfBlockGradient u x0 P) 0 ∧ { gradient := 0, hessian := Y } ∈ ClosedSubjet L (normalizedRightOfBlockGradient v y0 P) 0 ∧ -(epsilon⁻¹ + mu) • blockDiagonalIdentity n ≤ comparisonBlockDiagonal X Y ∧ comparisonBlockDiagonal X Y ≤ A + epsilon • (A * A)

Closed semijets for the translated affine-normalized functions with the CIL matrix bounds, from the selected two-sided-jet theorem.

theorem ViscositySolns.closedSemijets_and_cilBounds_translated_of_regularizedDoubledConvolution {n : ℕ} (hJensen : JensenContactSetPositiveMeasureOnClosedBallTheorem (n + n)) (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {epsilon mu : ℝ} (hlambda_nonneg : 0 ≤ epsilon⁻¹ + mu) (hlambda_ne : epsilon⁻¹ + mu ≠ 0) {K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u ((fun (x : Point n) => x0 + x) '' K)) (hv : LowerSemicontinuousOn v ((fun (y : Point n) => y0 + y) '' L)) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := blockPointLeft P, hessian := X } ∈ ClosedSuperjet ((fun (x : Point n) => x0 + x) '' K) u x0 ∧ { gradient := -blockPointRight P, hessian := Y } ∈ ClosedSubjet ((fun (y : Point n) => y0 + y) '' L) v y0 ∧ -(epsilon⁻¹ + mu) • blockDiagonalIdentity n ≤ comparisonBlockDiagonal X Y ∧ comparisonBlockDiagonal X Y ≤ A + epsilon • (A * A)

Closed semijets for the original functions on translated compact domains with the CIL matrix bounds.

In quantified mathematical form, under the hypotheses of closedSemijets_and_cilBounds_original_of_regularizedDoubledConvolution_normalized, there exist matrices X and Y such that

(P_x, X) ∈ \overline J^{2,+}_{x0+K} u(x0),

(-P_y, Y) ∈ \overline J^{2,-}_{y0+L} v(y0),

and

-(ε⁻¹ + μ)[I 0; 0 I] ≤ [X 0; 0 -Y] ≤ A + εA².

theorem ViscositySolns.closedSemijets_and_cilBounds_translated_of_selectedTwoSidedJets {n : ℕ} (hselected : SelectedTwoSidedJetsForRegularizedDoubledConvolutionTheorem n) {epsilon mu : ℝ} (hlambda_nonneg : 0 ≤ epsilon⁻¹ + mu) (hlambda_ne : epsilon⁻¹ + mu ≠ 0) {K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u ((fun (x : Point n) => x0 + x) '' K)) (hv : LowerSemicontinuousOn v ((fun (y : Point n) => y0 + y) '' L)) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := blockPointLeft P, hessian := X } ∈ ClosedSuperjet ((fun (x : Point n) => x0 + x) '' K) u x0 ∧ { gradient := -blockPointRight P, hessian := Y } ∈ ClosedSubjet ((fun (y : Point n) => y0 + y) '' L) v y0 ∧ -(epsilon⁻¹ + mu) • blockDiagonalIdentity n ≤ comparisonBlockDiagonal X Y ∧ comparisonBlockDiagonal X Y ≤ A + epsilon • (A * A)

Closed semijets for the original functions on translated compact domains with the CIL matrix bounds, from the selected two-sided-jet theorem.

theorem ViscositySolns.closedSemijets_and_cilBounds_ambient_of_regularizedDoubledConvolution {n : ℕ} (hJensen : JensenContactSetPositiveMeasureOnClosedBallTheorem (n + n)) (hAleksandrov : AleksandrovSecondDifferentiabilityByJetsOnClosedBallTheorem (n + n)) {epsilon mu : ℝ} (hlambda_nonneg : 0 ≤ epsilon⁻¹ + mu) (hlambda_ne : epsilon⁻¹ + mu ≠ 0) {C D K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u ((fun (x : Point n) => x0 + x) '' K)) (hv : LowerSemicontinuousOn v ((fun (y : Point n) => y0 + y) '' L)) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hKsubsetC : (fun (x : Point n) => x0 + x) '' K ⊆ C) (hLsubsetD : (fun (y : Point n) => y0 + y) '' L ⊆ D) (hKnhds : (fun (x : Point n) => x0 + x) '' K ∈ nhdsWithin x0 C) (hLnhds : (fun (y : Point n) => y0 + y) '' L ∈ nhdsWithin y0 D) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := blockPointLeft P, hessian := X } ∈ ClosedSuperjet C u x0 ∧ { gradient := -blockPointRight P, hessian := Y } ∈ ClosedSubjet D v y0 ∧ -(epsilon⁻¹ + mu) • blockDiagonalIdentity n ≤ comparisonBlockDiagonal X Y ∧ comparisonBlockDiagonal X Y ≤ A + epsilon • (A * A)

Closed semijets for the original functions on the ambient domains with the CIL matrix bounds.

In quantified mathematical form, assume the hypotheses of closedSemijets_and_cilBounds_translated_of_regularizedDoubledConvolution. Assume additionally that {x0 + x | x ∈ K} is a subset of C and is a relative neighborhood of x0 in C, and that {y0 + y | y ∈ L} is a subset of D and is a relative neighborhood of y0 in D. Then there exist matrices X and Y such that

(P_x, X) ∈ \overline J^{2,+}_C u(x0),

(-P_y, Y) ∈ \overline J^{2,-}_D v(y0),

and

-(ε⁻¹ + μ)[I 0; 0 I] ≤ [X 0; 0 -Y] ≤ A + εA².

theorem ViscositySolns.closedSemijets_and_cilBounds_ambient_of_selectedTwoSidedJets {n : ℕ} (hselected : SelectedTwoSidedJetsForRegularizedDoubledConvolutionTheorem n) {epsilon mu : ℝ} (hlambda_nonneg : 0 ≤ epsilon⁻¹ + mu) (hlambda_ne : epsilon⁻¹ + mu ≠ 0) {C D K L : Set (Point n)} {u v : Point n → ℝ} {x0 y0 : Point n} {φ0 : ℝ} {P : BlockPoint n} {A : BlockHessian n} (hHerm : Matrix.IsHermitian A) (hepsilon : 0 < epsilon) (hA : A ≤ mu • blockDiagonalIdentity n) (hKne : K.Nonempty) (hLne : L.Nonempty) (hKcompact : IsCompact K) (hLcompact : IsCompact L) (hu : UpperSemicontinuousOn u ((fun (x : Point n) => x0 + x) '' K)) (hv : LowerSemicontinuousOn v ((fun (y : Point n) => y0 + y) '' L)) (h0K : 0 ∈ K) (h0L : 0 ∈ L) (hKsubsetC : (fun (x : Point n) => x0 + x) '' K ⊆ C) (hLsubsetD : (fun (y : Point n) => y0 + y) '' L ⊆ D) (hKnhds : (fun (x : Point n) => x0 + x) '' K ∈ nhdsWithin x0 C) (hLnhds : (fun (y : Point n) => y0 + y) '' L ∈ nhdsWithin y0 D) (hmax : IsMaxOn (fun (q : DoubledPoint n) => u q.1 - v q.2 - doubledQuadraticExpansionAt x0 y0 φ0 P A q) {q : DoubledPoint n | q.1 - x0 ∈ K ∧ q.2 - y0 ∈ L} (x0, y0)) : ∃ (X : Hessian n) (Y : Hessian n), { gradient := blockPointLeft P, hessian := X } ∈ ClosedSuperjet C u x0 ∧ { gradient := -blockPointRight P, hessian := Y } ∈ ClosedSubjet D v y0 ∧ -(epsilon⁻¹ + mu) • blockDiagonalIdentity n ≤ comparisonBlockDiagonal X Y ∧ comparisonBlockDiagonal X Y ≤ A + epsilon • (A * A)

Closed semijets for the original functions on the ambient domains with the CIL matrix bounds, from the selected two-sided-jet theorem.

theorem ViscositySolns.HasSecondOrderJet.left_of_blockFunctionToPointFunction_sub {n : ℕ} {G H : Point n → ℝ} {p : Point (n + n)} {Z : Hessian (n + n)} (hJ : HasSecondOrderJet (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) 0 p Z) : HasSecondOrderJet G 0 (leftPointGradient p) (leftPointHessian Z)

The zero-base specialization of HasSecondOrderJet.left_of_blockFunctionToPointFunction_sub_at.

theorem ViscositySolns.HasSecondOrderJet.right_of_blockFunctionToPointFunction_sub {n : ℕ} {G H : Point n → ℝ} {p : Point (n + n)} {Z : Hessian (n + n)} (hJ : HasSecondOrderJet (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) 0 p Z) : HasSecondOrderJet H 0 (-rightPointGradient p) (-rightPointHessian Z)

The zero-base specialization of HasSecondOrderJet.right_of_blockFunctionToPointFunction_sub_at.

theorem ViscositySolns.hasSecondOrderJet_left_right_sequence_of_blockFunctionToPointFunction_sub {n : ℕ} {G H : Point n → ℝ} {zSeq : ℕ → Point (n + n)} {JSeq : ℕ → Jet (n + n)} (hJ : ∀ (k : ℕ), HasSecondOrderJet (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) (zSeq k) (JSeq k).gradient (JSeq k).hessian) : (∀ (k : ℕ), HasSecondOrderJet G (pointLeft (zSeq k)) (leftPointGradient (JSeq k).gradient) (leftPointHessian (JSeq k).hessian)) ∧ ∀ (k : ℕ), HasSecondOrderJet H (pointRight (zSeq k)) (-rightPointGradient (JSeq k).gradient) (-rightPointHessian (JSeq k).hessian)

Apply separated-function two-sided jet splitting to every term in a sequence.

In quantified mathematical form, let G, H : R^n -> R and let F(ξ, η) = G(ξ) - H(η). If for every natural number k, the pair ((J_k).gradient, (J_k).hessian) is an ordinary two-sided second-order jet of F at z_k, then for every natural number k the left component is an ordinary two-sided second-order jet of G at the left component of z_k, and the negative right component is an ordinary two-sided second-order jet of H at the right component of z_k.

theorem ViscositySolns.closedSemijets_of_tendsto_twoSidedJet_blockFunctionToPointFunction_sub {n : ℕ} {G H : Point n → ℝ} (hG : Continuous G) (hH : Continuous H) {zSeq : ℕ → Point (n + n)} {JSeq : ℕ → Jet (n + n)} {J : Jet (n + n)} (hz : Filter.Tendsto zSeq Filter.atTop (nhds 0)) (hJtendsto : Filter.Tendsto JSeq Filter.atTop (nhds J)) (hJ : ∀ (k : ℕ), HasSecondOrderJet (blockFunctionToPointFunction fun (q : BlockPoint n) => G (blockPointLeft q) - H (blockPointRight q)) (zSeq k) (JSeq k).gradient (JSeq k).hessian) : leftPointJet J ∈ ClosedSuperjet Set.univ G 0 ∧ (rightPointJet J).neg ∈ ClosedSubjet Set.univ H 0

A convergent sequence of two-sided jets of a separated difference gives closed semijets of the two component functions.

In quantified mathematical form, let G, H : R^n -> R, let F(ξ, η) = G(ξ) - H(η), and let z_k -> 0 in R^n × R^n. Suppose that J_k -> J, and suppose that for every natural number k, ((J_k).gradient, (J_k).hessian) is an ordinary two-sided second-order jet of F at z_k. If G and H are continuous, then the left component of J belongs to the closed superjet of G at 0, and the negative right component of J belongs to the closed subjet of H at 0.