Mathlib.Analysis
Analysis helpers staged for upstreaming: Bernoulli KL inequalities, functional-equation facts, scalar arithmetic, half-disc polar integration, and one-dimensional smooth descent bounds.
BernsteinSzegoTrig 13 core · 10 supporting · 4 submodules Trigonometric-polynomial infrastructure for Bernstein-Szegő comparisons: degree bounds, zero counting, cosine composition, and Szegő interpolation. AbsoluteValueMomentPriorDuality 19 core · 40 supporting · 4 submodules This umbrella module exports the intrinsic best uniform approximation error, the symmetric moment-matched probability-prior construction, its projection lemmas, and universal 1 / K rate bounds. ArgumentPrincipleCircle 7 core · 9 supporting · 3 submodules Complex-analysis infrastructure for the argument principle on positively oriented circles: multiplicity-weighted zero counts, logarithmic-derivative contour integrals, homotopy invariance, and Rouché comparison. CertifiedContourIntervalArithmetic 186 core · 144 supporting · 10 submodules Certified numerical-analysis infrastructure: exact rational intervals, effective certified-real refinement, transcendental enclosures, Lipschitz mesh quadrature, and measurable finite selection. Convex 1 core · 5 supporting · 1 submodule Convex-analysis helpers staged for upstreaming: reciprocal-product convexity and supporting inequalities for optimization arguments. EhlichZellerMesh 9 core · 14 supporting · 2 submodules Ehlich-Zeller mesh helpers: Chebyshev-Lobatto nodes, trigonometric transforms, mesh maxima, sup-norm transfer, and Bernstein/Szegő inequalities. FiniteDimL1LinfDuality 19 core · 26 supporting · 6 submodules Finite-dimensional l1-linfinity duality helpers: polynomial evaluation maps, moment systems, weak and strong duality, and Hahn-Banach setup. FinitePolynomialAlternationDuality 12 to review
43 core · 15 supporting · 27 submodules Compact-interval approximation theory for real polynomials: affine Markov derivative bounds, Chebyshev interpolation controls, and finite alternating moment-dual certificates for best uniform approximation. JacksonApproximation 2 to review
21 core · 40 supporting · 6 submodules Jackson approximation infrastructure: normalized fourth-power kernels, explicit moment bounds, even-trigonometric extraction, finite tensor convolution, four-dimensional coefficient envelopes, and affine rectangle transport. ParametricRationalIntegralAnalyticity 6 core · 9 supporting · 5 submodules This umbrella module exports the reusable finite-measure analyticity API for fixed-degree polynomial numerators divided by uniformly nonzero affine denominators, together with its scalar interval example. SymmetricTensorPencil 40 core · 27 supporting · 7 submodules Finite-dimensional symmetric-tensor-pencil recovery: contraction and conditioning bounds, generalized-eigenvalue perturbation, spectral matching, and a quantitative permutation-aligned local inverse. WeightedCircularTube 16 core · 21 supporting · 3 submodules Planar unit-circle tube infrastructure: radial power weights, uniform one-sided local mass bounds, finite positive annular normalizers, and reciprocal-scale separated nets.
TwoByTwoSpectralRoots 5 core · 12 supporting This module supplies explicit ordered roots, their spectral interpretation for symmetric matrices, and their local continuous differentiability away from a repeated root. ★ eigenvalue_eq_lambda₁_or_lambda₂
Ordered roots of a real two-by-two matrix
This module supplies explicit ordered roots, their spectral interpretation for symmetric matrices, and their local continuous differentiability away from a repeated root. The formulas are defined on all real two-by-two matrices, so the strict-gap region is open without choosing an eigenvector.
def rootDiscriminant reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-by-two matrix, the symmetric-matrix discriminant is the squared diagonal difference plus four times the squared upper off-diagonal entry. The lower off-diagonal entry is ignored, so this is the discriminant of the characteristic polynomial only for a symmetric matrix.
def lambda₁ reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-by-two matrix, its larger symmetric-formula root is half the trace plus half the nonnegative square root of the symmetric-matrix discriminant. For a symmetric matrix this is the larger eigenvalue; for a nonsymmetric matrix it need not be an eigenvalue.
Definition (Lean source)
def lambda₂ reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-by-two matrix, its smaller symmetric-formula root is half the trace minus half the nonnegative square root of the symmetric-matrix discriminant. For a symmetric matrix this is the smaller eigenvalue; for a nonsymmetric matrix it need not be an eigenvalue.
Definition (Lean source)
def strictGapSet reviewed
⚑ flagged
Causalean.Mathlib.Analysis
The strict-gap region consists of real two-by-two matrices whose lower quadratic-formula root is strictly below their upper root.
theorem eigenvalue_eq_lambda₁_or_lambda₂ reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real symmetric two-by-two matrix, a real number, a nonzero two-vector, and an eigenvector relation for that number, the number is one of the two explicit ordered roots.
Formal statement
Proof (Lean source)
theorem eigenvalue_eq_lambda₁_or_lambda₂ {G : Matrix (Fin 2) (Fin 2) ℝ}
(hG : G.IsHermitian) {μ : ℝ} {v : Fin 2 → ℝ} (hv : v ≠ 0)
(heig : G.mulVec v = μ • v) :
μ = lambda₁ G ∨ μ = lambda₂ G := by
have hsym : G 1 0 = G 0 1 := by
simpa using hG.apply 0 1
have h0 := congrFun heig 0
have h1 := congrFun heig 1
simp [mulVec] at h0 h1
rw [hsym] at h1
have hdet : (G 0 0 - μ) * (G 1 1 - μ) - G 0 1 * G 0 1 = 0 := by
by_cases hv0 : v 0 = 0
· have hv1 : v 1 ≠ 0 := by
intro hv1
apply hv
funext i
fin_cases i <;> assumption
rw [hv0] at h0 h1
simp only [mul_zero, zero_add] at h0 h1
apply (mul_eq_zero.mp ?_).resolve_right hv1
linear_combination (G 0 0 - μ) * h1 - G 0 1 * h0
· apply (mul_eq_zero.mp ?_).resolve_right hv0
linear_combination (G 1 1 - μ) * h0 - G 0 1 * h1
have hsum := lambda₁_add_lambda₂ G
have hprod := lambda₁_mul_lambda₂ hG
rw [Matrix.det_fin_two, hsym] at hprod
have hfactor : (μ - lambda₁ G) * (μ - lambda₂ G) = 0 := by
calc
_ = μ ^ 2 - μ * (lambda₁ G + lambda₂ G) + lambda₁ G * lambda₂ G := by
ring
_ = μ ^ 2 - μ * (G 0 0 + G 1 1) +
(G 0 0 * G 1 1 - G 0 1 * G 0 1) := by
rw [hsum, hprod]
_ = 0 := by
nlinarith [hdet]
rcases mul_eq_zero.mp hfactor with h | h
· left
linarith
· right
linarith
12 supporting declarations (lemmas, instances)
-
rootDiscriminant_nonnegtheorem — For a real two-by-two matrix, its explicit discriminant is nonnegative.Proof (Lean source)
theorem rootDiscriminant_nonneg (G : Matrix (Fin 2) (Fin 2) ℝ) : 0 ≤ rootDiscriminant G := by unfold rootDiscriminant positivity -
lambda₁_sub_lambda₂theorem — For a real two-by-two matrix, the difference between its upper and lower roots is the nonnegative square root of its discriminant.hypothesesconclusionProof (Lean source)
theorem lambda₁_sub_lambda₂ (G : Matrix (Fin 2) (Fin 2) ℝ) : lambda₁ G - lambda₂ G = sqrt (rootDiscriminant G) := by unfold lambda₁ lambda₂ ring -
lambda₂_le_lambda₁theorem — For a real two-by-two matrix, its lower explicit root does not exceed its upper explicit root.Proof (Lean source)
theorem lambda₂_le_lambda₁ (G : Matrix (Fin 2) (Fin 2) ℝ) : lambda₂ G ≤ lambda₁ G := by rw [← sub_nonneg, lambda₁_sub_lambda₂] exact Real.sqrt_nonneg _ -
mem_strictGapSet_iff_discriminant_postheorem — For a real two-by-two matrix, having distinct ordered roots is equivalent to strict positivity of its discriminant.Proof (Lean source)
theorem mem_strictGapSet_iff_discriminant_pos (G : Matrix (Fin 2) (Fin 2) ℝ) : G ∈ strictGapSet ↔ 0 < rootDiscriminant G := by change lambda₂ G < lambda₁ G ↔ 0 < rootDiscriminant G rw [← sub_pos, lambda₁_sub_lambda₂, Real.sqrt_pos] -
lambda₁_add_lambda₂theorem — For a real two-by-two matrix, the two explicit roots add to its trace. -
lambda₁_mul_lambda₂theorem — Given a real two-by-two matrix that is symmetric, the product of its two explicit roots equals its determinant.Proof (Lean source)
theorem lambda₁_mul_lambda₂ {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G.IsHermitian) : lambda₁ G * lambda₂ G = G.det := by have hsym : G 1 0 = G 0 1 := by simpa using hG.apply 0 1 have hsqrt : sqrt (rootDiscriminant G) ^ 2 = rootDiscriminant G := Real.sq_sqrt (rootDiscriminant_nonneg G) rw [Matrix.det_fin_two, hsym] unfold lambda₁ lambda₂ rootDiscriminant at * nlinarith -
det_sub_lambda_mul_one_eq_zerotheorem — Given a real symmetric two-by-two matrix and one of the two root labels, subtracting that labelled explicit root from the diagonal has zero determinant.hypothesesProof (Lean source)
theorem det_sub_lambda_mul_one_eq_zero {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G.IsHermitian) (i : Fin 2) : (G - (if i = 0 then lambda₁ G else lambda₂ G) • (1 : Matrix (Fin 2) (Fin 2) ℝ)).det = 0 := by have hsym : G 1 0 = G 0 1 := by simpa using hG.apply 0 1 have hsqrt : sqrt (rootDiscriminant G) ^ 2 = rootDiscriminant G := Real.sq_sqrt (rootDiscriminant_nonneg G) fin_cases i <;> rw [Matrix.det_fin_two] <;> simp [Matrix.sub_apply, Matrix.smul_apply, lambda₁, lambda₂] <;> rw [hsym] <;> unfold rootDiscriminant at * <;> nlinarith -
contDiffAt_lambda₁theorem — Given a real two-by-two matrix with a strict gap between its explicit roots, the upper root varies continuously differentiably near that matrix.Proof (Lean source)
theorem contDiffAt_lambda₁ {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G ∈ strictGapSet) : ContDiffAt ℝ 1 lambda₁ G := by have hdisc : ContDiffAt ℝ 1 rootDiscriminant G := by unfold rootDiscriminant fun_prop have hpos : 0 < rootDiscriminant G := (mem_strictGapSet_iff_discriminant_pos G).mp hG have hsqrt := hdisc.sqrt (ne_of_gt hpos) unfold lambda₁ exact (((contDiff_apply_apply ℝ ℝ (0 : Fin 2) (0 : Fin 2)).contDiffAt.add (contDiff_apply_apply ℝ ℝ (1 : Fin 2) (1 : Fin 2)).contDiffAt).add hsqrt).div_const 2 -
contDiffAt_lambda₂theorem — Given a real two-by-two matrix with a strict gap between its explicit roots, the lower root varies continuously differentiably near that matrix.Proof (Lean source)
theorem contDiffAt_lambda₂ {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G ∈ strictGapSet) : ContDiffAt ℝ 1 lambda₂ G := by have hdisc : ContDiffAt ℝ 1 rootDiscriminant G := by unfold rootDiscriminant fun_prop have hpos : 0 < rootDiscriminant G := (mem_strictGapSet_iff_discriminant_pos G).mp hG have hsqrt := hdisc.sqrt (ne_of_gt hpos) unfold lambda₂ exact (((contDiff_apply_apply ℝ ℝ (0 : Fin 2) (0 : Fin 2)).contDiffAt.add (contDiff_apply_apply ℝ ℝ (1 : Fin 2) (1 : Fin 2)).contDiffAt).sub hsqrt).div_const 2 -
isOpen_strictGapSettheorem — The region of real two-by-two matrices with distinct explicit roots is open.conclusionProof (Lean source)
theorem isOpen_strictGapSet : IsOpen strictGapSet := by have hdisc : Continuous rootDiscriminant := by unfold rootDiscriminant fun_prop rw [show strictGapSet = {G | 0 < rootDiscriminant G} by ext G exact mem_strictGapSet_iff_discriminant_pos G] exact isOpen_lt continuous_const hdisc -
contDiffOn_lambda₁theorem — The upper explicit root is continuously differentiable throughout the strict-gap region.conclusionProof (Lean source)
theorem contDiffOn_lambda₁ : ContDiffOn ℝ 1 lambda₁ strictGapSet := by intro G hG exact (contDiffAt_lambda₁ hG).contDiffWithinAt -
contDiffOn_lambda₂theorem — The lower explicit root is continuously differentiable throughout the strict-gap region.conclusionProof (Lean source)
theorem contDiffOn_lambda₂ : ContDiffOn ℝ 1 lambda₂ strictGapSet := by intro G hG exact (contDiffAt_lambda₂ hG).contDiffWithinAt
LocallyBoundedDerivative 2 core · 0 supporting This module packages the elementary finite-dimensional consequence that a continuously differentiable function has a bounded Fréchet derivative on some neighborhood of each point. ★ hasLocallyBoundedFDerivAt
Local boundedness of a continuously differentiable derivative
This module packages the elementary finite-dimensional consequence that a continuously differentiable function has a bounded Fréchet derivative on some neighborhood of each point. It is independent of the matrix-specific development.
def HasLocallyBoundedFDerivAt reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a function between real normed vector spaces and a point in its domain, the property of having a locally bounded Fréchet derivative means that one neighborhood of the point has a uniform nonnegative bound on derivative norms.
Definition (Lean source)
parameters
def
HasLocallyBoundedFDerivAt f x :
Prop
given by
∃ U ∈ 𝓝 x, ∃ C : ℝ,
0 ≤ C
clause 1
y ∈ U :
‖fderiv ℝ f y‖ ≤ C
theorem hasLocallyBoundedFDerivAt reviewed
⚑ flagged
Causalean.Mathlib.Analysis.ContDiffAt
Given a function between real normed vector spaces, a point in its domain, and continuous differentiability at that point, the function has a locally bounded Fréchet derivative there.
Formal statement
Proof (Lean source)
theorem ContDiffAt.hasLocallyBoundedFDerivAt {E F : Type*}
[NormedAddCommGroup E] [NormedSpace ℝ E]
[NormedAddCommGroup F] [NormedSpace ℝ F]
{f : E → F} {x : E} (hf : ContDiffAt ℝ 1 f x) :
HasLocallyBoundedFDerivAt f x := by
rcases contDiffAt_one_iff.mp hf with ⟨f', U, hU, hf'cont, hfderiv⟩
have hxU : x ∈ U := mem_of_mem_nhds hU
have hf'contAt : ContinuousAt f' x :=
(hf'cont x hxU).continuousAt hU
have hnorm : ContinuousAt (fun y => ‖f' y‖) x := hf'contAt.norm
have hbound : {y | ‖f' y‖ < ‖f' x‖ + 1} ∈ 𝓝 x :=
hnorm (Iio_mem_nhds (lt_add_one ‖f' x‖))
refine ⟨U ∩ {y | ‖f' y‖ < ‖f' x‖ + 1}, inter_mem hU hbound,
‖f' x‖ + 1, by positivity, ?_⟩
intro y hy
rw [(hfderiv y hy.1).fderiv]
exact le_of_lt hy.2
BernoulliKL 2 core · 2 supporting This file proves a scalar upper bound on the Kullback--Leibler divergence between two Bernoulli laws whose success probabilities both lie in the interval $[1/4,3/4]$. ★ bernoulli_kl_le_four_sq_sub_of_mem_quarter_band
Bernoulli KL Band Bound
This file proves a scalar upper bound on the Kullback--Leibler divergence between two Bernoulli laws whose success probabilities both lie in the interval . It supplies a Mathlib-adjacent analytic estimate used by finite-sample information arguments elsewhere in the library.
def bernD reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a real number, the negative Bernoulli entropy is .
theorem bernoulli_kl_le_four_sq_sub_of_mem_quarter_band reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For probabilities p and q both restricted to the band [1/4, 3/4], the Bernoulli Kullback–Leibler divergence p · log(p / q) + (1 - p) · log((1 - p) / (1 - q)) is bounded above by 4 · (p - q) ^ 2.
Formal statement
Proof (Lean source)
theorem bernoulli_kl_le_four_sq_sub_of_mem_quarter_band
{p q : ℝ} (hp_lo : (1 : ℝ) / 4 ≤ p) (hp_hi : p ≤ 3 / 4)
(hq_lo : (1 : ℝ) / 4 ≤ q) (hq_hi : q ≤ 3 / 4) :
p * log (p / q) + (1 - p) * log ((1 - p) / (1 - q))
≤ 4 * (p - q) ^ 2 := by
have hp0 : p ≠ 0 := by nlinarith
have hp1 : 1 - p ≠ 0 := by nlinarith
have hq0 : q ≠ 0 := by nlinarith
have hq1 : 1 - q ≠ 0 := by nlinarith
rw [bernoulliKL_eq_bregman hp0 hp1 hq0 hq1]
have hnonneg := bernH_nonneg_of_mem_quarter_band hp_lo hp_hi hq_lo hq_hi
unfold bernH at hnonneg
linarith
2 supporting declarations (lemmas, instances)
-
hasDerivAt_bernEntropylemma — Away from zero and one, the negative Bernoulli entropy has derivative equal to the log odds of its argument.hypothesesx :ℝhx0 :x ≠ 0hx1 :1 - x ≠ 0conclusionProof (Lean source)
lemma hasDerivAt_bernEntropy (x : ℝ) (hx0 : x ≠ 0) (hx1 : 1 - x ≠ 0) : HasDerivAt (fun t : ℝ => t * log t + (1 - t) * log (1 - t)) (log x - log (1 - x)) x := by have h1 : HasDerivAt (fun t : ℝ => t * log t) (log x + 1) x := Real.hasDerivAt_mul_log hx0 have hsub : HasDerivAt (fun t : ℝ => 1 - t) (0 - 1) x := (hasDerivAt_const x (1 : ℝ)).fun_sub (hasDerivAt_id' (x := x)) have h2log : HasDerivAt (fun t : ℝ => log (1 - t)) (-(1 - x)⁻¹) x := by have h : HasDerivAt (fun t : ℝ => log (1 - t)) ((1 - x)⁻¹ * (0 - 1)) x := (Real.hasDerivAt_log hx1).comp x hsub convert h using 1 ring have h2 : HasDerivAt (fun t : ℝ => (1 - t) * log (1 - t)) (-(log (1 - x)) - 1) x := by have h : HasDerivAt (fun t : ℝ => (1 - t) * log (1 - t)) _ x := hsub.fun_mul h2log convert h using 1 rw [mul_neg, mul_inv_cancel₀ hx1] ring have h : HasDerivAt (fun t : ℝ => t * log t + (1 - t) * log (1 - t)) _ x := h1.fun_add h2 convert h using 1 ring -
bernoulliKL_eq_bregmanlemma — Bernoulli Kullback–Leibler divergence equals the Bregman remainder of the negative entropy function at the second probability.hypothesesp q :ℝhp0 :p ≠ 0hp1 :1 - p ≠ 0hq0 :q ≠ 0hq1 :1 - q ≠ 0Proof (Lean source)
ClipInterval 3 core · 11 supporting Truncating (clipping, clamping, winsorising) a real number to a closed interval [a, b] is ubiquitous in estimation: propensity scores are clipped away from 0 and 1, outcomes and privatised statistics are clipped to a sym ★ abs_clipIcc_sub_le★ clipIcc_sub_sq_le
Clipping a real number into a closed interval
Truncating (clipping, clamping, winsorising) a real number to a closed interval [a, b] is
ubiquitous in estimation: propensity scores are clipped away from 0 and 1, outcomes and
privatised statistics are clipped to a symmetric band [-B, B], and so on. Every such argument
needs the same four facts — the clipped value lies in the interval, values already inside are
untouched, the map is 1-Lipschitz, and clipping never increases the distance (nor the squared
distance) to any target that is itself inside the interval.
Mathlib proves the contraction property, but only for the subtype-valued projection
Set.projIcc : ℝ → Set.Icc a b, which is awkward to use when the surrounding development works
with plain reals. This file provides the real-valued companion clipIcc a b x = max a (min b x)
(definitionally the underlying value of Set.projIcc) together with the facts above, so that a
symmetric band [-B, B], an asymmetric propensity band [q, 1 - q], and either the max-outside
or the min-outside spelling are all instances of one API.
def clipIcc reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For two real endpoints and a real input, the clipped value is the larger of the first endpoint and the smaller of the second endpoint and the input. When the first endpoint does not exceed the second, it is the input pushed into their closed interval.
lemma abs_clipIcc_sub_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Clipping toward an in-interval target does not increase distance. If a real number lies in the closed interval from a to b, then for any real x, clipping x into that interval moves it no farther from the target than x itself was.
Formal statement
Proof (Lean source)
lemma abs_clipIcc_sub_le (ht : t ∈ Icc a b) (x : ℝ) :
|clipIcc a b x - t| ≤ |x - t| := by
simpa [clipIcc_eq_self ht] using abs_clipIcc_sub_clipIcc_le a b x t
lemma clipIcc_sub_sq_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Squared version: clipping toward an in-interval target does not increase squared distance. If a real number lies in the closed interval from a to b, then for any real x, the squared distance from the clipped value of x to the target is at most the squared distance from x itself to the target.
Formal statement
Proof (Lean source)
lemma clipIcc_sub_sq_le (ht : t ∈ Icc a b) (x : ℝ) :
(clipIcc a b x - t) ^ 2 ≤ (x - t) ^ 2 := by
have h := abs_clipIcc_sub_le ht x
calc (clipIcc a b x - t) ^ 2 = |clipIcc a b x - t| ^ 2 := (sq_abs _).symm
_ ≤ |x - t| ^ 2 := by gcongr
_ = (x - t) ^ 2 := sq_abs _
11 supporting declarations (lemmas, instances)
-
coe_projIcc_eq_clipIcclemma — Clipping into an interval is exactly Mathlib's projection onto that interval, read as a plain real number instead of as an element of the interval. This is the bridge that makes every fact about the projection available to a development that never leaves the reals.hypothesesa :sharedℝb :sharedℝhab :a ≤ bx :ℝconclusion(Set.projIcc a b hab x : ℝ) = clipIcc a b xProof (Lean source)
lemma coe_projIcc_eq_clipIcc (hab : a ≤ b) (x : ℝ) : (Set.projIcc a b hab x : ℝ) = clipIcc a b x := rfl -
clipIcc_mem_Icclemma — A clipped value always lies in the interval it was clipped to (provided the interval is nonempty, i.e. its left endpoint does not exceed its right endpoint).Proof (Lean source)
-
clipIcc_eq_selflemma — Clipping leaves untouched any number that already lies inside the interval.Proof (Lean source)
lemma clipIcc_eq_self (hx : x ∈ Icc a b) : clipIcc a b x = x := by rw [clipIcc, min_eq_right hx.2, max_eq_right hx.1] -
clipIcc_eq_min_maxlemma — Clipping from below first and then from above gives the same answer as clipping from above first and then from below. This reconciles the two spellings of the same operation that occur in practice, max a (min b x) and min b (max a x).Proof (Lean source)
lemma clipIcc_eq_min_max (hab : a ≤ b) (x : ℝ) : clipIcc a b x = min b (max a x) := by rw [clipIcc, max_min_distrib_left, max_eq_right hab] -
lipschitzWith_clipIcclemma — Clipping is a contraction: two numbers are never pushed further apart by being clipped to a common interval.Proof (Lean source)
lemma lipschitzWith_clipIcc (a b : ℝ) : LipschitzWith 1 (clipIcc a b) := (LipschitzWith.id.const_min b).const_max a -
abs_clipIcc_sub_clipIcc_lelemma — Clipping two numbers to the same interval never increases the distance between them.Proof (Lean source)
lemma abs_clipIcc_sub_clipIcc_le (a b x y : ℝ) : |clipIcc a b x - clipIcc a b y| ≤ |x - y| := by simpa [Real.dist_eq] using (lipschitzWith_clipIcc a b).dist_le_mul x y -
abs_min_max_sub_min_max_lelemma — Capping from above and then flooring from below is a contraction as well: two numbers put through that order of operations are never pushed further apart. Unlike clipIcc_eq_min_max, this needs no assumption on the two thresholds, which is what makes it usable for a propensity band [q, 1 - q] whose definition carries no q ≤ 1/2 hypothesis.Proof (Lean source)
lemma abs_min_max_sub_min_max_le (a b x y : ℝ) : |min b (max a x) - min b (max a y)| ≤ |x - y| := by have h : LipschitzWith 1 (fun z : ℝ => min b (max a z)) := (LipschitzWith.id.const_max a).const_min b simpa [Real.dist_eq] using h.dist_le_mul x y -
continuous_clipIcclemma — Clipping to a fixed interval is a continuous operation.Proof (Lean source)
@[fun_prop] lemma continuous_clipIcc (a b : ℝ) : Continuous (clipIcc a b) := continuous_const.max (continuous_const.min continuous_id) -
measurable_clipIcclemma — Clipping to a fixed interval is measurable, so clipping a random variable again yields a random variable.Proof (Lean source)
@[fun_prop] lemma measurable_clipIcc (a b : ℝ) : Measurable (clipIcc a b) := (continuous_clipIcc a b).measurable -
abs_clipIcc_neg_lelemma — Clipping to a symmetric band around zero produces a value whose magnitude is at most the half-width of the band.Proof (Lean source)
lemma abs_clipIcc_neg_le (hB : 0 ≤ B) (x : ℝ) : |clipIcc (-B) B x| ≤ B := abs_le.mpr (clipIcc_mem_Icc (by linarith) x) -
clipIcc_neg_eq_selflemma — Clipping to a symmetric band around zero leaves untouched any number whose magnitude is already within the half-width of the band.Proof (Lean source)
lemma clipIcc_neg_eq_self (hx : |x| ≤ B) : clipIcc (-B) B x = x := clipIcc_eq_self (Set.mem_Icc.mpr (abs_le.mp hx))
ConvexProjection 7 core · 24 supporting This module provides metric projection onto a nonempty closed convex subset of a real Hilbert space, together with its variational, contraction, continuity, and measurability properties. ★ loewnerProj_frobDist_le
Projection onto closed convex sets
This module provides metric projection onto a nonempty closed convex subset of a real Hilbert space, together with its variational, contraction, continuity, and measurability properties. It also specializes the construction to a Loewner interval of real matrices, using Frobenius distance, and supplies the associated matrix inequalities.
def convexProj reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a real Hilbert space and a target subset that is nonempty, closed, and convex, the metric projection assigns each point its nearest point in that target subset.
def loewnerSet reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a square matrix dimension and two real endpoints, the Loewner interval is the set of real square matrices for which (1) the matrix minus the lower endpoint times the identity is positive semidefinite, and (2) the upper endpoint times the identity minus the matrix is positive semidefinite.
def frobDist reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a square matrix dimension and two real square matrices, the Frobenius distance is the square root of the sum of squared entrywise differences between the two matrices.
def mtx reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a square matrix dimension, the matrix vectorization linear equivalence identifies real square matrices of that dimension with Euclidean vectors indexed by ordered pairs of row and column coordinates.
def mtxHomeo reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a square matrix dimension, the matrix vectorization homeomorphism identifies real square matrices of that dimension, with their usual topology, with Euclidean vectors indexed by ordered pairs of row and column coordinates.
def loewnerProj reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a square matrix dimension and two real endpoints, the Loewner projection maps each real square matrix to its nearest point, in Frobenius distance, in the corresponding Loewner interval when the endpoints are ordered; when they are reversed, it is the identity map.
theorem loewnerProj_frobDist_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Loewner projection is a nonexpansive (nearest-point) map. For ordered interval endpoints c ≤ C, if a target matrix already lies in the Loewner interval [cI, CI], then projecting an arbitrary matrix onto that interval, in Frobenius geometry, does not increase its Frobenius distance to the in-interval target matrix.
Formal statement
Proof (Lean source)
theorem loewnerProj_frobDist_le (hcC : c ≤ C)
(G S : Matrix (Fin p) (Fin p) ℝ) (hS : S ∈ loewnerSet p c C) :
frobDist (loewnerProj p c C G) S ≤ frobDist G S := by
rw [frobDist_eq_norm, frobDist_eq_norm, loewnerProj, dif_pos hcC, loewnerProjAux]
simp only [LinearEquiv.apply_symm_apply]
exact convexProj_le_of_mem (mtx p '' loewnerSet p c C)
((loewnerSet_nonempty p c C hcC).image (mtx p))
(mtx_image_isClosed p c C)
((loewnerSet_convex p c C).linear_image (mtx p).toLinearMap) (mtx p G) (mtx p S) ⟨S, hS, rfl⟩
24 supporting declarations (lemmas, instances)
-
convexProj_speclemma — A point's metric projection onto a nonempty closed convex set belongs to that set and attains the smallest possible distance from the point among all points in the set.hypothesesconclusionconclusion 1convexProj K hne hc hconv x ∈ Kconclusion 2‖x - convexProj K hne hc hconv x‖ = ⨅ y : K, ‖x - y‖Proof (Lean source)
lemma convexProj_spec (K : Set E) (hne : K.Nonempty) (hc : IsClosed K) (hconv : Convex ℝ K) (x : E) : convexProj K hne hc hconv x ∈ K ∧ ‖x - convexProj K hne hc hconv x‖ = ⨅ y : K, ‖x - y‖ := Classical.choose_spec (exists_norm_eq_iInf_of_complete_convex hne hc.isComplete hconv x) -
convexProj_memtheorem — The metric projection of every point belongs to its nonempty closed convex target set.hypothesesconclusionconvexProj K hne hc hconv x ∈ KProof (Lean source)
theorem convexProj_mem (K : Set E) (hne : K.Nonempty) (hc : IsClosed K) (hconv : Convex ℝ K) (x : E) : convexProj K hne hc hconv x ∈ K := (convexProj_spec K hne hc hconv x).1 -
convexProj_variationaltheorem — The residual from a point to its metric projection has nonpositive inner product with every feasible direction based at the projection.hypothesesE :sharedType u_1K :Set Ehne :K.Nonemptyhc :IsClosed Khconv :Convex ℝ Kx :Ey :Ehy :y ∈ Kconclusion⟪x - convexProj K hne hc hconv x, y - convexProj K hne hc hconv x⟫_ℝ ≤ 0Proof (Lean source)
theorem convexProj_variational (K : Set E) (hne : K.Nonempty) (hc : IsClosed K) (hconv : Convex ℝ K) (x : E) (y : E) (hy : y ∈ K) : ⟪x - convexProj K hne hc hconv x, y - convexProj K hne hc hconv x⟫_ℝ ≤ 0 := by exact (norm_eq_iInf_iff_real_inner_le_zero hconv (convexProj_mem K hne hc hconv x)).1 (convexProj_spec K hne hc hconv x).2 y hy -
convexProj_le_of_memtheorem — Projecting a point onto a nonempty closed convex set cannot increase its distance from any point already in that set.hypothesesE :sharedType u_1K :Set Ehne :K.Nonemptyhc :IsClosed Khconv :Convex ℝ Kx y :Ehy :y ∈ Kconclusion‖convexProj K hne hc hconv x - y‖ ≤ ‖x - y‖Proof (Lean source)
theorem convexProj_le_of_mem (K : Set E) (hne : K.Nonempty) (hc : IsClosed K) (hconv : Convex ℝ K) (x y : E) (hy : y ∈ K) : ‖convexProj K hne hc hconv x - y‖ ≤ ‖x - y‖ := by let p := convexProj K hne hc hconv x have hv := convexProj_variational K hne hc hconv x y hy have hi : 0 ≤ ⟪x - p, p - y⟫_ℝ := by rw [show p - y = -(y - p) by abel, inner_neg_right] simpa [p] using neg_nonneg.mpr hv rw [← sq_le_sq₀ (norm_nonneg _) (norm_nonneg _)] rw [show x - y = (x - p) + (p - y) by abel, norm_add_sq_real] nlinarith [sq_nonneg ‖x - p‖] -
convexProj_eq_selftheorem — Every point in a nonempty closed convex target set is unchanged by metric projection onto that set.hypothesesconclusionconvexProj K hne hc hconv x = xProof (Lean source)
theorem convexProj_eq_self (K : Set E) (hne : K.Nonempty) (hc : IsClosed K) (hconv : Convex ℝ K) (x : E) (hx : x ∈ K) : convexProj K hne hc hconv x = x := by have h := convexProj_le_of_mem K hne hc hconv x x hx have : ‖convexProj K hne hc hconv x - x‖ = 0 := le_antisymm (by simpa using h) (norm_nonneg _) exact sub_eq_zero.mp (norm_eq_zero.mp this) -
convexProj_lipschitztheorem — Metric projection onto a nonempty closed convex set is nonexpansive: projected distances never exceed the original distances.hypothesesconclusionLipschitzWith 1 (convexProj K hne hc hconv)Proof (Lean source)
theorem convexProj_lipschitz (K : Set E) (hne : K.Nonempty) (hc : IsClosed K) (hconv : Convex ℝ K) : LipschitzWith 1 (convexProj K hne hc hconv) := by apply LipschitzWith.of_dist_le_mul intro x y let px := convexProj K hne hc hconv x let py := convexProj K hne hc hconv y have hx := convexProj_variational K hne hc hconv x py (convexProj_mem K hne hc hconv y) have hy := convexProj_variational K hne hc hconv y px (convexProj_mem K hne hc hconv x) have hi : ⟪px - py, px - py⟫_ℝ ≤ ⟪x - y, px - py⟫_ℝ := by simp only [inner_sub_left, inner_sub_right, real_inner_comm] at hx hy ⊢ nlinarith have hs : ‖px - py‖ ^ 2 ≤ ‖x - y‖ * ‖px - py‖ := by rw [← real_inner_self_eq_norm_sq] exact hi.trans (real_inner_le_norm _ _) have hn : ‖px - py‖ ≤ ‖x - y‖ := by by_cases hz : ‖px - py‖ = 0 · simp [hz] · have hp : 0 < ‖px - py‖ := lt_of_le_of_ne (norm_nonneg _) (Ne.symm hz) nlinarith simpa [dist_eq_norm, px, py] using hn -
continuous_convexProjtheorem — Metric projection onto a nonempty closed convex set varies continuously with the point being projected.hypothesesconclusionContinuous (convexProj K hne hc hconv)Proof (Lean source)
@[fun_prop] theorem continuous_convexProj (K : Set E) (hne : K.Nonempty) (hc : IsClosed K) (hconv : Convex ℝ K) : Continuous (convexProj K hne hc hconv) := (convexProj_lipschitz K hne hc hconv).continuous -
measurable_convexProjtheorem — Metric projection onto a nonempty closed convex set is measurable under the Borel sigma-algebra of the Hilbert space.hypothesesconclusionMeasurable (convexProj K hne hc hconv)Proof (Lean source)
@[fun_prop] theorem measurable_convexProj [MeasurableSpace E] [BorelSpace E] (K : Set E) (hne : K.Nonempty) (hc : IsClosed K) (hconv : Convex ℝ K) : Measurable (convexProj K hne hc hconv) := (continuous_convexProj K hne hc hconv).measurable -
frobDist_eq_normtheorem — The Frobenius distance between two finite real matrices equals the Euclidean norm of their difference after vectorizing the entries.hypothesesProof (Lean source)
-
frobDist_commtheorem — Frobenius distance is symmetric in its two matrix arguments. -
frobDist_triangletheorem — Frobenius distance satisfies the triangle inequality.hypothesesProof (Lean source)
theorem frobDist_triangle (A B D : Matrix (Fin p) (Fin p) ℝ) : frobDist A D ≤ frobDist A B + frobDist B D := by rw [frobDist_eq_norm, frobDist_eq_norm, frobDist_eq_norm] exact norm_sub_le_norm_sub_add_norm_sub (mtx p A) (mtx p B) (mtx p D) -
loewnerSet_nonemptytheorem — A Loewner interval with ordered scalar endpoints is nonempty.Proof (Lean source)
theorem loewnerSet_nonempty (p : ℕ) (c C : ℝ) (hcC : c ≤ C) : (loewnerSet p c C).Nonempty := by refine ⟨c • (1 : Matrix (Fin p) (Fin p) ℝ), ?_⟩ constructor · simpa using (Matrix.PosSemidef.zero : (0 : Matrix (Fin p) (Fin p) ℝ).PosSemidef) · convert (Matrix.PosSemidef.one.smul (α := ℝ) (sub_nonneg.mpr hcC) : ((C - c) • (1 : Matrix (Fin p) (Fin p) ℝ)).PosSemidef) using 1 ext i j simp only [Matrix.sub_apply, Matrix.smul_apply, smul_eq_mul] ring -
loewnerSet_convextheorem — Every Loewner interval of finite real matrices is convex.Proof (Lean source)
theorem loewnerSet_convex (p : ℕ) (c C : ℝ) : Convex ℝ (loewnerSet p c C) := by intro A hA B hB a b ha hb hab constructor · convert (hA.1.smul (α := ℝ) ha).add (hB.1.smul (α := ℝ) hb) using 1 ext i j simp only [Matrix.add_apply, Matrix.smul_apply, Matrix.sub_apply, smul_eq_mul] rw [show b = 1 - a by linarith] ring · convert (hA.2.smul (α := ℝ) ha).add (hB.2.smul (α := ℝ) hb) using 1 ext i j simp only [Matrix.add_apply, Matrix.smul_apply, Matrix.sub_apply, smul_eq_mul] rw [show b = 1 - a by linarith] ring -
isClosed_posSemideftheorem — Real positive-semidefinite matrices indexed by any finite set form a closed set in the coordinatewise topology.Proof (Lean source)
theorem isClosed_posSemidef {ι : Type*} [Finite ι] : IsClosed {A : Matrix ι ι ℝ | A.PosSemidef} := by classical letI := ofFinite ι rw [show {A : Matrix ι ι ℝ | A.PosSemidef} = {A | A.IsHermitian} ∩ {A | ∀ x, 0 ≤ dotProduct x (A.mulVec x)} by ext A; simp [Matrix.posSemidef_iff_dotProduct_mulVec]] apply IsClosed.inter · rw [show {A : Matrix ι ι ℝ | A.IsHermitian} = ⋂ i, ⋂ j, {A | A i j = A j i} by ext A simp only [IsHermitian, Set.mem_iInter, Set.mem_setOf_eq] constructor · intro h i j exact congr_fun (congr_fun h i) j |>.symm · intro h ext i j exact (h i j).symm] exact isClosed_iInter fun i => isClosed_iInter fun j => isClosed_eq (continuous_id.matrix_elem i j) (continuous_id.matrix_elem j i) · rw [show {A : Matrix ι ι ℝ | ∀ x, 0 ≤ dotProduct x (A.mulVec x)} = ⋂ x, {A | 0 ≤ dotProduct x (A.mulVec x)} by ext A; simp] exact isClosed_iInter fun x => isClosed_Ici.preimage (continuous_const.dotProduct (continuous_id.matrix_mulVec continuous_const)) -
loewnerSet_isClosedtheorem — Every Loewner interval of finite real matrices is closed in the coordinatewise product topology.Proof (Lean source)
theorem loewnerSet_isClosed (p : ℕ) (c C : ℝ) : IsClosed (loewnerSet p c C) := by exact (isClosed_posSemidef (ι := Fin p)).preimage (by fun_prop) |>.inter ((isClosed_posSemidef (ι := Fin p)).preimage (by fun_prop)) -
loewnerSet_posDeftheorem — Every matrix in a Loewner interval with a strictly positive lower endpoint is positive definite.hypothesesp :sharedℕc :sharedℝhc :0 < chG :conclusionG.PosDefProof (Lean source)
-
loewnerProj_memtheorem — When its endpoints are ordered, Loewner projection sends every finite real matrix into the corresponding Loewner interval.hypothesesconclusionloewnerProj p c C G ∈ loewnerSet p c CProof (Lean source)
theorem loewnerProj_mem (hcC : c ≤ C) (G : Matrix (Fin p) (Fin p) ℝ) : loewnerProj p c C G ∈ loewnerSet p c C := by rw [loewnerProj, dif_pos hcC, loewnerProjAux] have hm := convexProj_mem (mtx p '' loewnerSet p c C) ((loewnerSet_nonempty p c C hcC).image (mtx p)) (mtx_image_isClosed p c C) ((loewnerSet_convex p c C).linear_image (mtx p).toLinearMap) (mtx p G) rcases hm with ⟨S, hS, heq⟩ simpa [← heq] using hS -
measurable_loewnerProjtheorem — Loewner projection is measurable under the coordinatewise Borel sigma-algebra on finite real matrix spaces.Proof (Lean source)
@[fun_prop] theorem measurable_loewnerProj (p : ℕ) [MeasurableSpace (Matrix (Fin p) (Fin p) ℝ)] [BorelSpace (Matrix (Fin p) (Fin p) ℝ)] (c C : ℝ) : Measurable (loewnerProj p c C) := by by_cases h : c ≤ C · rw [loewnerProj, dif_pos h] unfold loewnerProjAux have he : (mtx p : Matrix (Fin p) (Fin p) ℝ → EuclideanSpace ℝ (Fin p × Fin p)) = mtxHomeo p := rfl have hes : ((mtx p).symm : EuclideanSpace ℝ (Fin p × Fin p) → Matrix (Fin p) (Fin p) ℝ) = (mtxHomeo p).symm := rfl rw [show (fun G => (mtx p).symm (convexProj (mtx p '' loewnerSet p c C) ((loewnerSet_nonempty p c C h).image (mtx p)) (mtx_image_isClosed p c C) ((loewnerSet_convex p c C).linear_image (mtx p).toLinearMap) (mtx p G))) = (mtxHomeo p).symm ∘ convexProj (mtx p '' loewnerSet p c C) ((loewnerSet_nonempty p c C h).image (mtx p)) (mtx_image_isClosed p c C) ((loewnerSet_convex p c C).linear_image (mtx p).toLinearMap) ∘ mtxHomeo p by funext G; simp [Function.comp_apply, he, hes]] exact (mtxHomeo p).symm.continuous.comp ((continuous_convexProj _ _ _ _).comp (mtxHomeo p).continuous) |>.measurable · rw [loewnerProj, dif_neg h] exact measurable_id -
mulVec_sub_norm_letheorem — Multiplying a vector by the difference of two finite real matrices has Euclidean norm at most their Frobenius distance times the vector's Euclidean norm.hypothesesProof (Lean source)
theorem mulVec_sub_norm_le (A B : Matrix (Fin p) (Fin p) ℝ) (v : Fin p → ℝ) : sqrt (∑ k, ((A - B).mulVec v k) ^ 2) ≤ frobDist A B * sqrt (∑ k, (v k) ^ 2) := by rw [frobDist, ← Real.sqrt_mul (sum_nonneg fun _ _ => sum_nonneg fun _ _ => sq_nonneg (A _ _ - B _ _))] apply Real.sqrt_le_sqrt rw [Finset.sum_mul] apply Finset.sum_le_sum intro k _ simpa [mulVec, dotProduct, frobDist, Matrix.sub_apply] using (Finset.sum_mul_sq_le_sq_mul_sq univ (fun l : Fin p => A k l - B k l) v) -
loewnerSet_inv_mulVec_norm_letheorem — The inverse of a matrix in a Loewner interval with a positive lower endpoint expands Euclidean norm by at most the reciprocal of that endpoint.hypothesesProof (Lean source)
theorem loewnerSet_inv_mulVec_norm_le (hc : 0 < c) {G : Matrix (Fin p) (Fin p) ℝ} (hG : (G - c • (1 : Matrix (Fin p) (Fin p) ℝ)).PosSemidef) (v : Fin p → ℝ) : sqrt (∑ k, (G⁻¹.mulVec v k) ^ 2) ≤ sqrt (∑ k, (v k) ^ 2) / c := by let z := G⁻¹.mulVec v have hpd := loewnerSet_posDef hc hG have hu : IsUnit G := hpd.isUnit have hudet : IsUnit G.det := (Matrix.isUnit_iff_isUnit_det G).mp hu have hGz : G.mulVec z = v := by change G.mulVec (G⁻¹.mulVec v) = v calc _ = (G * G⁻¹).mulVec v := Matrix.mulVec_mulVec v G G⁻¹ _ = v := by rw [Matrix.mul_nonsing_inv G hudet, Matrix.one_mulVec] have hquad := hG.dotProduct_mulVec_nonneg z have hlower : c * ∑ k, (z k) ^ 2 ≤ ∑ k, z k * v k := by rw [Matrix.sub_mulVec, hGz] at hquad have hq : (∑ k, z k * (c * z k)) ≤ ∑ k, z k * v k := by simpa [dotProduct, Matrix.smul_mulVec, Matrix.one_mulVec, mul_sub, Finset.sum_sub_distrib] using hquad calc c * ∑ k, (z k) ^ 2 = ∑ k, c * (z k) ^ 2 := Finset.mul_sum _ _ _ _ = ∑ k, z k * (c * z k) := by apply Finset.sum_congr rfl intro k hk ring _ ≤ _ := hq have hcs := Real.sum_mul_le_sqrt_mul_sqrt Finset.univ z v have hsquares : c * (sqrt (∑ k, (z k) ^ 2)) ^ 2 ≤ sqrt (∑ k, (z k) ^ 2) * sqrt (∑ k, (v k) ^ 2) := by rw [Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg (z _))] exact hlower.trans hcs have hznonneg := Real.sqrt_nonneg (∑ k, (z k) ^ 2) have hbound : c * sqrt (∑ k, (z k) ^ 2) ≤ sqrt (∑ k, (v k) ^ 2) := by by_cases hz : sqrt (∑ k, (z k) ^ 2) = 0 · simp [hz] · have hzpos : 0 < sqrt (∑ k, (z k) ^ 2) := lt_of_le_of_ne hznonneg (Ne.symm hz) nlinarith apply (le_div_iff₀ hc).2 simpa [z, mul_comm] using hbound -
matrixMeasurableSpaceinstance — For every nonnegative integer dimension, the measurable structure on real square matrices of that dimension is the coordinatewise product $\sigma$-algebra.parametersp :ℕinstancegiven by -
matrixBorelSpaceinstance — For every nonnegative integer dimension, the Borel-space structure on real square matrices of that dimension certifies that their coordinatewise product $\sigma$-algebra equals their Borel $\sigma$-algebra. -
loewnerProj_eq_selftheorem — Every matrix already in a nonempty Loewner interval is unchanged by metric projection onto that interval.hypothesesconclusionloewnerProj p c C G = GProof (Lean source)
theorem loewnerProj_eq_self {p : ℕ} {c C : ℝ} (hcC : c ≤ C) (G : Matrix (Fin p) (Fin p) ℝ) (hG : G ∈ loewnerSet p c C) : loewnerProj p c C G = G := by rw [loewnerProj, dif_pos hcC, loewnerProjAux] rw [convexProj_eq_self (mtx p '' loewnerSet p c C) ((loewnerSet_nonempty p c C hcC).image (mtx p)) (mtx_image_isClosed p c C) ((loewnerSet_convex p c C).linear_image (mtx p).toLinearMap) (mtx p G) ⟨G, hG, rfl⟩] exact (mtx p).symm_apply_apply G
FrechetFunctionalEquation 1 core · 0 supporting Fréchet-style finite-difference arguments appear in classical proofs of independence characterization theorems. ★ affine_of_continuous_of_second_diff_zero
Fréchet's functional equation (degree-one case)
Fréchet-style finite-difference arguments appear in classical proofs of independence
characterization theorems. This file proves the foundational degree-one case: a continuous
function with vanishing second forward difference is affine
(affine_of_continuous_of_second_diff_zero).
The argument is classical: a vanishing second difference makes f midpoint-affine;
subtracting f 0 yields an additive function; a continuous additive map of real
vector spaces is ℝ-linear (AddMonoidHom.toRealLinearMap).
theorem affine_of_continuous_of_second_diff_zero reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Fréchet functional equation, degree one. If f is a continuous function from the reals into a normed real vector space and its second forward difference vanishes: f(x+2s) + f(x) = 2·f(x+s) for all real x and s, then f is affine — there exist vectors a and b such that f(x) = a + x·b for every real x.
Formal statement
hypotheses
E :
Type u_1
ℝ → E
hf :
h2 :
∀ x s : ℝ, f (x + s + s) + f x = f (x + s) + f (x + s)
conclusion
∃ a b : E, ∀ x, f x = a + x • b
Proof (Lean source)
theorem affine_of_continuous_of_second_diff_zero
{f : ℝ → E} (hf : Continuous f)
(h2 : ∀ x s : ℝ, f (x + s + s) + f x = f (x + s) + f (x + s)) :
∃ a b : E, ∀ x, f x = a + x • b := by
-- Midpoint identity.
have hmid : ∀ p q : ℝ, f p + f q = f ((p + q) / 2) + f ((p + q) / 2) := by
intro p q
have h := h2 p ((q - p) / 2)
rw [show p + (q - p) / 2 + (q - p) / 2 = q from by ring,
show p + (q - p) / 2 = (p + q) / 2 from by ring] at h
rw [add_comm (f p) (f q)]; exact h
-- Doubling identity.
have hdouble : ∀ u : ℝ, f (u + u) + f 0 = f u + f u := by
intro u; simpa using h2 0 u
-- Additivity of `x ↦ f x - f 0`.
have hadd : ∀ a b : ℝ, f (a + b) - f 0 = (f a - f 0) + (f b - f 0) := by
intro a b
have hm := hmid (a + a) (b + b)
rw [show (a + a + (b + b)) / 2 = a + b from by ring] at hm
have ha := hdouble a
have hb := hdouble b
-- `(f a + f a) + (f b + f b) = (f (a+b) + f (a+b)) + (f 0 + f 0)`
have hsum : (f a + f a) + (f b + f b) = (f (a + b) + f (a + b)) + (f 0 + f 0) := by
rw [← ha, ← hb,
show (f (a + a) + f 0) + (f (b + b) + f 0)
= (f (a + a) + f (b + b)) + (f 0 + f 0) from by abel,
hm]
-- Cancel the doubling via the `ℝ`-action.
have hXY : f a + f b = f (a + b) + f 0 := by
have h2s : (2 : ℝ) • (f a + f b) = (2 : ℝ) • (f (a + b) + f 0) := by
rw [two_smul, two_smul,
show (f a + f b) + (f a + f b) = (f a + f a) + (f b + f b) from by abel,
show (f (a + b) + f 0) + (f (a + b) + f 0)
= (f (a + b) + f (a + b)) + (f 0 + f 0) from by abel,
hsum]
exact smul_right_injective E two_ne_zero h2s
have hfab : f (a + b) = (f a + f b) - f 0 := eq_sub_of_add_eq hXY.symm
rw [hfab]; abel
-- Continuous additive ⟹ `ℝ`-linear.
have hgcont : Continuous (fun x => f x - f 0) := hf.sub continuous_const
let φ : ℝ →+ E := AddMonoidHom.mk' (fun x => f x - f 0) hadd
let L : ℝ →L[ℝ] E := φ.toRealLinearMap hgcont
have hLx : ∀ x, L x = f x - f 0 := by
intro x
have : ⇑L = ⇑φ := φ.coe_toRealLinearMap hgcont
rw [this]; rfl
refine ⟨f 0, L 1, fun x => ?_⟩
have hlin : f x - f 0 = x • L 1 := by
rw [← hLx x, show L x = L (x • (1 : ℝ)) from by rw [smul_eq_mul, mul_one], map_smul]
rw [← hlin]; abel
GradientCoord 1 core · 0 supporting A single bridge lemma: the a-th coordinate of the (Riesz) gradient of a real-valued function on a finite-dimensional Euclidean space equals the ordinary one-variable derivative of the function along the a-th coordinate l ★ gradient_coord_eq_deriv
Coordinates of a Euclidean gradient as directional derivatives
A single bridge lemma: the a-th coordinate of the (Riesz) gradient of a real-valued function on a
finite-dimensional Euclidean space equals the ordinary one-variable derivative of the function along
the a-th coordinate line. This is the standard tool for computing a gradient coordinate by
coordinate — reduce each entry to a deriv of a one-parameter restriction, which the univariate
calculus API can then evaluate.
lemma gradient_coord_eq_deriv reviewed
⚑ flagged
Causalean.Mathlib
Gradient coordinate as a directional derivative. For a real-valued function f on a finite-dimensional Euclidean space that is differentiable at the point x, the a-th coordinate of its gradient at x equals the derivative at 0 of the one-variable restriction t ↦ f(x + t·eₐ) along the a-th standard basis direction.
Formal statement
hypotheses
Proof (Lean source)
lemma gradient_coord_eq_deriv {ι : Type*} [Fintype ι] [DecidableEq ι]
(f : EuclideanSpace ℝ ι → ℝ)
(x : EuclideanSpace ℝ ι) (a : ι)
(hf : DifferentiableAt ℝ f x) :
(gradient f x) a =
deriv (fun t : ℝ => f (x + t • single a (1 : ℝ))) 0 := by
have hinner : ⟪EuclideanSpace.single a (1 : ℝ), gradient f x⟫_ℝ =
fderiv ℝ f x (single a (1 : ℝ)) := by
rw [real_inner_comm]
exact inner_gradient_left (𝕜 := ℝ) (f := f) (x := x)
(y := single a (1 : ℝ))
have hline :
HasDerivAt
(fun t : ℝ => x + t • single a (1 : ℝ))
(single a (1 : ℝ)) 0 := by
simpa using
(((hasDerivAt_id (0 : ℝ)).smul_const (single a (1 : ℝ))).const_add x)
have hderiv :
HasDerivAt
(fun t : ℝ => f (x + t • single a (1 : ℝ)))
(fderiv ℝ f x (single a (1 : ℝ))) 0 := by
have hf' :
HasFDerivAt f (fderiv ℝ f x)
(x + (0 : ℝ) • single a (1 : ℝ)) := by
simpa using hf.hasFDerivAt
exact hf'.comp_hasDerivAt (0 : ℝ) hline
calc
(gradient f x) a = ⟪EuclideanSpace.single a (1 : ℝ), gradient f x⟫_ℝ := by
have hs :
⟪EuclideanSpace.single a (1 : ℝ), gradient f x⟫_ℝ = (gradient f x) a := by
simpa using EuclideanSpace.inner_single_left a (1 : ℝ) (gradient f x)
exact hs.symm
_ = fderiv ℝ f x (single a (1 : ℝ)) := hinner
_ = deriv (fun t : ℝ => f (x + t • single a (1 : ℝ))) 0 :=
hderiv.deriv.symm
HalfDiscPolar 3 core · 14 supporting This module derives weighted polar-integration formulas on upper half-discs, including radial mass identities, odd-angular cancellation, quadratic angular moments, and translation-invariant variants. ★ halfDisc_weighted_polar_integral
Polar integration and cancellation on half-discs
This module derives weighted polar-integration formulas on upper half-discs, including radial mass identities, odd-angular cancellation, quadratic angular moments, and translation-invariant variants.
def planarRadius reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a point in the real coordinate plane, the planar radius is its Euclidean distance from the origin, namely for coordinates .
Definition (Lean source)
def planarAngle reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a point in the real coordinate plane, the planar angle is the angular coordinate assigned by the polar-coordinate chart.
Definition (Lean source)
parameters
z :
ℝ × ℝ
def
planarAngle z :
ℝ
given by
(polarCoord z).2
lemma halfDisc_weighted_polar_integral reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For radial and angular weight functions g and h and a radius r, the integral of the product g(radius)·h(angle) over the open upper half-disc of radius r factors as the product of the radial integral ∫ s·g(s) ds over (0, r] and the angular integral ∫ h(θ) dθ over (0, π).
Formal statement
hypotheses
g h :
ℝ → ℝ
r :
ℝ
conclusion
Proof (Lean source)
-- @node: halfDisc_weighted_polar_integral
lemma halfDisc_weighted_polar_integral
(g h : ℝ → ℝ) (r : ℝ) :
(∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r},
g (planarRadius z) * h (planarAngle z)) =
(∫ s : ℝ in Ioc 0 r, s * g s) *
(∫ θ : ℝ in Ioo 0 Real.pi, h θ) := by
let D : Set (ℝ × ℝ) := {z | 0 < z.2 ∧ planarRadius z ≤ r}
let E : Set (ℝ × ℝ) := Ioc 0 r ×ˢ Ioo 0 Real.pi
have hD : MeasurableSet D := by
exact (measurableSet_lt measurable_const measurable_snd).inter
(measurableSet_le
((measurable_fst.pow_const 2).add (measurable_snd.pow_const 2)).sqrt
measurable_const)
have hE : MeasurableSet E := measurableSet_Ioc.prod measurableSet_Ioo
change (∫ z : ℝ × ℝ in D,
g (planarRadius z) * h (planarAngle z)) = _
rw [← integral_indicator hD, ← integral_comp_polarCoord_symm]
rw [show (∫ p in polarCoord.target,
p.1 • D.indicator
(fun z => g (planarRadius z) * h (planarAngle z))
(polarCoord.symm p)) =
∫ p in E, (p.1 * g p.1) * h p.2 by
rw [← integral_indicator polarCoord.open_target.measurableSet,
← integral_indicator hE]
apply integral_congr_ae
filter_upwards with p
by_cases hp : p ∈ polarCoord.target
· have hptarget := hp
simp only [polarCoord_target, mem_prod, mem_Ioi, mem_Ioo] at hp
have hinv := polarCoord.right_inv hp
have hrs : planarRadius (polarCoord.symm p) = p.1 :=
congrArg Prod.fst hinv
have htheta : planarAngle (polarCoord.symm p) = p.2 :=
congrArg Prod.snd hinv
have hsin : 0 < sin p.2 ↔ 0 < p.2 := by
constructor
· intro hs
by_contra hn
exact (not_lt_of_ge (Real.sin_nonpos_of_nonpos_of_neg_pi_le
(le_of_not_gt hn) hp.2.1.le)) hs
· intro htheta0
exact Real.sin_pos_of_pos_of_lt_pi htheta0 hp.2.2
have hy : 0 < p.1 * sin p.2 ↔ 0 < p.2 :=
(mul_pos_iff_of_pos_left hp.1).trans hsin
have hmem : polarCoord.symm p ∈ D ↔ p ∈ E := by
change (0 < (polarCoord.symm p).2 ∧
planarRadius (polarCoord.symm p) ≤ r) ↔
(0 < p.1 ∧ p.1 ≤ r) ∧ 0 < p.2 ∧ p.2 < Real.pi
rw [hrs]
simp only [polarCoord_symm_apply]
rw [hy]
constructor
· rintro ⟨hptheta, hpr⟩
exact ⟨⟨hp.1, hpr⟩, hptheta, hp.2.2⟩
· rintro ⟨⟨_, hpr⟩, hptheta0, _⟩
exact ⟨hptheta0, hpr⟩
by_cases hmemD : polarCoord.symm p ∈ D
· rw [indicator_of_mem hptarget, indicator_of_mem hmemD,
indicator_of_mem (hmem.mp hmemD), hrs, htheta]
simp [smul_eq_mul]
ring
· rw [indicator_of_mem hptarget]
simp only [indicator]
rw [if_neg hmemD, if_neg (mt hmem.mpr hmemD)]
simp
· have hpE : p ∉ E := by
rintro ⟨⟨hp0, _⟩, hptheta0, hpthetapi⟩
apply hp
simp only [polarCoord_target, mem_prod, mem_Ioi, mem_Ioo]
exact ⟨hp0, lt_trans (neg_lt_zero.mpr Real.pi_pos) hptheta0, hpthetapi⟩
simp only [indicator]
rw [if_neg hp, if_neg hpE]
]
change (∫ p in Ioc 0 r ×ˢ Ioo 0 Real.pi,
(p.1 * g p.1) * h p.2) = _
rw [Measure.volume_eq_prod]
exact setIntegral_prod_mul (μ := volume) (ν := volume)
(fun s : ℝ => s * g s) h (Ioc 0 r) (Ioo 0 Real.pi)
14 supporting declarations (lemmas, instances)
-
planarRadius_measurablelemma — The Euclidean radius on the coordinate plane is Borel measurable.conclusionProof (Lean source)
-- @node: planarRadius_measurable @[fun_prop] lemma planarRadius_measurable : Measurable planarRadius := by exact ((measurable_fst.pow_const 2).add (measurable_snd.pow_const 2)).sqrt -
integral_cos_zero_to_pilemma — The cosine has zero integral on a half-circle. -
integral_cos_sq_zero_to_pilemma — The quadratic cosine moment on a half-circle is π / 2. -
halfDisc_weighted_cos_cancellationlemma — A cosine angular tilt has zero integral against every radial weight on an upper half-disc.hypothesesg :ℝ → ℝr :ℝconclusion= 0Proof (Lean source)
-- @node: halfDisc_weighted_cos_cancellation lemma halfDisc_weighted_cos_cancellation (g : ℝ → ℝ) (r : ℝ) : (∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r}, g (planarRadius z) * cos (planarAngle z)) = 0 := by rw [halfDisc_weighted_polar_integral] have hcos : (∫ θ : ℝ in Ioo 0 pi, cos θ) = 0 := by rw [← integral_Ioc_eq_integral_Ioo] exact integral_cos_zero_to_pi rw [hcos, mul_zero] -
halfDisc_radialSet_weighted_cos_cancellationlemma — A cosine angular tilt has zero mass on every measurable radial subset of an upper half-disc. This is the setwise interface used to identify radial pushforwards, rather than merely their total masses.hypothesesconclusion(∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r} ∩ planarRadius ⁻¹' A, g (planarRadius z) * cos (planarAngle z))= 0Proof (Lean source)
-- @node: halfDisc_radialSet_weighted_cos_cancellation lemma halfDisc_radialSet_weighted_cos_cancellation (g : ℝ → ℝ) (r : ℝ) {A : Set ℝ} (hA : MeasurableSet A) : (∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r} ∩ planarRadius ⁻¹' A, g (planarRadius z) * cos (planarAngle z)) = 0 := by let D : Set (ℝ × ℝ) := {z | 0 < z.2 ∧ planarRadius z ≤ r} let R : Set (ℝ × ℝ) := planarRadius ⁻¹' A have hR : MeasurableSet R := hA.preimage planarRadius_measurable have hcancel := halfDisc_weighted_cos_cancellation (A.indicator g) r change (∫ z : ℝ × ℝ in D ∩ R, g (planarRadius z) * cos (planarAngle z)) = 0 rw [← hcancel] have hDR : D ∩ R = R ∩ D := inter_comm D R rw [hDR] rw [← Measure.restrict_restrict hR] rw [← integral_indicator hR] apply integral_congr_ae filter_upwards with z simp only [R, indicator, mem_preimage] split_ifs <;> simp_all -
planarFirst_div_radius_eq_coslemma — On the open upper half-plane, the first coordinate divided by the radius is the cosine of the polar angle.Proof (Lean source)
-- @node: planarFirst_div_radius_eq_cos lemma planarFirst_div_radius_eq_cos (z : ℝ × ℝ) (hz : 0 < z.2) : z.1 / planarRadius z = cos (planarAngle z) := by have hsource : z ∈ polarCoord.source := by simp only [polarCoord_source, mem_union, mem_setOf_eq] exact inr hz.ne' have hinv := polarCoord.left_inv hsource have hx := congrArg Prod.fst hinv have hr : planarRadius z = (polarCoord z).1 := rfl simp only [polarCoord_symm_apply] at hx rw [hr] unfold planarAngle have hpos : 0 < (polarCoord z).1 := by simpa only [polarCoord_target, mem_prod, mem_Ioi, mem_Ioo] using (polarCoord.map_source hsource).1 apply (div_eq_iff hpos.ne').2 rw [← hx] ring -
halfDisc_weighted_first_div_radius_cancellationlemma — A radial weight times the Cartesian direction cosine has zero integral on an open upper half-disc.hypothesesg :ℝ → ℝr :ℝconclusion= 0Proof (Lean source)
-- @node: halfDisc_weighted_first_div_radius_cancellation lemma halfDisc_weighted_first_div_radius_cancellation (g : ℝ → ℝ) (r : ℝ) : (∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r}, g (planarRadius z) * (z.1 / planarRadius z)) = 0 := by have heq : (∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r}, g (planarRadius z) * (z.1 / planarRadius z)) = ∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r}, g (planarRadius z) * cos (planarAngle z) := by apply integral_congr_ae have hD : MeasurableSet {z : ℝ × ℝ | 0 < z.2 ∧ planarRadius z ≤ r} := by exact (measurableSet_lt measurable_const measurable_snd).inter (measurableSet_le ((measurable_fst.pow_const 2).add (measurable_snd.pow_const 2)).sqrt measurable_const) exact ae_restrict_of_forall_mem hD fun z hz => by change g (planarRadius z) * (z.1 / planarRadius z) = g (planarRadius z) * cos (planarAngle z) rw [planarFirst_div_radius_eq_cos z hz.1] rw [heq] exact halfDisc_weighted_cos_cancellation g r -
closedHalfDisc_weighted_first_div_radius_cancellationlemma — Replacing the open diameter of an upper half-disc by the closed diameter does not affect the Cartesian cosine integral.hypothesesg :ℝ → ℝr :ℝconclusion= 0Proof (Lean source)
-- @node: closedHalfDisc_weighted_first_div_radius_cancellation lemma closedHalfDisc_weighted_first_div_radius_cancellation (g : ℝ → ℝ) (r : ℝ) : (∫ z : ℝ × ℝ in {z | 0 ≤ z.2 ∧ planarRadius z ≤ r}, g (planarRadius z) * (z.1 / planarRadius z)) = 0 := by rw [setIntegral_congr_set (show {z : ℝ × ℝ | 0 ≤ z.2 ∧ planarRadius z ≤ r} =ᵐ[volume] {z | 0 < z.2 ∧ planarRadius z ≤ r} by show ∀ᵐ z ∂(volume : Measure (ℝ × ℝ)), (0 ≤ z.2 ∧ planarRadius z ≤ r) = (0 < z.2 ∧ planarRadius z ≤ r) rw [ae_iff] apply measure_mono_null (t := {z : ℝ × ℝ | z.2 = 0}) · intro z hz simp only [mem_setOf_eq] by_contra hy apply hz apply propext constructor · rintro ⟨hy0, hr⟩ exact ⟨lt_of_le_of_ne hy0 (Ne.symm hy), hr⟩ · rintro ⟨hy0, hr⟩ exact ⟨hy0.le, hr⟩ · rw [Measure.volume_eq_prod] rw [show {z : ℝ × ℝ | z.2 = 0} = univ ×ˢ ({0} : Set ℝ) by ext z simp] rw [Measure.prod_prod] simp)] exact halfDisc_weighted_first_div_radius_cancellation g r -
translatedClosedHalfDisc_weighted_first_div_radius_cancellationlemma — Translation preserves the zero Cartesian-cosine integral over a closed upper half-disc.hypothesesg :ℝ → ℝr :ℝc :ℝ × ℝconclusion(∫ z : ℝ × ℝ in {z | 0 ≤ (z - c).2 ∧ planarRadius (z - c) ≤ r}, g (planarRadius (z - c)) * ((z - c).1 / planarRadius (z - c)))= 0Proof (Lean source)
-- @node: translatedClosedHalfDisc_weighted_first_div_radius_cancellation lemma translatedClosedHalfDisc_weighted_first_div_radius_cancellation (g : ℝ → ℝ) (r : ℝ) (c : ℝ × ℝ) : (∫ z : ℝ × ℝ in {z | 0 ≤ (z - c).2 ∧ planarRadius (z - c) ≤ r}, g (planarRadius (z - c)) * ((z - c).1 / planarRadius (z - c))) = 0 := by let D : Set (ℝ × ℝ) := {u | 0 ≤ u.2 ∧ planarRadius u ≤ r} let T : (ℝ × ℝ) → (ℝ × ℝ) := fun u => c + u have hT : MeasurableEmbedding T := (Homeomorph.addLeft c).measurableEmbedding have hmp : MeasurePreserving T (volume : Measure (ℝ × ℝ)) volume := measurePreserving_add_left volume c have hset : {z : ℝ × ℝ | 0 ≤ (z - c).2 ∧ planarRadius (z - c) ≤ r} = T '' D := by ext z constructor · intro hz refine ⟨z - c, ?_, ?_⟩ · exact hz · simp [T] · rintro ⟨u, hu, rfl⟩ simpa [T, D] using hu rw [hset, hmp.setIntegral_image_emb hT] have hfun : (fun u : ℝ × ℝ => g (planarRadius (T u - c)) * ((T u - c).1 / planarRadius (T u - c))) = fun u => g (planarRadius u) * (u.1 / planarRadius u) := by funext u simp [T] rw [hfun] exact closedHalfDisc_weighted_first_div_radius_cancellation g r -
halfDisc_weighted_cos_sqlemma — The cosine-squared angular moment converts a radial weight into the nonzero π/2 factor used to cancel the affine regression term.hypothesesg :ℝ → ℝr :ℝconclusionProof (Lean source)
-- @node: halfDisc_weighted_cos_sq lemma halfDisc_weighted_cos_sq (g : ℝ → ℝ) (r : ℝ) : (∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r}, g (planarRadius z) * cos (planarAngle z) ^ 2) = (∫ s : ℝ in Ioc 0 r, s * g s) * (pi / 2) := by have hcosSq : (∫ θ : ℝ in Ioo 0 pi, cos θ ^ 2) = pi / 2 := by rw [← integral_Ioc_eq_integral_Ioo] exact integral_cos_sq_zero_to_pi calc _ = (∫ s : ℝ in Ioc 0 r, s * g s) * (∫ θ : ℝ in Ioo 0 pi, cos θ ^ 2) := halfDisc_weighted_polar_integral g (fun θ => cos θ ^ 2) r _ = _ := by rw [hcosSq] -
halfDisc_radial_integrallemma — A radial integrand on a half-disc admits the expected polar-coordinate decomposition.hypothesesg :ℝ → ℝr :ℝconclusion(∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r}, g (planarRadius z))Proof (Lean source)
-- @node: halfDisc_radial_integral lemma halfDisc_radial_integral (g : ℝ → ℝ) (r : ℝ) : (∫ z : ℝ × ℝ in {z | 0 < z.2 ∧ planarRadius z ≤ r}, g (planarRadius z)) = ∫ s : ℝ in Ioc 0 r, Real.pi * s * g s := by let D : Set (ℝ × ℝ) := {z | 0 < z.2 ∧ planarRadius z ≤ r} let E : Set (ℝ × ℝ) := Ioc 0 r ×ˢ Ioo 0 Real.pi have hD : MeasurableSet D := by exact (measurableSet_lt measurable_const measurable_snd).inter (measurableSet_le ((measurable_fst.pow_const 2).add (measurable_snd.pow_const 2)).sqrt measurable_const) have hE : MeasurableSet E := measurableSet_Ioc.prod measurableSet_Ioo change (∫ z : ℝ × ℝ in D, g (planarRadius z)) = _ rw [← integral_indicator hD, ← integral_comp_polarCoord_symm] rw [show (∫ p in polarCoord.target, p.1 • D.indicator (fun z => g (planarRadius z)) (polarCoord.symm p)) = ∫ p in E, p.1 * g p.1 by rw [← integral_indicator polarCoord.open_target.measurableSet, ← integral_indicator hE] apply integral_congr_ae filter_upwards with p by_cases hp : p ∈ polarCoord.target · have hptarget := hp simp only [polarCoord_target, mem_prod, mem_Ioi, mem_Ioo] at hp have hrs : planarRadius (polarCoord.symm p) = p.1 := by exact congrArg fst (polarCoord.right_inv hp) have hsin : 0 < sin p.2 ↔ 0 < p.2 := by constructor · intro hs by_contra hn exact (not_lt_of_ge (Real.sin_nonpos_of_nonpos_of_neg_pi_le (le_of_not_gt hn) hp.2.1.le)) hs · intro htheta exact Real.sin_pos_of_pos_of_lt_pi htheta hp.2.2 have hy : 0 < p.1 * sin p.2 ↔ 0 < p.2 := (mul_pos_iff_of_pos_left hp.1).trans hsin have hmem : polarCoord.symm p ∈ D ↔ p ∈ E := by change (0 < (polarCoord.symm p).2 ∧ planarRadius (polarCoord.symm p) ≤ r) ↔ (0 < p.1 ∧ p.1 ≤ r) ∧ 0 < p.2 ∧ p.2 < Real.pi rw [hrs] simp only [polarCoord_symm_apply] rw [hy] constructor · rintro ⟨hptheta, hpr⟩ exact ⟨⟨hp.1, hpr⟩, hptheta, hp.2.2⟩ · rintro ⟨⟨_, hpr⟩, hptheta, _⟩ exact ⟨hptheta, hpr⟩ by_cases h : polarCoord.symm p ∈ D · rw [indicator_of_mem hptarget, indicator_of_mem h, indicator_of_mem (hmem.mp h), hrs] rfl · rw [indicator_of_mem hptarget] simp only [indicator] rw [if_neg h, if_neg (mt hmem.mpr h)] simp · have hpE : p ∉ E := by rintro ⟨⟨hp0, _⟩, hptheta0, hpthetapi⟩ apply hp simp only [polarCoord_target, mem_prod, mem_Ioi, mem_Ioo] exact ⟨hp0, lt_trans (neg_lt_zero.mpr Real.pi_pos) hptheta0, hpthetapi⟩ simp only [indicator] rw [if_neg hp, if_neg hpE] ] rw [show (fun p : ℝ × ℝ => p.1 * g p.1) = fun p => (p.1 * g p.1) * (1 : ℝ) by funext p; ring] change (∫ p in Ioc 0 r ×ˢ Ioo 0 Real.pi, (p.1 * g p.1) * (1 : ℝ)) = _ rw [Measure.volume_eq_prod] rw [setIntegral_prod_mul (μ := volume) (ν := volume) (fun s : ℝ => s * g s) (fun _ : ℝ => (1 : ℝ)) (Ioc 0 r) (Ioo 0 Real.pi)] rw [setIntegral_one_eq_measureReal, Measure.real_def, Real.volume_Ioo] simp only [sub_zero, ENNReal.toReal_ofReal Real.pi_pos.le] rw [mul_comm, ← integral_const_mul] apply integral_congr_ae filter_upwards with s ring -
halfDisc_cos_radial_cancellationlemma — Multiplication by cosine contributes zero after angular integration on every radial shell.hypothesesg :ℝ → ℝr :ℝProof (Lean source)
lemma halfDisc_cos_radial_cancellation (g : ℝ → ℝ) (r : ℝ) : (∫ s : ℝ in Ioc 0 r, s * g s * (∫ θ : ℝ in Ioc 0 pi, cos θ)) = 0 := by rw [integral_cos_zero_to_pi] simp -
translatedHalfDisc_weighted_cos_cancellationlemma — Translating an upper half-disc does not change the cosine cancellation.hypothesesg :ℝ → ℝr :ℝc :ℝ × ℝconclusion(∫ z : ℝ × ℝ in (fun u : ℝ × ℝ => c + u) '' {u | 0 < u.2 ∧ planarRadius u ≤ r}, g (planarRadius (z - c)) * cos (planarAngle (z - c)))= 0Proof (Lean source)
-- @node: translatedHalfDisc_weighted_cos_cancellation lemma translatedHalfDisc_weighted_cos_cancellation (g : ℝ → ℝ) (r : ℝ) (c : ℝ × ℝ) : (∫ z : ℝ × ℝ in (fun u : ℝ × ℝ => c + u) '' {u | 0 < u.2 ∧ planarRadius u ≤ r}, g (planarRadius (z - c)) * cos (planarAngle (z - c))) = 0 := by let D : Set (ℝ × ℝ) := {u | 0 < u.2 ∧ planarRadius u ≤ r} let T : (ℝ × ℝ) → (ℝ × ℝ) := fun u => c + u have hT : MeasurableEmbedding T := (Homeomorph.addLeft c).measurableEmbedding have hmp : MeasurePreserving T (volume : Measure (ℝ × ℝ)) volume := measurePreserving_add_left volume c rw [show (fun u : ℝ × ℝ => c + u) = T by rfl] rw [hmp.setIntegral_image_emb hT (fun z => g (planarRadius (z - c)) * cos (planarAngle (z - c))) D] have hpoint : (fun u : ℝ × ℝ => g (planarRadius (T u - c)) * cos (planarAngle (T u - c))) = fun u => g (planarRadius u) * cos (planarAngle u) := by funext u simp [T] rw [hpoint] exact halfDisc_weighted_cos_cancellation g r -
translatedHalfDisc_radialSet_weighted_cos_cancellationlemma — Translation preserves cosine cancellation on every measurable radial subset of a half-disc.hypothesesconclusion(∫ z : ℝ × ℝ in ((fun u : ℝ × ℝ => c + u) '' {u | 0 < u.2 ∧ planarRadius u ≤ r}) ∩ {z | planarRadius (z - c) ∈ A}, g (planarRadius (z - c)) * cos (planarAngle (z - c)))= 0Proof (Lean source)
-- @node: translatedHalfDisc_radialSet_weighted_cos_cancellation lemma translatedHalfDisc_radialSet_weighted_cos_cancellation (g : ℝ → ℝ) (r : ℝ) (c : ℝ × ℝ) {A : Set ℝ} (hA : MeasurableSet A) : (∫ z : ℝ × ℝ in ((fun u : ℝ × ℝ => c + u) '' {u | 0 < u.2 ∧ planarRadius u ≤ r}) ∩ {z | planarRadius (z - c) ∈ A}, g (planarRadius (z - c)) * cos (planarAngle (z - c))) = 0 := by let D : Set (ℝ × ℝ) := (fun u : ℝ × ℝ => c + u) '' {u | 0 < u.2 ∧ planarRadius u ≤ r} let R : Set (ℝ × ℝ) := {z | planarRadius (z - c) ∈ A} have hR : MeasurableSet R := by exact hA.preimage (planarRadius_measurable.comp (by fun_prop)) have hcancel := translatedHalfDisc_weighted_cos_cancellation (A.indicator g) r c change (∫ z : ℝ × ℝ in D ∩ R, g (planarRadius (z - c)) * cos (planarAngle (z - c))) = 0 rw [← hcancel] have hDR : D ∩ R = R ∩ D := inter_comm D R rw [hDR] rw [← Measure.restrict_restrict hR] rw [← integral_indicator hR] apply integral_congr_ae filter_upwards with z simp only [R, indicator, mem_setOf_eq] split_ifs <;> simp_all
LineSecondDeriv 2 core · 6 supporting For f : E → ℝ and a direction d : E, the restriction of f to the line s ↦ f (q + s • d) has first and second derivatives expressible as directional derivatives of f at the moving base point q + t • d: * deriv_line : deri ★ convexOn_deriv2_nonneg
Second directional derivative along an affine line
For f : E → ℝ and a direction d : E, the restriction of f to the line
s ↦ f (q + s • d) has first and second derivatives expressible as directional
derivatives of f at the moving base point q + t • d:
* deriv_line : deriv (fun s => f (q + s • d)) t = fderiv ℝ f (q + t • d) d
* deriv_deriv_line: `deriv (deriv fun s => f (q + s • d)) t
= secondDirDeriv f d (q + t • d)`
where secondDirDeriv f d q = fderiv ℝ (fun x => fderiv ℝ f x d) q d. Two consequences
make secondDirDeriv usable as a curvature modulus over a constraint set:
* continuous_secondDirDeriv : it is continuous in the base point (so it is bounded on a
compact set, giving the BddAbove needed for a ciSup), and
* convexOn_deriv2_nonneg : a convex C² function of one variable has nonnegative second
derivative at interior points (so such a modulus is nonnegative).
Mathlib has convexOn_of_deriv2_nonneg (sufficiency) but not the converse used here.
The statements are objective-agnostic: callers supply ContDiff ℝ 2 f and read off the
directional curvature. This is the substrate behind the dirModulus / EnvelopeLineC2Data
discharge for the reciprocal-product variance envelope.
def secondDirDeriv reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a real normed vector space, a real-valued function on that space, a direction vector, and a base point, the second directional derivative is the directional derivative at the base point, in the given direction, of the function mapping a point to the directional derivative of the original function in that direction.
lemma convexOn_deriv2_nonneg reviewed
⚑ flagged
Causalean.Mathlib.Analysis
A convex function of one real variable has nonnegative second derivative at interior points of its domain. If g is convex on the set S, differentiable at every point of S, x lies in the interior of S, and the derivative of g is itself differentiable at x, then the second derivative of g at x is nonnegative.
Formal statement
hypotheses
S :
Set ℝ
g :
ℝ → ℝ
x :
ℝ
hconv :
ConvexOn ℝ S g
hdiff :
∀ y ∈ S, DifferentiableAt ℝ g y
hx :
x ∈ interior S
hdd :
DifferentiableAt ℝ (deriv g) x
Proof (Lean source)
lemma convexOn_deriv2_nonneg {S : Set ℝ} {g : ℝ → ℝ} {x : ℝ}
(hconv : ConvexOn ℝ S g) (hdiff : ∀ y ∈ S, DifferentiableAt ℝ g y)
(hx : x ∈ interior S) (hdd : DifferentiableAt ℝ (deriv g) x) :
0 ≤ deriv (deriv g) x := by
have hacc : AccPt x (𝓟 S) := by
have hacc' : AccPt x (𝓟 (interior S)) := by
simpa using
(PerfectSpace.univ_preperfect.open_inter isOpen_interior x ⟨hx, mem_univ x⟩)
exact hacc'.mono (principal_mono.mpr interior_subset)
exact hdd.hasDerivAt.hasDerivWithinAt.nonneg_of_monotoneOn hacc
(hconv.monotoneOn_deriv hdiff)
6 supporting declarations (lemmas, instances)
-
hasDerivAt_linelemma — The line s ↦ q + s • d is differentiable with derivative d, as a HasDerivAt.Proof (Lean source)
lemma hasDerivAt_line (q d : E) (t : ℝ) : HasDerivAt (fun s : ℝ => q + s • d) d t := by simpa using ((hasDerivAt_id t).smul_const d).const_add q -
deriv_linelemma — First directional derivative along a line.hypothesesProof (Lean source)
lemma deriv_line {f : E → ℝ} (q d : E) (t : ℝ) (hf : DifferentiableAt ℝ f (q + t • d)) : deriv (fun s : ℝ => f (q + s • d)) t = fderiv ℝ f (q + t • d) d := by exact (hf.hasFDerivAt.comp_hasDerivAt t (hasDerivAt_line q d t)).deriv -
contDiff_one_fderiv_applylemma — x ↦ fderiv ℝ f x d is Cⁿ when f is Cⁿ⁺¹. It is the composition of the derivative map with the continuous linear evaluation L ↦ L d.hypothesesProof (Lean source)
lemma contDiff_one_fderiv_apply {n : ℕ} {f : E → ℝ} (hf : ContDiff ℝ (n + 1) f) (d : E) : ContDiff ℝ n (fun x => fderiv ℝ f x d) := by exact (ContinuousLinearMap.apply ℝ ℝ d).contDiff.comp (hf.fderiv_right (m := n) (by rfl)) -
differentiable_fderiv_applylemma — x ↦ fderiv ℝ f x d is differentiable when f is C².hypothesesconclusionDifferentiable ℝ (fun x => fderiv ℝ f x d)Proof (Lean source)
lemma differentiable_fderiv_apply {f : E → ℝ} (hf : ContDiff ℝ 2 f) (d : E) : Differentiable ℝ (fun x => fderiv ℝ f x d) := (contDiff_one_fderiv_apply hf d).differentiable (by norm_num) -
deriv_deriv_linelemma — Second directional derivative along a line. The second derivative of the line restriction at parameter t is the second directional derivative of f at the moving base point q + t • d. Note this is an identity of deriv (not derivWithin): it holds at every t because the line restriction is differentiable on all of ℝ.hypothesesconclusionderiv (deriv fun s : ℝ => f (q + s • d)) t = secondDirDeriv f d (q + t • d)Proof (Lean source)
lemma deriv_deriv_line {f : E → ℝ} (hf : ContDiff ℝ 2 f) (q d : E) (t : ℝ) : deriv (deriv fun s : ℝ => f (q + s • d)) t = secondDirDeriv f d (q + t • d) := by have hstep : (deriv fun s : ℝ => f (q + s • d)) = fun s => fderiv ℝ f (q + s • d) d := by funext s exact deriv_line q d s ((hf.differentiable two_ne_zero) (q + s • d)) rw [hstep] exact deriv_line q d t ((differentiable_fderiv_apply hf d) (q + t • d)) -
continuous_secondDirDerivlemma — The curvature modulus is continuous in the base point. Hence bounded on any compact set, which supplies the BddAbove hypothesis of le_ciSup.hypothesesconclusionContinuous (secondDirDeriv f d)Proof (Lean source)
@[fun_prop] lemma continuous_secondDirDeriv {f : E → ℝ} (hf : ContDiff ℝ 2 f) (d : E) : Continuous (secondDirDeriv f d) := by exact (ContinuousLinearMap.apply ℝ ℝ d).continuous.comp ((contDiff_one_fderiv_apply hf d).continuous_fderiv (by norm_num))
LogRatioStability 6 core · 6 supporting This module defines explicit uniform C¹ and C² control on a set. ★ logRatioDerivative_fixedSign_open_C1
Uniform C1 stability of positive log-ratio derivatives
This module defines explicit uniform C¹ and C² control on a set. It proves continuity of
reciprocal, quotient, logarithm, and the within-derivative of a positive log ratio under uniform
C¹ convergence, then packages openness of a strict fixed-sign derivative margin on a compact
real interval.
def UniformlyOn reviewed
⚑ flagged
Causalean.Mathlib.Analysis
A sequence of real-valued functions converges uniformly on K when every positive error tolerance eventually controls all points of K.
Definition (Lean source)
parameters
def
UniformlyOn K f g :
Prop
given by
∃ N, ∀ n ≥ N, ∀ x ∈ K, |f n x - g x| < ε
def UniformC1On reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Uniform C¹ convergence on a real set means uniform convergence of both function values and their first within-derivatives.
Definition (Lean source)
def C1CloseOn reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Two real functions are uniformly C¹-close on a set when both values and first within-derivatives differ by less than the same radius everywhere on the set.
Definition (Lean source)
parameters
def
C1CloseOn K ε f g :
Prop
given by
clause 1
x ∈ K :
|f x - g x| < ε
def C2CloseOn reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Two real functions are uniformly C²-close when they are uniformly C¹-close and their second within-derivatives differ by less than the same radius.
Definition (Lean source)
parameters
def
C2CloseOn K ε f g :
Prop
given by
clause 1
C1CloseOn K ε f g
clause 2
x ∈ K :
|derivWithin (fun y ↦ derivWithin f K y) K x
- derivWithin (fun y ↦ derivWithin g K y) K x| < ε
def logRatio reviewed
⚑ flagged
Causalean.Mathlib.Analysis
The log ratio of q to p is the pointwise function x ↦ log (q x / p x).
Definition (Lean source)
theorem logRatioDerivative_fixedSign_open_C1 reviewed
⚑ flagged
Causalean.Mathlib.Analysis
A nondegenerate compact interval and positive lower and derivative margins, two continuously differentiable center functions, their shared lower bounds, a chosen orientation, and a derivative margin in that orientation ensure a positive uniform C¹ neighborhood in which both perturbed functions stay positive and their log-ratio derivative retains that orientation.
Formal statement
hypotheses
a b m margin :
ℝ
hab :
a < b
hm :
0 < m
hmargin :
0 < margin
q p :
ℝ → ℝ
hq :
ContDiffOn ℝ 1 q (Icc a b)
hp :
ContDiffOn ℝ 1 p (Icc a b)
hqlower :
∀ x ∈ Icc a b, m ≤ q x
hplower :
∀ x ∈ Icc a b, m ≤ p x
sign :
ℝ
hsign :
sign = 1 ∨ sign = -1
hfixed :
∀ x ∈ Icc a b, margin ≤ sign * derivWithin (logRatio q p) (Icc a b) x
conclusion
∃ ε > 0,
∀ q' p' : ℝ → ℝ,
DifferentiableOn ℝ q' (Icc a b) → DifferentiableOn ℝ p' (Icc a b) → C1CloseOn (Icc a b) ε q' q → C1CloseOn (Icc a b) ε p' p → (∀ x ∈ Icc a b, 0 < q' x ∧ 0 < p' x ∧ 0 < sign * derivWithin (logRatio q' p') (Icc a b) x)
Proof (Lean source)
theorem logRatioDerivative_fixedSign_open_C1 {a b m margin : ℝ}
(hab : a < b) (hm : 0 < m) (hmargin : 0 < margin)
{q p : ℝ → ℝ} (hq : ContDiffOn ℝ 1 q (Icc a b))
(hp : ContDiffOn ℝ 1 p (Icc a b))
(hqlower : ∀ x ∈ Icc a b, m ≤ q x)
(hplower : ∀ x ∈ Icc a b, m ≤ p x)
(sign : ℝ) (hsign : sign = 1 ∨ sign = -1)
(hfixed : ∀ x ∈ Icc a b,
margin ≤ sign * derivWithin (logRatio q p) (Icc a b) x) :
∃ ε > 0, ∀ q' p' : ℝ → ℝ,
DifferentiableOn ℝ q' (Icc a b) →
DifferentiableOn ℝ p' (Icc a b) →
C1CloseOn (Icc a b) ε q' q → C1CloseOn (Icc a b) ε p' p →
(∀ x ∈ Icc a b, 0 < q' x ∧ 0 < p' x ∧
0 < sign * derivWithin (logRatio q' p') (Icc a b) x) := by
have hunique := uniqueDiffOn_Icc hab
have hqderiv_cont : ContinuousOn (fun x ↦ derivWithin q (Icc a b) x) (Icc a b) :=
hq.continuousOn_derivWithin hunique (by norm_num)
have hpderiv_cont : ContinuousOn (fun x ↦ derivWithin p (Icc a b) x) (Icc a b) :=
hp.continuousOn_derivWithin hunique (by norm_num)
obtain ⟨Cq, hCq⟩ := isCompact_Icc.exists_bound_of_continuousOn hq.continuousOn
obtain ⟨Cp, hCp⟩ := isCompact_Icc.exists_bound_of_continuousOn hp.continuousOn
obtain ⟨Dq, hDq⟩ := isCompact_Icc.exists_bound_of_continuousOn hqderiv_cont
obtain ⟨Dp, hDp⟩ := isCompact_Icc.exists_bound_of_continuousOn hpderiv_cont
let B := |Cq| + |Cp| + |Dq| + |Dp| + 1
have hB : 0 < B := by dsimp [B]; positivity
have hqB : ∀ x ∈ Icc a b, |q x| ≤ B := by
intro x hx
calc
|q x| ≤ Cq := hCq x hx
_ ≤ |Cq| := le_abs_self Cq
_ ≤ B := by
dsimp [B]
linarith [abs_nonneg Cp, abs_nonneg Dq, abs_nonneg Dp]
have hpB : ∀ x ∈ Icc a b, |p x| ≤ B := by
intro x hx
calc
|p x| ≤ Cp := hCp x hx
_ ≤ |Cp| := le_abs_self Cp
_ ≤ B := by
dsimp [B]
linarith [abs_nonneg Cq, abs_nonneg Dq, abs_nonneg Dp]
have hDqB : ∀ x ∈ Icc a b, |derivWithin q (Icc a b) x| ≤ B := by
intro x hx
calc
|derivWithin q (Icc a b) x| ≤ Dq := hDq x hx
_ ≤ |Dq| := le_abs_self Dq
_ ≤ B := by
dsimp [B]
linarith [abs_nonneg Cq, abs_nonneg Cp, abs_nonneg Dp]
have hDpB : ∀ x ∈ Icc a b, |derivWithin p (Icc a b) x| ≤ B := by
intro x hx
calc
|derivWithin p (Icc a b) x| ≤ Dp := hDp x hx
_ ≤ |Dp| := le_abs_self Dp
_ ≤ B := by
dsimp [B]
linarith [abs_nonneg Cq, abs_nonneg Cp, abs_nonneg Dq]
let L := (2 * B) / (m ^ 2 / 2)
have hL : 0 < L := by dsimp [L]; positivity
let ε := min (m / 2) (margin / (4 * L))
have hε : 0 < ε := by dsimp [ε]; positivity
have hεm : ε ≤ m / 2 := min_le_left _ _
have hεmargin : 2 * L * ε ≤ margin / 2 := by
have hεL : ε ≤ margin / (4 * L) := min_le_right _ _
have hL4 : 0 < 4 * L := by positivity
calc
2 * L * ε ≤ 2 * L * (margin / (4 * L)) := by gcongr
_ = margin / 2 := by field_simp; ring
refine ⟨ε, hε, ?_⟩
intro q' p' hq'diff hp'diff hqclose hpclose x hx
have hqpos : 0 < q x := hm.trans_le (hqlower x hx)
have hppos : 0 < p x := hm.trans_le (hplower x hx)
have hq'pos : 0 < q' x := by
have hneg := neg_lt_of_abs_lt (hqclose.1 x hx)
linarith [hqlower x hx, hεm, hm]
have hp'pos : 0 < p' x := by
have hneg := neg_lt_of_abs_lt (hpclose.1 x hx)
linarith [hplower x hx, hεm, hm]
refine ⟨hq'pos, hp'pos, ?_⟩
have hqfrac := abs_div_sub_div_lt hm hB hε hεm (hqlower x hx) (hqB x hx)
(hDqB x hx) (hqclose.1 x hx) (hqclose.2 x hx)
have hpfrac := abs_div_sub_div_lt hm hB hε hεm (hplower x hx) (hpB x hx)
(hDpB x hx) (hpclose.1 x hx) (hpclose.2 x hx)
have hqfrac' :
|derivWithin q' (Icc a b) x / q' x - derivWithin q (Icc a b) x / q x| < L * ε := by
convert hqfrac using 1 <;> dsimp [L] <;> ring
have hpfrac' :
|derivWithin p' (Icc a b) x / p' x - derivWithin p (Icc a b) x / p x| < L * ε := by
convert hpfrac using 1 <;> dsimp [L] <;> ring
have hderivdiff :
|derivWithin (logRatio q' p') (Icc a b) x -
derivWithin (logRatio q p) (Icc a b) x| < 2 * L * ε := by
rw [derivWithin_logRatio hab hq'diff hp'diff (fun y hy ↦ by
have hneg := neg_lt_of_abs_lt (hqclose.1 y hy)
nlinarith [hqlower y hy]) (fun y hy ↦ by
have hneg := neg_lt_of_abs_lt (hpclose.1 y hy)
nlinarith [hplower y hy]) hx,
derivWithin_logRatio hab (hq.differentiableOn (by norm_num))
(hp.differentiableOn (by norm_num))
(fun y hy ↦ hm.trans_le (hqlower y hy))
(fun y hy ↦ hm.trans_le (hplower y hy)) hx]
calc
|(derivWithin q' (Icc a b) x / q' x - derivWithin p' (Icc a b) x / p' x) -
(derivWithin q (Icc a b) x / q x - derivWithin p (Icc a b) x / p x)| =
|(derivWithin q' (Icc a b) x / q' x - derivWithin q (Icc a b) x / q x) -
(derivWithin p' (Icc a b) x / p' x - derivWithin p (Icc a b) x / p x)| := by
congr 1 <;> ring
_ ≤ |derivWithin q' (Icc a b) x / q' x - derivWithin q (Icc a b) x / q x| +
|derivWithin p' (Icc a b) x / p' x - derivWithin p (Icc a b) x / p x| := by
simpa only [sub_eq_add_neg, Real.norm_eq_abs, norm_neg] using
norm_add_le
(derivWithin q' (Icc a b) x / q' x - derivWithin q (Icc a b) x / q x)
(-(derivWithin p' (Icc a b) x / p' x - derivWithin p (Icc a b) x / p x))
_ < L * ε + L * ε := add_lt_add hqfrac' hpfrac'
_ = 2 * L * ε := by ring
have hsignabs : |sign| = 1 := by rcases hsign with rfl | rfl <;> norm_num
have hsignedDiff :
|sign * derivWithin (logRatio q' p') (Icc a b) x -
sign * derivWithin (logRatio q p) (Icc a b) x| < margin / 2 := by
rw [← mul_sub, abs_mul, hsignabs, one_mul]
exact hderivdiff.trans_le hεmargin
have hlowerSigned := hfixed x hx
have hneg := neg_lt_of_abs_lt hsignedDiff
nlinarith
6 supporting declarations (lemmas, instances)
-
uniformlyOn_inv_of_lowerBoundtheorem — Uniform convergence is preserved by reciprocals when every approximating denominator and its limit share one strictly positive lower bound.hypothesesα :m :ℝhm :0 < mhconv :UniformlyOn K f ghlower :∀ n xifx ∈ Kthenm ≤ f n xhlower_limit :∀ xifx ∈ Kthenm ≤ g xconclusionUniformlyOn K (fun n x ↦ (f n x)⁻¹) (fun x ↦ (g x)⁻¹)Proof (Lean source)
theorem uniformlyOn_inv_of_lowerBound {α : Type*} {K : Set α} {f : ℕ → α → ℝ} {g : α → ℝ} {m : ℝ} (hm : 0 < m) (hconv : UniformlyOn K f g) (hlower : ∀ n x, x ∈ K → m ≤ f n x) (hlower_limit : ∀ x, x ∈ K → m ≤ g x) : UniformlyOn K (fun n x ↦ (f n x)⁻¹) (fun x ↦ (g x)⁻¹) := by intro ε hε obtain ⟨N, hN⟩ := hconv (ε * m ^ 2) (mul_pos hε (sq_pos_of_pos hm)) refine ⟨N, fun n hn x hx ↦ ?_⟩ have hfn : 0 < f n x := hm.trans_le (hlower n x hx) have hg : 0 < g x := hm.trans_le (hlower_limit x hx) rw [inv_sub_inv hfn.ne' hg.ne', abs_div, abs_of_pos (mul_pos hfn hg)] apply (div_lt_iff₀ (mul_pos hfn hg)).2 calc |g x - f n x| = |f n x - g x| := abs_sub_comm _ _ _ < ε * m ^ 2 := hN n hn x hx _ ≤ ε * (f n x * g x) := by gcongr nlinarith [hlower n x hx, hlower_limit x hx] -
uniformlyOn_div_of_lowerBoundtheorem — Uniform convergence is preserved by quotients on a compact set when numerators converge to a continuous limit and denominators share a strictly positive lower bound.hypothesesα :hK :u :ℕ → α → ℝv :ℕ → α → ℝu₀ v₀ :α → ℝm :ℝhm :0 < mhu :UniformlyOn K u u₀hv :UniformlyOn K v v₀hu₀ :ContinuousOn u₀ Khlower :∀ n xifx ∈ Kthenm ≤ v n xhlower_limit :∀ xifx ∈ Kthenm ≤ v₀ xconclusionUniformlyOn K (fun n x ↦ u n x / v n x) (fun x ↦ u₀ x / v₀ x)Proof (Lean source)
theorem uniformlyOn_div_of_lowerBound {α : Type*} [TopologicalSpace α] {K : Set α} (hK : IsCompact K) {u : ℕ → α → ℝ} {v : ℕ → α → ℝ} {u₀ v₀ : α → ℝ} {m : ℝ} (hm : 0 < m) (hu : UniformlyOn K u u₀) (hv : UniformlyOn K v v₀) (hu₀ : ContinuousOn u₀ K) (hlower : ∀ n x, x ∈ K → m ≤ v n x) (hlower_limit : ∀ x, x ∈ K → m ≤ v₀ x) : UniformlyOn K (fun n x ↦ u n x / v n x) (fun x ↦ u₀ x / v₀ x) := by obtain ⟨C, hC⟩ := hK.exists_bound_of_continuousOn hu₀ have hinv := uniformlyOn_inv_of_lowerBound hm hv hlower hlower_limit intro ε hε let B := |C| + 1 have hB : 0 < B := add_pos_of_nonneg_of_pos (abs_nonneg C) zero_lt_one obtain ⟨Nu, hNu⟩ := hu (ε * m / 2) (by positivity) obtain ⟨Nv, hNv⟩ := hinv (ε / (2 * B)) (by positivity) refine ⟨max Nu Nv, fun n hn x hx ↦ ?_⟩ have hnu := hNu n (le_trans (le_max_left _ _) hn) x hx have hnv := hNv n (le_trans (le_max_right _ _) hn) x hx have hvpos : 0 < v n x := hm.trans_le (hlower n x hx) have hv_inv : |(v n x)⁻¹| ≤ m⁻¹ := by rw [abs_of_pos (inv_pos.mpr hvpos)] exact (inv_le_inv₀ hvpos hm).2 (hlower n x hx) have hu₀_bound : |u₀ x| < B := (hC x hx).trans_lt (lt_of_le_of_lt (le_abs_self C) (lt_add_one _)) have hfirst : |u n x - u₀ x| * |(v n x)⁻¹| < (ε * m / 2) * m⁻¹ := by calc _ < (ε * m / 2) * |(v n x)⁻¹| := mul_lt_mul_of_pos_right hnu (abs_pos.mpr (inv_ne_zero hvpos.ne')) _ ≤ (ε * m / 2) * m⁻¹ := mul_le_mul_of_nonneg_left hv_inv (by positivity) have hsecond : |u₀ x| * |(v n x)⁻¹ - (v₀ x)⁻¹| < B * (ε / (2 * B)) := by calc _ ≤ B * |(v n x)⁻¹ - (v₀ x)⁻¹| := mul_le_mul_of_nonneg_right hu₀_bound.le (abs_nonneg _) _ < B * (ε / (2 * B)) := mul_lt_mul_of_pos_left hnv hB change |u n x / v n x - u₀ x / v₀ x| < ε rw [div_eq_mul_inv, div_eq_mul_inv] calc |u n x * (v n x)⁻¹ - u₀ x * (v₀ x)⁻¹| = |(u n x - u₀ x) * (v n x)⁻¹ + u₀ x * ((v n x)⁻¹ - (v₀ x)⁻¹)| := by congr 1 ring _ ≤ |u n x - u₀ x| * |(v n x)⁻¹| + |u₀ x| * |(v n x)⁻¹ - (v₀ x)⁻¹| := by simpa only [abs_mul] using abs_add_le ((u n x - u₀ x) * (v n x)⁻¹) (u₀ x * ((v n x)⁻¹ - (v₀ x)⁻¹)) _ < (ε * m / 2) * m⁻¹ + B * (ε / (2 * B)) := add_lt_add hfirst hsecond _ = ε := by field_simp; ring -
uniformlyOn_log_of_lowerBoundtheorem — Uniform convergence is preserved by the real logarithm when all functions share a strictly positive lower bound.hypothesesα :m :ℝhm :0 < mhconv :UniformlyOn K f ghlower :∀ n xifx ∈ Kthenm ≤ f n xhlower_limit :∀ xifx ∈ Kthenm ≤ g xconclusionProof (Lean source)
theorem uniformlyOn_log_of_lowerBound {α : Type*} {K : Set α} {f : ℕ → α → ℝ} {g : α → ℝ} {m : ℝ} (hm : 0 < m) (hconv : UniformlyOn K f g) (hlower : ∀ n x, x ∈ K → m ≤ f n x) (hlower_limit : ∀ x, x ∈ K → m ≤ g x) : UniformlyOn K (fun n x ↦ log (f n x)) (fun x ↦ log (g x)) := by have hlog_lip : ∀ {r s : ℝ}, m ≤ r → m ≤ s → |log r - log s| ≤ m⁻¹ * |r - s| := by intro r s hr hs simpa only [Real.norm_eq_abs] using (Convex.norm_image_sub_le_of_norm_hasDerivWithin_le (f := log) (f' := fun y : ℝ ↦ y⁻¹) (C := m⁻¹) (fun y hy ↦ (Real.hasDerivAt_log (hm.trans_le hy).ne').hasDerivWithinAt) (fun y hy ↦ by have hypos : 0 < y := hm.trans_le hy rw [Real.norm_eq_abs, abs_of_pos (inv_pos.mpr hypos)] exact (inv_le_inv₀ hypos hm).2 hy) (convex_Ici m) hs hr) intro ε hε obtain ⟨N, hN⟩ := hconv (ε * m) (mul_pos hε hm) refine ⟨N, fun n hn x hx ↦ ?_⟩ change |log (f n x) - log (g x)| < ε calc _ ≤ m⁻¹ * |f n x - g x| := hlog_lip (hlower n x hx) (hlower_limit x hx) _ < m⁻¹ * (ε * m) := mul_lt_mul_of_pos_left (hN n hn x hx) (inv_pos.mpr hm) _ = ε := by field_simp -
derivWithin_logRatiotheorem — On a nondegenerate compact interval, the within-derivative of a positive log ratio is the difference of the two logarithmic derivatives.hypothesesa b :ℝhab :a < bq p :ℝ → ℝhq :DifferentiableOn ℝ q (Icc a b)hp :DifferentiableOn ℝ p (Icc a b)hqpos :∀ x ∈ Icc a b, 0 < q xhppos :∀ x ∈ Icc a b, 0 < p xx :ℝhx :x ∈ Icc a bconclusionderivWithin (logRatio q p) (Icc a b) x= derivWithin q (Icc a b) x / q x - derivWithin p (Icc a b) x / p xProof (Lean source)
theorem derivWithin_logRatio {a b : ℝ} (hab : a < b) {q p : ℝ → ℝ} (hq : DifferentiableOn ℝ q (Icc a b)) (hp : DifferentiableOn ℝ p (Icc a b)) (hqpos : ∀ x ∈ Icc a b, 0 < q x) (hppos : ∀ x ∈ Icc a b, 0 < p x) {x : ℝ} (hx : x ∈ Icc a b) : derivWithin (logRatio q p) (Icc a b) x = derivWithin q (Icc a b) x / q x - derivWithin p (Icc a b) x / p x := by have hq_at := hq x hx have hp_at := hp x hx have hqne : q x ≠ 0 := (hqpos x hx).ne' have hpne : p x ≠ 0 := (hppos x hx).ne' have hunique := (uniqueDiffOn_Icc hab).uniqueDiffWithinAt hx have hdiv : DifferentiableWithinAt ℝ (fun y ↦ q y / p y) (Icc a b) x := hq_at.div hp_at hpne have hdiv_deriv := derivWithin_div hq_at hp_at hpne change derivWithin (fun y ↦ q y / p y) (Icc a b) x = _ at hdiv_deriv change derivWithin (fun y ↦ log (q y / p y)) (Icc a b) x = _ rw [derivWithin.log hdiv (div_ne_zero hqne hpne) hunique] rw [hdiv_deriv] field_simp -
uniformC1On_logRatiotheorem — Positive pairs converging uniformly in C¹ to C¹ limits on a compact interval have log ratios converging uniformly in C¹, provided the whole family shares one positive lower bound.hypothesesa b m :ℝhab :a < bhm :0 < mq p :ℕ → ℝ → ℝq₀ p₀ :ℝ → ℝhqdiff :∀ n, DifferentiableOn ℝ (q n) (Icc a b)hpdiff :∀ n, DifferentiableOn ℝ (p n) (Icc a b)hq₀diff :ContDiffOn ℝ 1 q₀ (Icc a b)hp₀diff :ContDiffOn ℝ 1 p₀ (Icc a b)hqconv :UniformC1On (Icc a b) q q₀hpconv :UniformC1On (Icc a b) p p₀hqlower :∀ n xifx ∈ Icc a bthenm ≤ q n xhplower :∀ n xifx ∈ Icc a bthenm ≤ p n xhq₀lower :∀ xifx ∈ Icc a bthenm ≤ q₀ xhp₀lower :∀ xifx ∈ Icc a bthenm ≤ p₀ xconclusionProof (Lean source)
theorem uniformC1On_logRatio {a b m : ℝ} (hab : a < b) (hm : 0 < m) {q p : ℕ → ℝ → ℝ} {q₀ p₀ : ℝ → ℝ} (hqdiff : ∀ n, DifferentiableOn ℝ (q n) (Icc a b)) (hpdiff : ∀ n, DifferentiableOn ℝ (p n) (Icc a b)) (hq₀diff : ContDiffOn ℝ 1 q₀ (Icc a b)) (hp₀diff : ContDiffOn ℝ 1 p₀ (Icc a b)) (hqconv : UniformC1On (Icc a b) q q₀) (hpconv : UniformC1On (Icc a b) p p₀) (hqlower : ∀ n x, x ∈ Icc a b → m ≤ q n x) (hplower : ∀ n x, x ∈ Icc a b → m ≤ p n x) (hq₀lower : ∀ x, x ∈ Icc a b → m ≤ q₀ x) (hp₀lower : ∀ x, x ∈ Icc a b → m ≤ p₀ x) : UniformC1On (Icc a b) (fun n ↦ logRatio (q n) (p n)) (logRatio q₀ p₀) := by have hqpos : ∀ n x, x ∈ Icc a b → 0 < q n x := fun n x hx ↦ hm.trans_le (hqlower n x hx) have hppos : ∀ n x, x ∈ Icc a b → 0 < p n x := fun n x hx ↦ hm.trans_le (hplower n x hx) have hq₀pos : ∀ x, x ∈ Icc a b → 0 < q₀ x := fun x hx ↦ hm.trans_le (hq₀lower x hx) have hp₀pos : ∀ x, x ∈ Icc a b → 0 < p₀ x := fun x hx ↦ hm.trans_le (hp₀lower x hx) have hsub : ∀ {u v : ℕ → ℝ → ℝ} {u₀ v₀ : ℝ → ℝ}, UniformlyOn (Icc a b) u u₀ → UniformlyOn (Icc a b) v v₀ → UniformlyOn (Icc a b) (fun n x ↦ u n x - v n x) (fun x ↦ u₀ x - v₀ x) := by intro u v u₀ v₀ hu hv ε hε obtain ⟨Nu, hNu⟩ := hu (ε / 2) (by positivity) obtain ⟨Nv, hNv⟩ := hv (ε / 2) (by positivity) refine ⟨max Nu Nv, fun n hn x hx ↦ ?_⟩ calc |(u n x - v n x) - (u₀ x - v₀ x)| = |(u n x - u₀ x) - (v n x - v₀ x)| := by ring_nf _ ≤ |u n x - u₀ x| + |v n x - v₀ x| := by simpa only [sub_eq_add_neg, Real.norm_eq_abs, norm_neg] using norm_add_le (u n x - u₀ x) (-(v n x - v₀ x)) _ < ε / 2 + ε / 2 := add_lt_add (hNu n (le_trans (le_max_left _ _) hn) x hx) (hNv n (le_trans (le_max_right _ _) hn) x hx) _ = ε := by ring have hqlog := uniformlyOn_log_of_lowerBound hm hqconv.1 hqlower hq₀lower have hplog := uniformlyOn_log_of_lowerBound hm hpconv.1 hplower hp₀lower have hvalue := hsub hqlog hplog have hqderiv_cont : ContinuousOn (fun x ↦ derivWithin q₀ (Icc a b) x) (Icc a b) := hq₀diff.continuousOn_derivWithin (uniqueDiffOn_Icc hab) (by norm_num) have hpderiv_cont : ContinuousOn (fun x ↦ derivWithin p₀ (Icc a b) x) (Icc a b) := hp₀diff.continuousOn_derivWithin (uniqueDiffOn_Icc hab) (by norm_num) have hqquot := uniformlyOn_div_of_lowerBound isCompact_Icc hm hqconv.2 hqconv.1 hqderiv_cont hqlower hq₀lower have hpquot := uniformlyOn_div_of_lowerBound isCompact_Icc hm hpconv.2 hpconv.1 hpderiv_cont hplower hp₀lower refine ⟨?_, ?_⟩ · intro ε hε obtain ⟨N, hN⟩ := hvalue ε hε refine ⟨N, fun n hn x hx ↦ ?_⟩ change |log (q n x / p n x) - log (q₀ x / p₀ x)| < ε rw [Real.log_div (hqpos n x hx).ne' (hppos n x hx).ne', Real.log_div (hq₀pos x hx).ne' (hp₀pos x hx).ne'] exact hN n hn x hx · intro ε hε obtain ⟨N, hN⟩ := hsub hqquot hpquot ε hε refine ⟨N, fun n hn x hx ↦ ?_⟩ change |derivWithin (logRatio (q n) (p n)) (Icc a b) x - derivWithin (logRatio q₀ p₀) (Icc a b) x| < ε rw [derivWithin_logRatio hab (hqdiff n) (hpdiff n) (hqpos n) (hppos n) hx, derivWithin_logRatio hab (hq₀diff.differentiableOn (by norm_num)) (hp₀diff.differentiableOn (by norm_num)) hq₀pos hp₀pos hx] exact hN n hn x hx -
logRatioDerivative_fixedSign_open_C2theorem — The same strict fixed-sign derivative property is open under uniform C² perturbations, because uniform C² control includes the required uniform C¹ control.hypothesesa b m margin :ℝhab :a < bhm :0 < mhmargin :0 < marginq p :ℝ → ℝhq :ContDiffOn ℝ 1 q (Icc a b)hp :ContDiffOn ℝ 1 p (Icc a b)hqlower :∀ x ∈ Icc a b, m ≤ q xhplower :∀ x ∈ Icc a b, m ≤ p xsign :ℝhsign :sign = 1 ∨ sign = -1hfixed :∀ x ∈ Icc a b, margin ≤ sign * derivWithin (logRatio q p) (Icc a b) xconclusion∃ ε > 0,∀ q' p' : ℝ → ℝ,DifferentiableOn ℝ q' (Icc a b) → DifferentiableOn ℝ p' (Icc a b) → C2CloseOn (Icc a b) ε q' q → C2CloseOn (Icc a b) ε p' p → (∀ x ∈ Icc a b, 0 < q' x ∧ 0 < p' x ∧ 0 < sign * derivWithin (logRatio q' p') (Icc a b) x)Proof (Lean source)
theorem logRatioDerivative_fixedSign_open_C2 {a b m margin : ℝ} (hab : a < b) (hm : 0 < m) (hmargin : 0 < margin) {q p : ℝ → ℝ} (hq : ContDiffOn ℝ 1 q (Icc a b)) (hp : ContDiffOn ℝ 1 p (Icc a b)) (hqlower : ∀ x ∈ Icc a b, m ≤ q x) (hplower : ∀ x ∈ Icc a b, m ≤ p x) (sign : ℝ) (hsign : sign = 1 ∨ sign = -1) (hfixed : ∀ x ∈ Icc a b, margin ≤ sign * derivWithin (logRatio q p) (Icc a b) x) : ∃ ε > 0, ∀ q' p' : ℝ → ℝ, DifferentiableOn ℝ q' (Icc a b) → DifferentiableOn ℝ p' (Icc a b) → C2CloseOn (Icc a b) ε q' q → C2CloseOn (Icc a b) ε p' p → (∀ x ∈ Icc a b, 0 < q' x ∧ 0 < p' x ∧ 0 < sign * derivWithin (logRatio q' p') (Icc a b) x) := by obtain ⟨ε, hε, hopen⟩ := logRatioDerivative_fixedSign_open_C1 hab hm hmargin hq hp hqlower hplower sign hsign hfixed refine ⟨ε, hε, ?_⟩ intro q' p' hq'diff hp'diff hqclose hpclose exact hopen q' p' hq'diff hp'diff hqclose.1 hpclose.1
MonomialGram 4 core · 8 supporting This module proves that distinct multivariate monomials have a positive-definite Gram matrix on every nondegenerate real cube. ★ monomialGram_posDef
Multivariate monomial Gram matrices
This module proves that distinct multivariate monomials have a positive-definite Gram matrix on every nondegenerate real cube. It also supplies the resulting uniform quadratic coercivity bound.
def supBall reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a coordinate index set, a real-valued center vector, and a real radius, the closed sup-norm ball is the set of real-valued vectors whose every coordinate differs from the corresponding coordinate of the center by at most that radius.
Definition (Lean source)
parameters
ι :
Type*
x0 :
ι → ℝ
r :
ℝ
def
given by
{x | ∀ i, |x i - x0 i| ≤ r}
def monomial reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a finite coordinate index set, an assignment of a nonnegative integer exponent to each coordinate, and a real-valued coordinate vector, the multivariate monomial is the product of the coordinates after each has been raised to its assigned exponent.
Definition (Lean source)
def monomialGram reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a coordinate dimension and a finite family size, an assignment of a multivariate exponent vector to each member of that family, and a real radius, the monomial Gram matrix has as its entry the integral of the product of the th and th associated monomials over the centered closed coordinate cube of that radius.
theorem monomialGram_posDef reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Positive-definiteness of the monomial Gram matrix. For a finite family of multivariate monomials indexed by their exponent vectors, if the cube radius r is strictly positive and the exponent vectors are pairwise distinct, then the Gram matrix of pairwise integrals of the monomials over the cube of radius r is positive-definite.
Formal statement
hypotheses
conclusion
(monomialGram expo r).PosDef
Proof (Lean source)
theorem monomialGram_posDef {d p : ℕ} (expo : Fin p → (Fin d → ℕ)) {r : ℝ}
(hr : 0 < r) (hexpo : Injective expo) :
(monomialGram expo r).PosDef := by
apply Matrix.PosDef.of_dotProduct_mulVec_pos (monomialGram_isHermitian expo r)
intro z hz
rw [show star z = z by ext k; simp]
simp only [dotProduct, mulVec, Finset.mul_sum]
simp_rw [← mul_assoc]
rw [monomialGram_quadForm expo z]
let f : (Fin d → ℝ) → ℝ := fun u => ∑ k, z k * monomial (expo k) u
have hfcont : Continuous f := continuous_monomialCombination expo z
have hfint : IntegrableOn (fun u => (f u) ^ 2) (cube d r) :=
(hfcont.pow 2).continuousOn.integrableOn_compact (isCompact_cube d r)
have hnonneg : 0 ≤ ∫ u in cube d r, (f u) ^ 2 :=
MeasureTheory.integral_nonneg_of_ae
(Filter.Eventually.of_forall fun _ => sq_nonneg _)
by_contra hpos
have hintzero : (∫ u in cube d r, (f u) ^ 2) = 0 :=
le_antisymm (le_of_not_gt hpos) hnonneg
have hae_sq : (fun u => (f u) ^ 2) =ᵐ[volume.restrict (cube d r)] 0 :=
(MeasureTheory.setIntegral_eq_zero_iff_of_nonneg_ae
(Filter.Eventually.of_forall fun _ => sq_nonneg _) hfint).mp hintzero
have hae_f : f =ᵐ[volume.restrict (cube d r)] 0 :=
hae_sq.mono fun u hu => by simpa using (sq_eq_zero_iff.mp hu)
let U : Set (Fin d → ℝ) := pi univ (fun _ => Ioo (-r) r)
have hUopen : IsOpen U :=
isOpen_set_pi Set.finite_univ (fun _ _ => isOpen_Ioo)
have hUcube : U ⊆ cube d r := by
intro u hu j
rw [abs_le]
exact ⟨(hu j (Set.mem_univ j)).1.le, (hu j (Set.mem_univ j)).2.le⟩
have hae_U : f =ᵐ[volume.restrict U] 0 :=
ae_restrict_of_ae_restrict_of_subset hUcube hae_f
have hpoint : EqOn f 0 U :=
MeasureTheory.Measure.eqOn_open_of_ae_eq hae_U hUopen hfcont.continuousOn
continuous_zero.continuousOn
apply hz
apply monomial_coefficients_eq_zero_of_vanishes_on_openCube hr hexpo z
intro u hu
exact hpoint (fun j _ => hu j)
8 supporting declarations (lemmas, instances)
-
continuous_monomiallemma — A multivariate real monomial varies continuously with its coordinate vector.Proof (Lean source)
@[fun_prop] lemma continuous_monomial {ι : Type*} [Fintype ι] (e : ι → ℕ) : Continuous (monomial e) := by unfold monomial exact continuous_finset_prod _ fun j _ => (continuous_apply j).pow (e j) -
continuous_monomialCombinationlemma — A finite linear combination of multivariate real monomials is continuous.hypothesesconclusionContinuous (fun u => ∑ k, z k * monomial (expo k) u)Proof (Lean source)
@[fun_prop] lemma continuous_monomialCombination {d p : ℕ} (expo : Fin p → (Fin d → ℕ)) (z : Fin p → ℝ) : Continuous (fun u => ∑ k, z k * monomial (expo k) u) := by exact continuous_finset_sum _ fun k _ => continuous_const.mul (continuous_monomial (expo k)) -
monomial_linearIndependent_on_cubetheorem — A linear combination of distinct multivariate monomials that vanishes throughout the interior of a cube with positive radius must have every coefficient equal to zero.Proof (Lean source)
theorem monomial_linearIndependent_on_cube {d p : ℕ} {expo : Fin p → (Fin d → ℕ)} {r : ℝ} (hr : 0 < r) (hexpo : Injective expo) (z : Fin p → ℝ) (hz : ∀ u, (∀ j, u j ∈ Ioo (-r) r) → (∑ k, z k * monomial (expo k) u) = 0) : z = 0 := by exact monomial_coefficients_eq_zero_of_vanishes_on_openCube hr hexpo z hz -
monomialGram_quadFormtheorem — Evaluating the monomial Gram quadratic form at a coefficient vector equals integrating the square of the corresponding monomial combination over the cube.hypothesesconclusion∑ k, ∑ l, z k * monomialGram expo r k l * z lProof (Lean source)
theorem monomialGram_quadForm {d p : ℕ} (expo : Fin p → (Fin d → ℕ)) {r : ℝ} (z : Fin p → ℝ) : ∑ k, ∑ l, z k * monomialGram expo r k l * z l = ∫ u in {u : Fin d → ℝ | ∀ j, |u j| ≤ r}, (∑ k, z k * monomial (expo k) u) ^ 2 := by change (∑ k, ∑ l, z k * (∫ u in cube d r, monomial (expo k) u * monomial (expo l) u) * z l) = _ have hkl (k l : Fin p) : IntegrableOn (fun u => (z k * monomial (expo k) u) * (z l * monomial (expo l) u)) (cube d r) := (((continuous_const.mul (continuous_monomial (expo k))).mul (continuous_const.mul (continuous_monomial (expo l)))).continuousOn.integrableOn_compact (isCompact_cube d r)) calc _ = ∑ k, ∑ l, ∫ u in cube d r, (z k * monomial (expo k) u) * (z l * monomial (expo l) u) := by apply Finset.sum_congr rfl intro k _ apply Finset.sum_congr rfl intro l _ rw [show (fun u => (z k * monomial (expo k) u) * (z l * monomial (expo l) u)) = fun u => (z k * z l) * (monomial (expo k) u * monomial (expo l) u) by funext u ring, MeasureTheory.integral_const_mul] ring _ = ∫ u in cube d r, ∑ k, ∑ l, (z k * monomial (expo k) u) * (z l * monomial (expo l) u) := by symm rw [MeasureTheory.integral_finset_sum univ (fun k _ => integrable_finset_sum _ fun l _ => hkl k l)] apply Finset.sum_congr rfl intro k _ rw [MeasureTheory.integral_finset_sum univ (fun l _ => hkl k l)] _ = ∫ u in cube d r, (∑ k, z k * monomial (expo k) u) ^ 2 := by congr 1 funext u rw [pow_two, Finset.sum_mul_sum] -
monomialGram_isHermitiantheorem — The monomial Gram matrix is symmetric, and hence Hermitian over the real numbers.Proof (Lean source)
theorem monomialGram_isHermitian {d p : ℕ} (expo : Fin p → (Fin d → ℕ)) (r : ℝ) : (monomialGram expo r).IsHermitian := by apply Matrix.IsHermitian.ext intro k l simp only [star_id_of_comm] simp [monomialGram, mul_comm] -
monomialGram_posSemideftheorem — Every coefficient vector gives a nonnegative quadratic form under the monomial Gram matrix.Proof (Lean source)
theorem monomialGram_posSemidef {d p : ℕ} (expo : Fin p → (Fin d → ℕ)) {r : ℝ} : (monomialGram expo r).PosSemidef := by apply Matrix.PosSemidef.of_dotProduct_mulVec_nonneg (monomialGram_isHermitian expo r) intro z rw [show star z = z by ext k; simp] simp only [dotProduct, mulVec, Finset.mul_sum] simp_rw [← mul_assoc] rw [monomialGram_quadForm expo z] exact MeasureTheory.integral_nonneg_of_ae (Filter.Eventually.of_forall fun _ => sq_nonneg _) -
sum_sq_poslemma — The sum of squared coordinates of a nonzero finite real-valued vector is strictly positive.Proof (Lean source)
lemma sum_sq_pos {ι : Type*} [Fintype ι] (z : ι → ℝ) (hz : z ≠ 0) : 0 < ∑ k, (z k) ^ 2 := by have hnonneg : 0 ≤ ∑ k, (z k) ^ 2 := sum_nonneg fun _ _ => sq_nonneg _ refine lt_of_le_of_ne hnonneg ?_ intro heq apply hz funext k have hk : (z k) ^ 2 = 0 := (Finset.sum_eq_zero_iff_of_nonneg (fun _ _ => sq_nonneg _)).mp heq.symm k (Finset.mem_univ k) exact sq_eq_zero_iff.mp hk -
exists_monomialGram_coercivetheorem — A fixed family of distinct monomials on a cube with positive radius admits a positive uniform lower bound: its Gram quadratic form dominates the squared Euclidean norm of the coefficients.hypothesesconclusion∃ cmin : ℝ,0 < cminProof (Lean source)
theorem exists_monomialGram_coercive {d p : ℕ} (expo : Fin p → (Fin d → ℕ)) {r : ℝ} (hr : 0 < r) (hexpo : Injective expo) : ∃ cmin : ℝ, 0 < cmin ∧ ∀ z : Fin p → ℝ, cmin * (∑ k, (z k) ^ 2) ≤ ∑ k, ∑ l, z k * monomialGram expo r k l * z l := by by_cases hp : p = 0 · subst p refine ⟨1, one_pos, ?_⟩ intro z simp have hp0 : 0 < p := Nat.pos_of_ne_zero hp let q : (Fin p → ℝ) → ℝ := fun z => ∑ k, ∑ l, z k * monomialGram expo r k l * z l let s2 : (Fin p → ℝ) → ℝ := fun z => ∑ k, (z k) ^ 2 let S : Set (Fin p → ℝ) := {z | s2 z = 1} have hqcont : Continuous q := by dsimp [q] fun_prop have hs2cont : Continuous s2 := by dsimp [s2] fun_prop have hSclosed : IsClosed S := by exact isClosed_eq hs2cont continuous_const have hSbounded : Bornology.IsBounded S := by apply (Metric.isBounded_iff_subset_closedBall 0).mpr refine ⟨1, ?_⟩ intro z hz rw [Metric.mem_closedBall, dist_zero_right] apply (pi_norm_le_iff_of_nonneg zero_le_one).mpr intro k rw [Real.norm_eq_abs, ← sq_le_one_iff_abs_le_one] have hk : (z k) ^ 2 ≤ 1 := by rw [← hz] exact Finset.single_le_sum (fun i _ => sq_nonneg (z i)) (Finset.mem_univ k) exact hk have hScompact : IsCompact S := Metric.isCompact_iff_isClosed_bounded.mpr ⟨hSclosed, hSbounded⟩ let e : Fin p := ⟨0, hp0⟩ let zunit : Fin p → ℝ := single e 1 have hzunit : zunit ∈ S := by classical simp [S, s2, zunit, Pi.single_apply] obtain ⟨zmin, hzmin, hmin⟩ := hScompact.exists_isMinOn ⟨zunit, hzunit⟩ hqcont.continuousOn have hPD := monomialGram_posDef expo hr hexpo have hzmin_ne : zmin ≠ 0 := by intro hzero simp [S, s2, hzero] at hzmin have hqmin_pos : 0 < q zmin := by have h := hPD.dotProduct_mulVec_pos hzmin_ne rw [show star zmin = zmin by ext k; simp] at h simpa only [q, dotProduct, mulVec, Finset.mul_sum, ← mul_assoc] using h refine ⟨q zmin, hqmin_pos, ?_⟩ intro z by_cases hz : z = 0 · simp [hz, q] have hspos : 0 < s2 z := by exact sum_sq_pos z hz let a : ℝ := (sqrt (s2 z))⁻¹ let w : Fin p → ℝ := a • z have hsqrt : (sqrt (s2 z)) ^ 2 = s2 z := by exact (Real.sq_sqrt hspos.le) have hsqrt_ne : sqrt (s2 z) ≠ 0 := (Real.sqrt_pos.2 hspos).ne' have hwS : w ∈ S := by simp only [S, Set.mem_setOf_eq, s2, w, Pi.smul_apply, smul_eq_mul] calc ∑ k, (a * z k) ^ 2 = a ^ 2 * ∑ k, (z k) ^ 2 := by simp_rw [mul_pow, Finset.mul_sum] _ = 1 := by dsimp [a] rw [inv_pow, hsqrt] exact inv_mul_cancel₀ hspos.ne' have hscale : q w = a ^ 2 * q z := by dsimp [q, w] symm rw [Finset.mul_sum] apply Finset.sum_congr rfl intro k _ rw [Finset.mul_sum] apply Finset.sum_congr rfl intro l _ ring have hlower : q zmin ≤ q w := hmin hwS rw [hscale] at hlower change q zmin * s2 z ≤ q z calc q zmin * s2 z ≤ (a ^ 2 * q z) * s2 z := mul_le_mul_of_nonneg_right hlower hspos.le _ = q z := by dsimp [a] rw [inv_pow, hsqrt] field_simp
OffsetPeeling 3 core · 6 supporting This file gives deterministic Young/weighted-AM-GM bounds that control expressions of the form a·t^θ after subtracting a linear offset in t. ★ offset_peeling
Offset peeling inequalities
This file gives deterministic Young/weighted-AM-GM bounds that control
expressions of the form a·t^θ after subtracting a linear offset in t.
It provides the quarter-offset constant offsetPeelingConstant, its general
coefficient version offsetPeelingConstantC, the corresponding peeling bounds
offset_peeling and offset_peeling_coeff, endpoint extensions at θ = 0,
and max_two_split for splitting a clipped two-term offset across summands.
def offsetPeelingConstant reviewed
⚑ flagged
Causalean.Mathlib.OffsetPeeling
Given a real number , the quarter-offset peeling constant is .
Definition (Lean source)
parameters
θ :
ℝ
def
offsetPeelingConstant θ :
ℝ
given by
(1 - θ) * (4 * θ) ^ (θ / (1 - θ))
def offsetPeelingConstantC reviewed
⚑ flagged
Causalean.Mathlib.OffsetPeeling
Given a real offset coefficient and a real number , the general-offset peeling constant is \((1-\theta)(\theta/c)^{\theta/(1-\theta)}).
Definition (Lean source)
parameters
c θ :
ℝ
def
offsetPeelingConstantC c θ :
ℝ
given by
(1 - θ) * (θ / c) ^ (θ / (1 - θ))
lemma offset_peeling reviewed
⚑ flagged
Causalean.Mathlib.OffsetPeeling
Deterministic Young/AM-GM peeling for the quarter-offset. For an exponent strictly between zero and one and nonnegative coefficients a and t, the positive part of a·t^θ − t/4 is at most the offset-peeling constant times a raised to the power 1/(1−θ).
Formal statement
hypotheses
θ a t :
ℝ
hθ_pos :
0 < θ
hθ_lt :
θ < 1
ha :
0 ≤ a
ht :
0 ≤ t
conclusion
max 0 (a * t ^ θ - (1 / 4 : ℝ) * t) ≤ offsetPeelingConstant θ * a ^ (1 / (1 - θ))
Proof (Lean source)
lemma offset_peeling
(θ a t : ℝ) (hθ_pos : 0 < θ) (hθ_lt : θ < 1)
(ha : 0 ≤ a) (ht : 0 ≤ t) :
max 0 (a * t ^ θ - (1 / 4 : ℝ) * t)
≤ offsetPeelingConstant θ * a ^ (1 / (1 - θ)) := by
simpa [offsetPeelingConstant, offsetPeelingConstantC, div_eq_mul_inv, mul_comm] using
offset_peeling_coeff (1 / 4) θ a t (by norm_num) hθ_pos hθ_lt ha ht
6 supporting declarations (lemmas, instances)
-
offset_peeling_coefflemma — Generalized offset peeling at coefficient c: for 0 < c, 0 < θ < 1, max 0 (a·t^θ − c·t) ≤ offsetPeelingConstantC c θ · a^{1/(1−θ)} (weighted AM-GM).hypothesesc θ a t :ℝhc_pos :0 < chθ_pos :0 < θhθ_lt :θ < 1ha :0 ≤ aht :0 ≤ tconclusionmax 0 (a * t ^ θ - c * t) ≤ offsetPeelingConstantC c θ * a ^ (1 / (1 - θ))Proof (Lean source)
lemma offset_peeling_coeff (c θ a t : ℝ) (hc_pos : 0 < c) (hθ_pos : 0 < θ) (hθ_lt : θ < 1) (ha : 0 ≤ a) (ht : 0 ≤ t) : max 0 (a * t ^ θ - c * t) ≤ offsetPeelingConstantC c θ * a ^ (1 / (1 - θ)) := by have hθ_nonneg : 0 ≤ θ := le_of_lt hθ_pos have hone_sub_nonneg : 0 ≤ 1 - θ := sub_nonneg.mpr (le_of_lt hθ_lt) have hone_sub_pos : 0 < 1 - θ := sub_pos.mpr hθ_lt have hθc_pos : 0 < θ / c := div_pos hθ_pos hc_pos have hθc_nonneg : 0 ≤ θ / c := le_of_lt hθc_pos let p₁ : ℝ := c * t / θ let p₂ : ℝ := (θ / c) ^ (θ / (1 - θ)) * a ^ (1 / (1 - θ)) have hp₁ : 0 ≤ p₁ := div_nonneg (mul_nonneg (le_of_lt hc_pos) ht) hθ_nonneg have hp₂ : 0 ≤ p₂ := mul_nonneg (Real.rpow_nonneg hθc_nonneg _) (Real.rpow_nonneg ha _) have hw : θ + (1 - θ) = 1 := by ring have hamg := Real.geom_mean_le_arith_mean2_weighted hθ_nonneg hone_sub_nonneg hp₁ hp₂ hw have hrhs : θ * p₁ + (1 - θ) * p₂ = c * t + offsetPeelingConstantC c θ * a ^ (1 / (1 - θ)) := by dsimp [p₁, p₂, offsetPeelingConstantC] field_simp [ne_of_gt hθ_pos, ne_of_gt hone_sub_pos, ne_of_gt hc_pos] have hlhs : p₁ ^ θ * p₂ ^ (1 - θ) = a * t ^ θ := by dsimp [p₁, p₂] rw [Real.mul_rpow (Real.rpow_nonneg hθc_nonneg _) (Real.rpow_nonneg ha _)] rw [← Real.rpow_mul hθc_nonneg] rw [← Real.rpow_mul ha] have hpow₁ : θ / (1 - θ) * (1 - θ) = θ := by field_simp [ne_of_gt hone_sub_pos] have hpow₂ : 1 / (1 - θ) * (1 - θ) = 1 := by field_simp [ne_of_gt hone_sub_pos] rw [hpow₁, hpow₂, Real.rpow_one] rw [← mul_assoc] rw [← Real.mul_rpow hp₁ hθc_nonneg] have hdiv : c * t / θ * (θ / c) = t := by field_simp [ne_of_gt hθ_pos, ne_of_gt hc_pos] rw [hdiv] ring have hmain : a * t ^ θ ≤ c * t + offsetPeelingConstantC c θ * a ^ (1 / (1 - θ)) := by rw [← hlhs] simpa [hrhs] using hamg have hR_nonneg : 0 ≤ offsetPeelingConstantC c θ * a ^ (1 / (1 - θ)) := by dsimp [offsetPeelingConstantC] exact mul_nonneg (mul_nonneg hone_sub_nonneg (Real.rpow_nonneg hθc_nonneg _)) (Real.rpow_nonneg ha _) exact max_le (by simpa using hR_nonneg) (by linarith) -
offsetPeelingConstantC_nonneglemma — The general offset-peeling constant is nonnegative when the offset is positive and the exponent lies between zero and one.hypothesesc θ :ℝhc_nonneg :0 ≤ chθ_nonneg :0 ≤ θhθ_le :θ ≤ 1conclusion0 ≤ offsetPeelingConstantC c θProof (Lean source)
lemma offsetPeelingConstantC_nonneg (c θ : ℝ) (hc_nonneg : 0 ≤ c) (hθ_nonneg : 0 ≤ θ) (hθ_le : θ ≤ 1) : 0 ≤ offsetPeelingConstantC c θ := by have hsub : 0 ≤ 1 - θ := sub_nonneg.mpr hθ_le have hbase : 0 ≤ θ / c := div_nonneg hθ_nonneg hc_nonneg unfold offsetPeelingConstantC exact mul_nonneg hsub (Real.rpow_nonneg hbase _) -
offset_peeling_coeff_nonneg_thetalemma — The general offset-peeling bound remains valid at exponent zero by the same constant formula.hypothesesc θ a t :ℝhc_pos :0 < chθ_nonneg :0 ≤ θhθ_lt :θ < 1ha :0 ≤ aht :0 ≤ tconclusionmax 0 (a * t ^ θ - c * t) ≤ offsetPeelingConstantC c θ * a ^ (1 / (1 - θ))Proof (Lean source)
lemma offset_peeling_coeff_nonneg_theta (c θ a t : ℝ) (hc_pos : 0 < c) (hθ_nonneg : 0 ≤ θ) (hθ_lt : θ < 1) (ha : 0 ≤ a) (ht : 0 ≤ t) : max 0 (a * t ^ θ - c * t) ≤ offsetPeelingConstantC c θ * a ^ (1 / (1 - θ)) := by by_cases hθ_zero : θ = 0 · subst θ have hconst : offsetPeelingConstantC c 0 = 1 := by unfold offsetPeelingConstantC simp have hsub : a * t ^ (0 : ℝ) - c * t ≤ a := by rw [Real.rpow_zero] nlinarith [mul_nonneg (le_of_lt hc_pos) ht] simpa [hconst] using max_le ha hsub · exact offset_peeling_coeff c θ a t hc_pos (lt_of_le_of_ne hθ_nonneg (Ne.symm hθ_zero)) hθ_lt ha ht -
offsetPeelingConstant_nonneglemma — The offset-peeling constant for the quarter-offset case is nonnegative when the exponent lies between zero and one.Proof (Lean source)
lemma offsetPeelingConstant_nonneg (θ : ℝ) (hθ_nonneg : 0 ≤ θ) (hθ_le : θ ≤ 1) : 0 ≤ offsetPeelingConstant θ := by simpa [offsetPeelingConstant, offsetPeelingConstantC, div_eq_mul_inv, mul_comm] using offsetPeelingConstantC_nonneg (1 / 4) θ (by norm_num) hθ_nonneg hθ_le -
offset_peeling_nonneg_thetalemma — The quarter-offset peeling bound remains valid at exponent zero by continuity of the constant formula.hypothesesθ a t :ℝhθ_nonneg :0 ≤ θhθ_lt :θ < 1ha :0 ≤ aht :0 ≤ tconclusionmax 0 (a * t ^ θ - (1 / 4 : ℝ) * t) ≤ offsetPeelingConstant θ * a ^ (1 / (1 - θ))Proof (Lean source)
lemma offset_peeling_nonneg_theta (θ a t : ℝ) (hθ_nonneg : 0 ≤ θ) (hθ_lt : θ < 1) (ha : 0 ≤ a) (ht : 0 ≤ t) : max 0 (a * t ^ θ - (1 / 4 : ℝ) * t) ≤ offsetPeelingConstant θ * a ^ (1 / (1 - θ)) := by simpa [offsetPeelingConstant, offsetPeelingConstantC, div_eq_mul_inv, mul_comm] using offset_peeling_coeff_nonneg_theta (1 / 4) θ a t (by norm_num) hθ_nonneg hθ_lt ha ht -
max_two_splitlemma — Split a clipped two-term offset across its summands: max 0 (a − 2r) ≤ max 0 (b − r) + max 0 (c − r) when a ≤ b + c.Proof (Lean source)
lemma max_two_split (a b c r : ℝ) (h : a ≤ b + c) : max 0 (a - 2 * r) ≤ max 0 (b - r) + max 0 (c - r) := by have hb : b - r ≤ max 0 (b - r) := le_max_right _ _ have hc : c - r ≤ max 0 (c - r) := le_max_right _ _ have hb0 : 0 ≤ max 0 (b - r) := le_max_left _ _ have hc0 : 0 ≤ max 0 (c - r) := le_max_left _ _ apply max_le · linarith · linarith
RankOneGramPseudoinverse 6 core · 5 supporting This module identifies eigenvector-based rank-one truncation and pseudoinverse formulas with a choice-free algebraic construction from the left Gram matrix. ★ algebraicRankOnePseudoInverse_isMoorePenrose
Rank-one truncation and pseudoinverse from a two-row Gram matrix
This module identifies eigenvector-based rank-one truncation and pseudoinverse formulas with a choice-free algebraic construction from the left Gram matrix. It proves the Moore--Penrose identities and local continuous differentiability on the isolated-positive-root region.
def leftGram reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real matrix with two rows, its left Gram matrix records all pairwise inner products of those rows.
def eigenvectorRankOneTruncation reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-vector and a real matrix with two rows, the eigenvector-selected rank-one truncation multiplies the matrix on the left by the outer product of the vector with itself. No condition is imposed on the vector: this is an orthogonal rank-one projection of the rows only when the vector has unit length (the intended use is a unit upper eigenvector of the left Gram matrix); a non-unit vector rescales the result and the zero vector gives the zero matrix.
def eigenvectorRankOnePseudoInverse reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-vector and a real matrix with two rows, the eigenvector-selected rank-one pseudoinverse formula is the transpose of the matrix times the outer product of the vector with itself, divided by the larger root of the left Gram matrix (zero if that root is zero). No condition is imposed on the vector; this is the Moore–Penrose pseudoinverse of the rank-one truncation only when the vector is a unit upper eigenvector of the left Gram matrix.
def algebraicRankOneTruncation reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real matrix with two rows, the choice-free algebraic rank-one truncation applies the algebraic upper projector of its left Gram matrix. It has rank one under a strict gap between the two roots of the left Gram matrix; without a gap the projector's division by the zero gap makes it the zero matrix.
def algebraicRankOnePseudoInverse reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real matrix with two rows, the choice-free algebraic rank-one pseudoinverse transposes the algebraically projected matrix and divides by the upper Gram root.
theorem algebraicRankOnePseudoInverse_isMoorePenrose reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-row matrix with a strict positive upper left-Gram root, the algebraic rank-one pseudoinverse satisfies all four Moore--Penrose equations for the algebraic rank-one truncation.
Formal statement
Proof (Lean source)
theorem algebraicRankOnePseudoInverse_isMoorePenrose {H : Matrix (Fin 2) E ℝ}
(hgap : leftGram H ∈ strictGapSet) (hpos : 0 < lambda₁ (leftGram H)) :
let A := algebraicRankOneTruncation H
let Aplus := algebraicRankOnePseudoInverse H
A * Aplus * A = A ∧
Aplus * A * Aplus = Aplus ∧
(A * Aplus).IsHermitian ∧
(Aplus * A).IsHermitian := by
let G := leftGram H
let P := topProjector G
let l := lambda₁ G
have hG : G.IsHermitian := leftGram_isHermitian H
have hP : P.IsHermitian := topProjector_isHermitian hG
have hPP : P * P = P := topProjector_mul_self hG hgap
have hl : l ≠ 0 := ne_of_gt hpos
have hdecomp : G = (lambda₁ G - lambda₂ G) • P + lambda₂ G • 1 := by
have hne : lambda₁ G - lambda₂ G ≠ 0 := ne_of_gt (sub_pos.mpr hgap)
ext i j
simp [P, topProjector]
field_simp [hne]
ring
have hPG : P * G = l • P := by
rw [hdecomp, Matrix.mul_add, Matrix.mul_smul, Matrix.mul_smul,
hPP, Matrix.mul_one]
ext i j
simp [l]
ring
have hAAplus :
algebraicRankOneTruncation H * algebraicRankOnePseudoInverse H = P := by
rw [algebraicRankOneTruncation, algebraicRankOnePseudoInverse,
Matrix.mul_smul]
change (lambda₁ G)⁻¹ • ((P * H) * (H.transpose * P)) = P
rw [← Matrix.mul_assoc (P * H) H.transpose P,
Matrix.mul_assoc P H H.transpose]
change (lambda₁ G)⁻¹ • (P * G * P) = P
rw [hPG, Matrix.smul_mul, hPP]
simp [l, hl]
have hAplusP : algebraicRankOnePseudoInverse H * P =
algebraicRankOnePseudoInverse H := by
rw [algebraicRankOnePseudoInverse, Matrix.smul_mul, Matrix.mul_assoc, hPP]
have hAplusA :
algebraicRankOnePseudoInverse H * algebraicRankOneTruncation H =
l⁻¹ • (H.transpose * P * H) := by
rw [algebraicRankOnePseudoInverse, algebraicRankOneTruncation,
Matrix.smul_mul]
change (lambda₁ G)⁻¹ • ((H.transpose * P) * (P * H)) =
(lambda₁ G)⁻¹ • (H.transpose * P * H)
rw [Matrix.mul_assoc, ← Matrix.mul_assoc P P H, hPP]
rw [Matrix.mul_assoc]
dsimp only
refine ⟨?_, ?_, hAAplus ▸ hP, ?_⟩
· rw [hAAplus]
change P * (P * H) = P * H
rw [← Matrix.mul_assoc, hPP]
· rw [Matrix.mul_assoc, hAAplus, hAplusP]
· rw [hAplusA]
apply (Matrix.isHermitian_conjTranspose_mul_mul H hP).smul
simp [isSelfAdjoint_iff]
5 supporting declarations (lemmas, instances)
-
leftGram_isHermitiantheorem — For a real matrix with two rows, its left Gram matrix is symmetric.Proof (Lean source)
theorem leftGram_isHermitian (H : Matrix (Fin 2) E ℝ) : (leftGram H).IsHermitian := by simpa [leftGram, conjTranspose_eq_transpose_of_trivial] using Matrix.isHermitian_mul_conjTranspose_self H -
eigenvectorRankOneTruncation_eq_algebraictheorem — Given a real two-row matrix with a strict left-Gram root gap and a unit upper left-Gram eigenvector, the eigenvector-selected and algebraic rank-one truncations agree.Proof (Lean source)
theorem eigenvectorRankOneTruncation_eq_algebraic {H : Matrix (Fin 2) E ℝ} (hgap : leftGram H ∈ strictGapSet) {u : Fin 2 → ℝ} (hu_unit : dotProduct u u = 1) (hu_eig : (leftGram H).mulVec u = lambda₁ (leftGram H) • u) : eigenvectorRankOneTruncation u H = algebraicRankOneTruncation H := by rw [eigenvectorRankOneTruncation, algebraicRankOneTruncation, topProjector_eq_outerProjector (leftGram_isHermitian H) hgap hu_unit hu_eig] -
eigenvectorRankOnePseudoInverse_eq_algebraictheorem — Given a real two-row matrix with a strict positive upper left-Gram root and a unit upper left-Gram eigenvector, the eigenvector-selected and algebraic rank-one pseudoinverse formulas agree.Proof (Lean source)
theorem eigenvectorRankOnePseudoInverse_eq_algebraic {H : Matrix (Fin 2) E ℝ} (hgap : leftGram H ∈ strictGapSet) (hpos : 0 < lambda₁ (leftGram H)) {u : Fin 2 → ℝ} (hu_unit : dotProduct u u = 1) (hu_eig : (leftGram H).mulVec u = lambda₁ (leftGram H) • u) : eigenvectorRankOnePseudoInverse u H = algebraicRankOnePseudoInverse H := by have _hlambda_ne : lambda₁ (leftGram H) ≠ 0 := ne_of_gt hpos rw [eigenvectorRankOnePseudoInverse, algebraicRankOnePseudoInverse, topProjector_eq_outerProjector (leftGram_isHermitian H) hgap hu_unit hu_eig] -
contDiffAt_algebraicRankOneTruncationtheorem — Given a real two-row matrix whose left Gram matrix has distinct roots, the algebraic rank-one truncation varies continuously differentiably near that matrix.Proof (Lean source)
theorem contDiffAt_algebraicRankOneTruncation {H : Matrix (Fin 2) E ℝ} (hgap : leftGram H ∈ strictGapSet) : ContDiffAt ℝ 1 algebraicRankOneTruncation H := by have hgram : ContDiffAt ℝ 1 leftGram H := by unfold leftGram exact contDiffAt_matrix_mul contDiffAt_id (contDiffAt_matrix_transpose contDiffAt_id) have hprojector : ContDiffAt ℝ 1 (fun X => topProjector (leftGram X)) H := (contDiffAt_topProjector hgap).comp H hgram unfold algebraicRankOneTruncation exact contDiffAt_matrix_mul hprojector contDiffAt_id -
contDiffAt_algebraicRankOnePseudoInversetheorem — Given a real two-row matrix whose left Gram matrix has a strict positive upper root, the algebraic rank-one pseudoinverse varies continuously differentiably near that matrix.Proof (Lean source)
theorem contDiffAt_algebraicRankOnePseudoInverse {H : Matrix (Fin 2) E ℝ} (hgap : leftGram H ∈ strictGapSet) (hpos : 0 < lambda₁ (leftGram H)) : ContDiffAt ℝ 1 algebraicRankOnePseudoInverse H := by have hgram : ContDiffAt ℝ 1 leftGram H := by unfold leftGram exact contDiffAt_matrix_mul contDiffAt_id (contDiffAt_matrix_transpose contDiffAt_id) have hlambda : ContDiffAt ℝ 1 (fun X => lambda₁ (leftGram X)) H := (contDiffAt_lambda₁ hgap).comp H hgram have hinv : ContDiffAt ℝ 1 (fun X => (lambda₁ (leftGram X))⁻¹) H := hlambda.inv (ne_of_gt hpos) have hprojector : ContDiffAt ℝ 1 (fun X => topProjector (leftGram X)) H := (contDiffAt_topProjector hgap).comp H hgram unfold algebraicRankOnePseudoInverse exact hinv.smul (contDiffAt_matrix_mul (contDiffAt_matrix_transpose contDiffAt_id) hprojector)
RankOneWaldSmoothness 4 core · 3 supporting This module composes the algebraic rank-one pseudoinverse with a target direction and an outcome direction. ★ algebraicWaldFunctional_hasLocallyBoundedFDerivAt
Smoothness of the induced rank-one Wald functional
This module composes the algebraic rank-one pseudoinverse with a target direction and an outcome direction. Its regularity condition is solely a positive isolated upper root of the left Gram matrix and makes no continuity assumption about an eigenvector selector.
abbrev WaldInput reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a finite outcome-coordinate type, an input to the rank-one Wald functional consists of a real two-row matrix, an outcome direction, and a two-dimensional target direction.
def waldRegularSet reviewed
⚑ flagged
Causalean.Mathlib.Analysis
The regularity region contains rank-one Wald inputs whose left Gram matrix has distinct roots and a strictly positive upper root.
def algebraicWaldFunctional reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a rank-one Wald input, the choice-free algebraic Wald functional applies the algebraic rank-one pseudoinverse to the target direction and pairs the result with the outcome direction.
Definition (Lean source)
parameters
E :
Type u_1
x :
def
algebraicWaldFunctional x :
ℝ
given by
theorem algebraicWaldFunctional_hasLocallyBoundedFDerivAt reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a rank-one Wald input in the regularity region, the algebraic Wald functional has a bounded Fréchet derivative on some neighborhood of that input.
Formal statement
hypotheses
hx :
x ∈ waldRegularSet (E := E)
conclusion
HasLocallyBoundedFDerivAt (algebraicWaldFunctional (E := E)) x
Proof (Lean source)
theorem algebraicWaldFunctional_hasLocallyBoundedFDerivAt {x : WaldInput E}
(hx : x ∈ waldRegularSet (E := E)) :
HasLocallyBoundedFDerivAt (algebraicWaldFunctional (E := E)) x := by
exact ContDiffAt.hasLocallyBoundedFDerivAt (contDiffAt_algebraicWaldFunctional hx)
3 supporting declarations (lemmas, instances)
-
isOpen_waldRegularSettheorem — The regularity region of the algebraic rank-one Wald functional is open.Proof (Lean source)
theorem isOpen_waldRegularSet : IsOpen (waldRegularSet (E := E)) := by rw [show waldRegularSet (E := E) = (fun x : WaldInput E => leftGram x.1) ⁻¹' strictGapSet ∩ {x | 0 < lambda₁ (leftGram x.1)} by rfl] apply (isOpen_strictGapSet.preimage continuous_leftGram_fst).inter have hlambda : Continuous (fun x : WaldInput E => lambda₁ (leftGram x.1)) := by unfold lambda₁ rootDiscriminant leftGram fun_prop exact isOpen_lt continuous_const hlambda -
contDiffAt_algebraicWaldFunctionaltheorem — Given a rank-one Wald input in the regularity region, the algebraic Wald functional varies continuously differentiably near that input.hypotheseshx :x ∈ waldRegularSet (E := E)conclusionContDiffAt ℝ 1 (algebraicWaldFunctional (E := E)) xProof (Lean source)
theorem contDiffAt_algebraicWaldFunctional {x : WaldInput E} (hx : x ∈ waldRegularSet (E := E)) : ContDiffAt ℝ 1 (algebraicWaldFunctional (E := E)) x := by have hpinv : ContDiffAt ℝ 1 (fun y : WaldInput E => algebraicRankOnePseudoInverse y.1) x := (contDiffAt_algebraicRankOnePseudoInverse hx.1 hx.2).comp x (by fun_prop) have hmulVec : ContDiffAt ℝ 1 (fun y : WaldInput E => (algebraicRankOnePseudoInverse y.1).mulVec y.2.2) x := by apply contDiffAt_pi' intro i simp only [mulVec] apply ContDiffAt.sum intro j _ exact ((contDiffAt_pi.mp (contDiffAt_pi.mp hpinv i) j).mul (by fun_prop)) unfold algebraicWaldFunctional dotProduct apply ContDiffAt.sum intro i _ exact (by fun_prop : ContDiffAt ℝ 1 (fun y : WaldInput E => y.2.1 i) x).mul (contDiffAt_pi.mp hmulVec i) -
contDiffOn_algebraicWaldFunctionaltheorem — The algebraic Wald functional is continuously differentiable throughout its regularity region.hypothesesE :sharedType u_1conclusionProof (Lean source)
theorem contDiffOn_algebraicWaldFunctional : ContDiffOn ℝ 1 (algebraicWaldFunctional (E := E)) (waldRegularSet (E := E)) := by intro x hx exact (contDiffAt_algebraicWaldFunctional hx).contDiffWithinAt
RectangularSignalSingularValues 4 core · 7 supporting This module provides reusable finite-dimensional real singular-value results for rectangular products, orthonormal compression to an adjoint range, and vertical stacking. ★ singularValues_product_adjoint_lower_bound★ singularValues_le_verticalStack_left★ singularValues_comp_linearIsometry_of_range_eq_adjoint_range
Rectangular signal singular values
This module provides reusable finite-dimensional real singular-value results for rectangular products, orthonormal compression to an adjoint range, and vertical stacking. The product bound works on the rank-sized signal subspace rather than assuming an ambient adjoint is injective; all results retain Mathlib's zero-extended singular-value indexing.
theorem singularValues_product_adjoint_lower_bound reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a left rectangular factor, an injective square core, a right rectangular factor, and full-column-rank assumptions for the two rectangular factors, the last signal singular value of their adjoint product is at least the product of the three least signal singular values.
Formal statement
hypotheses
E :
Type u_1
F :
Type u_2
A :
K →ₗ[ℝ] F
D :
K →ₗ[ℝ] K
B :
K →ₗ[ℝ] E
hA :
hD :
hB :
conclusion
A.singularValues (finrank ℝ K - 1) * D.singularValues (finrank ℝ K - 1) * B.singularValues (finrank ℝ K - 1)
≤ (A ∘ₗ D ∘ₗ B.adjoint).singularValues (finrank ℝ K - 1)
Proof (Lean source)
theorem singularValues_product_adjoint_lower_bound
[Nontrivial K]
(A : K →ₗ[ℝ] F) (D : K →ₗ[ℝ] K) (B : K →ₗ[ℝ] E)
(hA : Injective A) (hD : Injective D)
(hB : Injective B) :
A.singularValues (finrank ℝ K - 1) *
D.singularValues (finrank ℝ K - 1) *
B.singularValues (finrank ℝ K - 1) ≤
(A ∘ₗ D ∘ₗ B.adjoint).singularValues (finrank ℝ K - 1) := by
apply le_singularValues_of_subspace (A ∘ₗ D ∘ₗ B.adjoint) B.range
· exact mul_nonneg
(mul_nonneg (A.singularValues_nonneg _) (D.singularValues_nonneg _))
(B.singularValues_nonneg _)
· rw [B.finrank_range_of_inj hB]
exact sub_lt (Module.finrank_pos) (by omega)
· intro y hy
have hBadj := least_singularValue_mul_norm_le_adjoint_on_range B hB y hy
have hDleast := least_singularValue_mul_norm_le D hD (B.adjoint y)
have hAleast := least_singularValue_mul_norm_le A hA (D (B.adjoint y))
calc
(A.singularValues (finrank ℝ K - 1) *
D.singularValues (finrank ℝ K - 1) *
B.singularValues (finrank ℝ K - 1)) * ‖y‖ =
(A.singularValues (finrank ℝ K - 1) *
D.singularValues (finrank ℝ K - 1)) *
(B.singularValues (finrank ℝ K - 1) * ‖y‖) := by ring
_ ≤ (A.singularValues (finrank ℝ K - 1) *
D.singularValues (finrank ℝ K - 1)) * ‖B.adjoint y‖ :=
mul_le_mul_of_nonneg_left hBadj (mul_nonneg (A.singularValues_nonneg _)
(D.singularValues_nonneg _))
_ = A.singularValues (finrank ℝ K - 1) *
(D.singularValues (finrank ℝ K - 1) * ‖B.adjoint y‖) := by ring
_ ≤ A.singularValues (finrank ℝ K - 1) * ‖D (B.adjoint y)‖ :=
mul_le_mul_of_nonneg_left hDleast (A.singularValues_nonneg _)
_ ≤ ‖A (D (B.adjoint y))‖ := hAleast
_ = ‖(A ∘ₗ D ∘ₗ B.adjoint) y‖ := rfl
def verticalStack reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a real inner-product domain space, two real inner-product codomain spaces, and two real linear maps from the common domain into those respective codomains, the vertical stack is the real linear map sending each domain vector to its ordered pair of component outputs, equipped with the Hilbert direct-sum norm.
Definition (Lean source)
parameters
E :
Type u_1
F₀ :
Type u_2
F₁ :
Type u_3
M₀ :
E →ₗ[ℝ] F₀
M₁ :
E →ₗ[ℝ] F₁
def
given by
(WithLp.linearEquiv 2 ℝ (F₀ × F₁)).symm.comp (M₀.prod M₁)
theorem singularValues_le_verticalStack_left reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a first real linear map, a second compatible real linear map, and a singular-value index, the vertical stack's indexed singular value is at least that of the first component.
Formal statement
hypotheses
E :
Type u_1
F₀ :
Type u_2
F₁ :
Type u_3
M₀ :
E →ₗ[ℝ] F₀
M₁ :
E →ₗ[ℝ] F₁
j :
ℕ
conclusion
M₀.singularValues j ≤ (verticalStack M₀ M₁).singularValues j
Proof (Lean source)
theorem singularValues_le_verticalStack_left
(M₀ : E →ₗ[ℝ] F₀) (M₁ : E →ₗ[ℝ] F₁) (j : ℕ) :
M₀.singularValues j ≤ (verticalStack M₀ M₁).singularValues j := by
apply singularValues_le_of_gram_sub_isPositive M₀ (verticalStack M₀ M₁)
rw [verticalStack_adjoint_comp_self]
simpa using M₁.isPositive_adjoint_comp_self
theorem singularValues_comp_linearIsometry_of_range_eq_adjoint_range reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real linear map, orthonormal signal coordinates, an equality between the coordinate range and the map's adjoint range, and a singular-value index, compressing to those coordinates preserves the indexed singular value.
Formal statement
hypotheses
E :
Type u_1
F :
Type u_2
K :
Type u_3
M :
E →ₗ[ℝ] F
V :
K →ₗᵢ[ℝ] E
hrange :
V.toLinearMap.range = M.adjoint.range
j :
ℕ
conclusion
(M ∘ₗ V.toLinearMap).singularValues j = M.singularValues j
Proof (Lean source)
theorem singularValues_comp_linearIsometry_of_range_eq_adjoint_range
(M : E →ₗ[ℝ] F) (V : K →ₗᵢ[ℝ] E)
(hrange : V.toLinearMap.range = M.adjoint.range) (j : ℕ) :
(M ∘ₗ V.toLinearMap).singularValues j = M.singularValues j := by
let A := M ∘ₗ V.toLinearMap
have hfin : finrank ℝ K = finrank ℝ M.range := by
calc
finrank ℝ K = finrank ℝ V.toLinearMap.range := V.equivRange.toLinearEquiv.finrank_eq
_ = finrank ℝ M.adjoint.range := by rw [hrange]
_ = finrank ℝ M.range := M.finrank_range_adjoint
have hrangeA : A.range = M.range := by
change (M ∘ₗ V.toLinearMap).range = M.range
rw [LinearMap.range_comp, hrange, ← LinearMap.range_comp]
exact M.range_self_comp_adjoint
by_cases hj : j < finrank ℝ M.range
· have hjK : j < finrank ℝ K := by omega
apply le_antisymm
· obtain ⟨S, hdimS, hboundS⟩ :=
Causalean.Mathlib.Analysis.exists_large_subspace_norm_le_singularValues M
(hj.trans_le (LinearMap.finrank_range_le M))
let T : Submodule ℝ K := S.comap V.toLinearMap
have hmapT : T.map V.toLinearMap = V.toLinearMap.range ⊓ S := by
simpa [T, inf_comm] using Submodule.map_comap_eq V.toLinearMap S
have hdim_map (U : Submodule ℝ K) :
finrank ℝ (U.map V.toLinearMap) = finrank ℝ U := by
let f : U →ₗ[ℝ] E := V.toLinearMap.comp U.subtype
have hf : Injective f := V.injective.comp U.injective_subtype
have hfrange : f.range = U.map V.toLinearMap := by
simp [f, LinearMap.range_comp]
rw [← hfrange, f.finrank_range_of_inj hf]
have hdimT : finrank ℝ K ≤ finrank ℝ T + j := by
have hsum :=
Submodule.finrank_sup_add_finrank_inf_eq V.toLinearMap.range S
have hsup := Submodule.finrank_le (V.toLinearMap.range ⊔ S)
have hfinV : finrank ℝ V.toLinearMap.range = finrank ℝ K := by
simpa using V.equivRange.toLinearEquiv.finrank_eq.symm
rw [← hmapT, hdim_map, hfinV] at hsum
omega
apply
singularValues_le_of_large_subspace A hjK T hdimT
intro x hx
simpa [A] using hboundS (V x) hx
· obtain ⟨T, hdimT, hboundT⟩ :=
Causalean.Mathlib.Analysis.exists_large_subspace_norm_le_singularValues A hjK
let U : Submodule ℝ E := T.map V.toLinearMap
let S : Submodule ℝ E := U ⊔ M.ker
have hUorth : U ≤ M.kerᗮ := by
rw [M.orthogonal_ker, ← hrange]
exact LinearMap.map_le_range
have hdisjoint : Disjoint U M.ker :=
M.ker.orthogonal_disjoint.symm.mono hUorth le_rfl
have hdimU : finrank ℝ U = finrank ℝ T := by
let f : T →ₗ[ℝ] E := V.toLinearMap.comp T.subtype
have hf : Injective f := V.injective.comp T.injective_subtype
have hfrange : f.range = U := by
simp [f, U, LinearMap.range_comp]
rw [← hfrange, f.finrank_range_of_inj hf]
have hdimS : finrank ℝ E ≤ finrank ℝ S + j := by
have hsum := Submodule.finrank_sup_add_finrank_inf_eq U M.ker
rw [hdisjoint.eq_bot, finrank_bot, add_zero, hdimU] at hsum
have hranknull := M.finrank_range_add_finrank_ker
dsimp [S]
omega
apply
singularValues_le_of_large_subspace M
(hj.trans_le (LinearMap.finrank_range_le M)) S hdimS
intro x hx
rcases Submodule.mem_sup.mp hx with ⟨u, hu, k, hk, rfl⟩
rcases hu with ⟨t, ht, rfl⟩
have hvorth : V t ∈ M.kerᗮ := hUorth (by exact ⟨t, ht, rfl⟩)
have hinter : inner ℝ (V t) k = 0 :=
(M.ker.mem_orthogonal' (V t)).mp hvorth k hk
have hnormsq : ‖V t + k‖ ^ 2 = ‖V t‖ ^ 2 + ‖k‖ ^ 2 :=
by simpa [pow_two] using
norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (V t) k hinter
have hnormle : ‖t‖ ≤ ‖V t + k‖ := by
rw [V.norm_map] at hnormsq
nlinarith [sq_nonneg ‖k‖, norm_nonneg (V t + k), norm_nonneg t]
calc
‖M (V t + k)‖ = ‖A t‖ := by
simp [A, LinearMap.mem_ker.mp hk]
_ ≤ A.singularValues j * ‖t‖ := hboundT t ht
_ ≤ A.singularValues j * ‖V t + k‖ :=
mul_le_mul_of_nonneg_left hnormle (A.singularValues_nonneg j)
· have hle : finrank ℝ M.range ≤ j := Nat.le_of_not_gt hj
have hleA : finrank ℝ A.range ≤ j := by rwa [hrangeA]
rw [A.singularValues_eq_zero_iff_le_finrank_range.mpr hleA,
M.singularValues_eq_zero_iff_le_finrank_range.mpr hle]
7 supporting declarations (lemmas, instances)
-
le_singularValues_of_subspacetheorem — Given a real linear map, a candidate signal subspace, a singular-value index, a nonnegative expansion factor, a dimension condition putting that index below the signal-subspace dimension, and a lower expansion bound on the signal subspace, the indexed singular value is at least that factor.hypothesesE :sharedType u_1F :sharedType u_2T :E →ₗ[ℝ] FS :Submodule ℝ Ej :ℕc :ℝhc :0 ≤ chdim :j < finrank ℝ Shbound :∀ x : Eifx ∈ Sthenc * ‖x‖ ≤ ‖T x‖conclusionc ≤ T.singularValues jProof (Lean source)
theorem le_singularValues_of_subspace (T : E →ₗ[ℝ] F) (S : Submodule ℝ E) {j : ℕ} {c : ℝ} (hc : 0 ≤ c) (hdim : j < finrank ℝ S) (hbound : ∀ x : E, x ∈ S → c * ‖x‖ ≤ ‖T x‖) : c ≤ T.singularValues j := by have hj : j < finrank ℝ E := lt_of_lt_of_le hdim (Submodule.finrank_le S) obtain ⟨L, hdimL, hTL⟩ := Causalean.Mathlib.Analysis.exists_large_subspace_norm_le_singularValues T hj have hinfne : S ⊓ L ≠ ⊥ := by intro hinf have hformula := S.finrank_sup_add_finrank_inf_eq L have hsup := Submodule.finrank_le (S ⊔ L) rw [hinf, finrank_bot, add_zero] at hformula omega obtain ⟨x, hx, hx0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hinfne have hlower := hbound x hx.1 have hupper := hTL x hx.2 have hxnorm : 0 < ‖x‖ := norm_pos_iff.mpr hx0 nlinarith -
least_singularValue_mul_norm_letheorem — Given an injective finite-dimensional real linear map and a vector in its domain, the map expands that vector by at least its last domain-indexed singular value.hypothesesconclusionT.singularValues (finrank ℝ E - 1) * ‖x‖ ≤ ‖T x‖Proof (Lean source)
theorem least_singularValue_mul_norm_le [Nontrivial E] (T : E →ₗ[ℝ] F) (hT : Injective T) (x : E) : T.singularValues (finrank ℝ E - 1) * ‖x‖ ≤ ‖T x‖ := by let hself := T.isSymmetric_adjoint_comp_self let b := hself.eigenvectorBasis rfl have hdimpos : 0 < finrank ℝ E := Module.finrank_pos have hj : finrank ℝ E - 1 < finrank ℝ E := by omega have hof (r : ℝ) : (RCLike.ofReal r : ℝ) = r := by calc (RCLike.ofReal r : ℝ) = RCLike.re (RCLike.ofReal r : ℝ) := (RCLike.re_to_real).symm _ = r := RCLike.ofReal_re r have hnorm_sq : ‖T x‖ ^ 2 = ∑ i : Fin (finrank ℝ E), hself.eigenvalues rfl i * ‖inner ℝ (b i) x‖ ^ 2 := by calc ‖T x‖ ^ 2 = inner ℝ (T x) (T x) := (real_inner_self_eq_norm_sq _).symm _ = inner ℝ x ((T.adjoint ∘ₗ T) x) := by exact (T.adjoint_inner_right x (T x)).symm _ = ∑ i, inner ℝ x (b i) * inner ℝ (b i) ((T.adjoint ∘ₗ T) x) := (b.sum_inner_mul_inner x ((T.adjoint ∘ₗ T) x)).symm _ = ∑ i, hself.eigenvalues rfl i * ‖inner ℝ (b i) x‖ ^ 2 := by apply Finset.sum_congr rfl intro i _ rw [← hself (b i) x, hself.apply_eigenvectorBasis] simp only [real_inner_smul_left, hof] rw [real_inner_comm x (b i)] simp only [Real.norm_eq_abs, sq_abs] ring have hlam (i : Fin (finrank ℝ E)) : T.singularValues (finrank ℝ E - 1) ^ 2 ≤ hself.eigenvalues rfl i := by rw [T.sq_singularValues_fin rfl ⟨finrank ℝ E - 1, hj⟩] exact hself.eigenvalues_antitone rfl (by apply Fin.le_iff_val_le_val.mpr exact Nat.le_sub_one_of_lt i.isLt) apply (sq_le_sq₀ (mul_nonneg (T.singularValues_nonneg _) (norm_nonneg _)) (norm_nonneg _)).mp rw [mul_pow, hnorm_sq, ← b.sum_sq_norm_inner_right x, Finset.mul_sum] exact Finset.sum_le_sum fun i _ => mul_le_mul_of_nonneg_right (hlam i) (sq_nonneg _) -
least_singularValue_mul_norm_le_adjoint_on_rangetheorem — Given a full-column-rank real linear map and a vector in its column space, the adjoint expands that signal vector by at least the map's least singular value.hypothesesE :sharedType u_1B :K →ₗ[ℝ] EhB :y :Ehy :y ∈ B.rangeconclusionB.singularValues (finrank ℝ K - 1) * ‖y‖ ≤ ‖B.adjoint y‖Proof (Lean source)
theorem least_singularValue_mul_norm_le_adjoint_on_range [Nontrivial K] (B : K →ₗ[ℝ] E) (hB : Injective B) (y : E) (hy : y ∈ B.range) : B.singularValues (finrank ℝ K - 1) * ‖y‖ ≤ ‖B.adjoint y‖ := by rcases hy with ⟨z, rfl⟩ by_cases hz : z = 0 · simp [hz] have hzpos : 0 < ‖z‖ := norm_pos_iff.mpr hz have hleast := least_singularValue_mul_norm_le B hB z have hcs := real_inner_le_norm z (B.adjoint (B z)) have hadj : inner ℝ z (B.adjoint (B z)) = ‖B z‖ ^ 2 := by calc inner ℝ z (B.adjoint (B z)) = inner ℝ (B z) (B z) := B.adjoint_inner_right z (B z) _ = ‖B z‖ ^ 2 := real_inner_self_eq_norm_sq _ rw [hadj] at hcs have hsv := B.singularValues_nonneg (finrank ℝ K - 1) have hBnorm := norm_nonneg (B z) have hadjnorm := norm_nonneg (B.adjoint (B z)) nlinarith -
singularValues_mul_mul_transpose_lower_boundtheorem — Given finite real left and right matrices, an injective finite real square core, and full-column-rank assumptions for the two rectangular matrices, the last signal singular value of their transpose product is bounded below by the product of the three least signal singular values.hypothesesProof (Lean source)
theorem Matrix.singularValues_mul_mul_transpose_lower_bound {m n k : Type*} [Fintype m] [Fintype n] [Fintype k] [DecidableEq n] [DecidableEq k] [Nonempty k] (A : Matrix m k ℝ) (D : Matrix k k ℝ) (B : Matrix n k ℝ) (hA : Injective A.toEuclideanLin) (hD : Injective D.toEuclideanLin) (hB : Injective B.toEuclideanLin) : A.toEuclideanLin.singularValues (card k - 1) * D.toEuclideanLin.singularValues (card k - 1) * B.toEuclideanLin.singularValues (card k - 1) ≤ (A * D * B.transpose).toEuclideanLin.singularValues (card k - 1) := by have htrans : B.transpose = B.conjTranspose := by ext i j simp [Matrix.conjTranspose_apply] have hlin : (A * D * B.transpose).toEuclideanLin = A.toEuclideanLin ∘ₗ D.toEuclideanLin ∘ₗ B.toEuclideanLin.adjoint := by rw [← Matrix.toEuclideanLin_conjTranspose_eq_adjoint B, ← htrans] apply LinearMap.ext intro x apply PiLp.ext intro i simp only [LinearMap.comp_apply, Matrix.ofLp_toEuclideanLin_apply, Matrix.mulVec_mulVec] rw [Matrix.mul_assoc] have h := singularValues_product_adjoint_lower_bound A.toEuclideanLin D.toEuclideanLin B.toEuclideanLin hA hD hB simpa only [finrank_euclideanSpace, ← hlin] using h -
verticalStack_adjoint_comp_selftheorem — Given two real linear maps with a common domain, the Gram operator of their vertical stack is the sum of their two component Gram operators.hypothesesE :sharedType u_1F₀ :sharedType u_2F₁ :sharedType u_3M₀ :E →ₗ[ℝ] F₀M₁ :E →ₗ[ℝ] F₁conclusion(verticalStack M₀ M₁).adjoint ∘ₗ verticalStack M₀ M₁= (M₀.adjoint ∘ₗ M₀) + (M₁.adjoint ∘ₗ M₁)Proof (Lean source)
theorem verticalStack_adjoint_comp_self (M₀ : E →ₗ[ℝ] F₀) (M₁ : E →ₗ[ℝ] F₁) : (verticalStack M₀ M₁).adjoint ∘ₗ verticalStack M₀ M₁ = (M₀.adjoint ∘ₗ M₀) + (M₁.adjoint ∘ₗ M₁) := by ext x apply ext_inner_right ℝ intro y simp only [LinearMap.comp_apply, LinearMap.add_apply] rw [(verticalStack M₀ M₁).adjoint_inner_left, inner_add_left, M₀.adjoint_inner_left, M₁.adjoint_inner_left] rfl -
singularValues_le_verticalStack_righttheorem — Given a first compatible real linear map, a second real linear map, and a singular-value index, the vertical stack's indexed singular value is at least that of the second component.hypothesesE :sharedType u_1F₀ :sharedType u_2F₁ :sharedType u_3M₀ :E →ₗ[ℝ] F₀M₁ :E →ₗ[ℝ] F₁j :ℕconclusionM₁.singularValues j ≤ (verticalStack M₀ M₁).singularValues jProof (Lean source)
theorem singularValues_le_verticalStack_right (M₀ : E →ₗ[ℝ] F₀) (M₁ : E →ₗ[ℝ] F₁) (j : ℕ) : M₁.singularValues j ≤ (verticalStack M₀ M₁).singularValues j := by apply singularValues_le_of_gram_sub_isPositive M₁ (verticalStack M₀ M₁) rw [verticalStack_adjoint_comp_self] simpa [add_comm] using M₀.isPositive_adjoint_comp_self -
singularValues_comp_linearIsometry_lasttheorem — Given a real linear map, orthonormal coordinates for its adjoint range, the last coordinate-indexed singular value after compression equals the corresponding singular value before compression.hypothesesE :sharedType u_1F :sharedType u_2K :sharedType u_3M :E →ₗ[ℝ] FV :K →ₗᵢ[ℝ] Ehrange :V.toLinearMap.range = M.adjoint.rangeconclusionProof (Lean source)
theorem singularValues_comp_linearIsometry_last (M : E →ₗ[ℝ] F) (V : K →ₗᵢ[ℝ] E) (hrange : V.toLinearMap.range = M.adjoint.range) : (M ∘ₗ V.toLinearMap).singularValues (finrank ℝ K - 1) = M.singularValues (finrank ℝ K - 1) := by exact singularValues_comp_linearIsometry_of_range_eq_adjoint_range M V hrange _
RpowArith 4 core · 0 supporting This file provides reusable arithmetic identities and inequalities for real powers and square roots, especially for sample-size factors and negative exponents. ★ inv_eq_rpow_neg_one★ div_rpow_of_nonneg_of_pos★ rpow_natCast_nonpos_le_one★ inv_mul_sqrt_eq_rpow_neg_half
Small real-power arithmetic helpers
This file provides reusable arithmetic identities and inequalities for real
powers and square roots, especially for sample-size factors and negative
exponents. The main lemmas identify reciprocals with real powers
(inv_eq_rpow_neg_one), factor (A / n) ^ p into an A part
and an n part (div_rpow_of_nonneg_of_pos), bound nonpositive powers of natural casts
(rpow_natCast_nonpos_le_one), and rewrite q⁻¹ * sqrt q as q ^ (-1/2)
(inv_mul_sqrt_eq_rpow_neg_half).
lemma inv_eq_rpow_neg_one reviewed
⚑ flagged
Causalean.Mathlib.RpowArith
For any real number x, its reciprocal equals its real power raised to the exponent −1.
Formal statement
hypotheses
x :
ℝ
conclusion
x⁻¹ = x ^ (-1 : ℝ)
Proof (Lean source)
lemma inv_eq_rpow_neg_one (x : ℝ) : x⁻¹ = x ^ (-1 : ℝ) := by
rw [Real.rpow_neg_one]
lemma div_rpow_of_nonneg_of_pos reviewed
⚑ flagged
Causalean.Mathlib.RpowArith
Factoring a real power of a quotient. For a nonnegative numerator A and a strictly positive denominator n, the real power (A/n)^p equals A^p times n raised to the power −p, for any real exponent p.
Formal statement
hypotheses
A p n :
ℝ
hA :
0 ≤ A
hn :
0 < n
conclusion
(A / n) ^ p = A ^ p * n ^ (-p)
Proof (Lean source)
lemma div_rpow_of_nonneg_of_pos
(A p n : ℝ) (hA : 0 ≤ A) (hn : 0 < n) :
(A / n) ^ p = A ^ p * n ^ (-p) := by
have hnnonneg : 0 ≤ n := le_of_lt hn
have hinv_nonneg : 0 ≤ n⁻¹ := inv_nonneg.mpr hnnonneg
have hinv := inv_eq_rpow_neg_one n
calc
(A / n) ^ p = (A * n⁻¹) ^ p := by
rw [div_eq_mul_inv]
_ = A ^ p * (n⁻¹) ^ p := by
rw [Real.mul_rpow hA hinv_nonneg]
_ = A ^ p * (n ^ (-1 : ℝ)) ^ p := by
rw [hinv]
_ = A ^ p * n ^ ((-1 : ℝ) * p) := by
rw [Real.rpow_mul hnnonneg]
_ = A ^ p * n ^ (-p) := by
congr 1
ring_nf
lemma rpow_natCast_nonpos_le_one reviewed
⚑ flagged
Causalean.Mathlib.RpowArith
Nonpositive real power of a natural number is at most one. For a nonpositive real exponent e, the real power of any natural-number cast raised to e is at most 1.
Formal statement
hypotheses
n :
ℕ
e :
ℝ
he :
e ≤ 0
conclusion
(n : ℝ) ^ e ≤ 1
Proof (Lean source)
lemma rpow_natCast_nonpos_le_one
(n : ℕ) (e : ℝ) (he : e ≤ 0) :
(n : ℝ) ^ e ≤ 1 := by
cases n with
| zero =>
by_cases he_zero : e = 0
· simp [he_zero]
· simp [Real.zero_rpow he_zero]
| succ n =>
have hn_ge_one : 1 ≤ ((n + 1 : ℕ) : ℝ) := by
exact_mod_cast (Nat.succ_le_succ (zero_le n))
exact Real.rpow_le_one_of_one_le_of_nonpos hn_ge_one he
lemma inv_mul_sqrt_eq_rpow_neg_half reviewed
⚑ flagged
Causalean.Mathlib.RpowArith
Reciprocal times square root as a negative-half power. For a nonnegative real number q, the reciprocal of q times the square root of q equals q raised to the power −1/2.
Formal statement
Proof (Lean source)
lemma inv_mul_sqrt_eq_rpow_neg_half (q : ℝ) (hq : 0 ≤ q) :
q⁻¹ * sqrt q = q ^ (-(1 / 2 : ℝ)) := by
rcases hq.eq_or_lt with rfl | hq
· simp
· calc
q⁻¹ * sqrt q = q ^ (-1 : ℝ) * q ^ (1 / (2 : ℝ)) := by
rw [Real.sqrt_eq_rpow]
rw [Real.rpow_neg hq.le, Real.rpow_one]
_ = q ^ ((-1 : ℝ) + 1 / (2 : ℝ)) := by
rw [← Real.rpow_add hq]
_ = q ^ (-(1 / 2 : ℝ)) := by ring_nf
SecondOrderDescent 2 core · 8 supporting This module provides the one-dimensional smooth-optimization descent lemma. ★ second_order_descent_gap
Second-order descent for one real variable
This module provides the one-dimensional smooth-optimization descent lemma. A real function whose second derivative is bounded above in a segment's interior lies below the corresponding quadratic Taylor model, and a negative initial slope gives an explicit positive decrease at the clipped quadratic-model step.
The statements are objective-agnostic. Callers supply the regularity on Set.Icc 0 T
and the interior pointwise second-derivative bound; this file only turns those hypotheses into
the quadratic upper bound and the optimized descent gap.
def descentStep reviewed
⚑ flagged
Causalean.Mathlib.Analysis
For a real curvature bound, a real slope margin, and a real available interval length, the quadratic-model step is the available interval length when the curvature bound is zero and otherwise the smaller of that length and the slope margin divided by the curvature bound.
Definition (Lean source)
theorem second_order_descent_gap reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Quadratic-model descent gap. For a real function f on [0, T] where the interval length T, the slope margin c, and the curvature bound M are all nonnegative, f is twice continuously differentiable on [0, T], f is differentiable at 0, its second derivative is bounded above by M throughout the open interval, and its derivative at 0 is at most −c, then the clipped quadratic-model step lies in [0, T], and the resulting decrease f(0) − f(step) is at least c·step − (M/2)·step².
Formal statement
hypotheses
f :
ℝ → ℝ
M c T :
ℝ
hT :
0 ≤ T
hc :
0 ≤ c
hMnn :
0 ≤ M
hf :
ContDiffOn ℝ 2 f (Icc 0 T)
hf0 :
DifferentiableAt ℝ f 0
hslope :
deriv f 0 ≤ -c
Proof (Lean source)
theorem second_order_descent_gap {f : ℝ → ℝ} {M c T : ℝ} (hT : 0 ≤ T) (hc : 0 ≤ c)
(hMnn : 0 ≤ M) (hf : ContDiffOn ℝ 2 f (Icc 0 T)) (hf0 : DifferentiableAt ℝ f 0)
(hM : ∀ t ∈ Ioo 0 T, deriv (deriv f) t ≤ M) (hslope : deriv f 0 ≤ -c) :
descentStep M c T ∈ Icc 0 T ∧
f 0 - f (descentStep M c T) ≥
c * descentStep M c T - (M / 2) * descentStep M c T ^ 2 := by
let s := descentStep M c T
have hs : s ∈ Icc 0 T := descentStep_mem_Icc hMnn hc hT
refine ⟨hs, ?_⟩
have hs0 : 0 ≤ s := hs.1
have hub : f s ≤ f 0 + deriv f 0 * s + (M / 2) * s ^ 2 :=
second_order_upper_bound hf hf0 hM hs
have hslope_mul : deriv f 0 * s ≤ -c * s :=
mul_le_mul_of_nonneg_right hslope hs0
nlinarith
8 supporting declarations (lemmas, instances)
-
descentStep_of_eq_zerotheorem — With zero curvature bound, the clipped quadratic-model step is the endpoint.Proof (Lean source)
-
descentStep_of_postheorem — With a positive curvature bound, the clipped quadratic-model step is the smaller of the available interval length and the unconstrained quadratic-model optimizer.Proof (Lean source)
theorem descentStep_of_pos {M : ℝ} (hM : 0 < M) (c T : ℝ) : descentStep M c T = min T (c / M) := by simp [descentStep, hM.ne'] -
descentStep_mem_Icctheorem — The clipped quadratic-model step is feasible whenever the interval length, slope margin, and curvature bound are nonnegative.Proof (Lean source)
theorem descentStep_mem_Icc {M c T : ℝ} (hM : 0 ≤ M) (hc : 0 ≤ c) (hT : 0 ≤ T) : descentStep M c T ∈ Icc 0 T := by unfold descentStep split_ifs with h · exact ⟨hT, le_rfl⟩ · have hMpos : 0 < M := lt_of_le_of_ne hM (Ne.symm h) exact ⟨le_min hT (div_nonneg hc hM), min_le_left _ _⟩ -
second_order_upper_boundtheorem — A twice differentiable real function whose second derivative is bounded above on an interval's interior is no larger than its tangent at the left endpoint plus the quadratic curvature allowance.hypothesesf :ℝ → ℝM T :ℝhf :ContDiffOn ℝ 2 f (Icc 0 T)hf0 :DifferentiableAt ℝ f 0t :ℝht :t ∈ Icc 0 Tconclusionf t ≤ f 0 + deriv f 0 * t + (M / 2) * t ^ 2Proof (Lean source)
theorem second_order_upper_bound {f : ℝ → ℝ} {M T : ℝ} (hf : ContDiffOn ℝ 2 f (Icc 0 T)) (hf0 : DifferentiableAt ℝ f 0) (hM : ∀ t ∈ Ioo 0 T, deriv (deriv f) t ≤ M) {t : ℝ} (ht : t ∈ Icc 0 T) : f t ≤ f 0 + deriv f 0 * t + (M / 2) * t ^ 2 := by rcases ht with ⟨ht0, htT⟩ rcases ht0.eq_or_lt with rfl | htpos · simp · have hf' : ContDiffOn ℝ 2 f (Icc 0 t) := hf.mono (Icc_subset_Icc le_rfl htT) have huIcc : uIcc (0 : ℝ) t = Icc 0 t := uIcc_of_le htpos.le have huIoo : uIoo (0 : ℝ) t = Ioo 0 t := uIoo_of_le htpos.le have htay : ∃ x' ∈ Ioo (0 : ℝ) t, f t - taylorWithinEval f 1 (Icc 0 t) 0 t = iteratedDeriv 2 f x' * (t - 0) ^ 2 / (factorial 2) := by have h0 := taylor_mean_remainder_lagrange_iteratedDeriv (f := f) (x := t) (x₀ := 0) (n := 1) htpos.ne (by rw [huIcc] exact_mod_cast hf') rw [huIcc, huIoo] at h0 simpa using h0 have hpoly : taylorWithinEval f 1 (Icc 0 t) 0 t = f 0 + deriv f 0 * t := by rw [taylorWithinEval_succ, taylor_within_zero_eval, iteratedDerivWithin_one] · rw [hf0.derivWithin ((uniqueDiffOn_Icc htpos) 0 ⟨le_rfl, htpos.le⟩)] simp [mul_comm] have hid : iteratedDeriv 2 f = deriv (deriv f) := by rw [iteratedDeriv_succ, iteratedDeriv_one] rcases htay with ⟨ξ, hξ, heq⟩ have hb : deriv (deriv f) ξ ≤ M := hM ξ ⟨hξ.1, hξ.2.trans_le htT⟩ have heq' : f t - (f 0 + deriv f 0 * t) = deriv (deriv f) ξ * t ^ 2 / 2 := by rw [hpoly, hid] at heq simpa [sub_zero, factorial] using heq have hquad : deriv (deriv f) ξ * t ^ 2 / 2 ≤ M * t ^ 2 / 2 := by nlinarith [sq_nonneg t, hb] nlinarith -
first_order_upper_boundtheorem — A real function with nonpositive second derivative in an interval's interior lies below its tangent line at the left endpoint.hypothesesconclusionf t ≤ f 0 + deriv f 0 * tProof (Lean source)
theorem first_order_upper_bound {f : ℝ → ℝ} {T : ℝ} (hf : ContDiffOn ℝ 2 f (Icc 0 T)) (hf0 : DifferentiableAt ℝ f 0) (hM : ∀ t ∈ Ioo 0 T, deriv (deriv f) t ≤ 0) {t : ℝ} (ht : t ∈ Icc 0 T) : f t ≤ f 0 + deriv f 0 * t := by have h := second_order_upper_bound (M := 0) hf hf0 hM ht simpa using h -
second_order_descent_gap_mintheorem — With positive curvature, the clipped quadratic-model step gives at least half of the linear descent term.hypothesesf :ℝ → ℝM c T :ℝhT :0 ≤ Thc :0 ≤ chMpos :0 < Mhf :ContDiffOn ℝ 2 f (Icc 0 T)hf0 :DifferentiableAt ℝ f 0hslope :deriv f 0 ≤ -cProof (Lean source)
theorem second_order_descent_gap_min {f : ℝ → ℝ} {M c T : ℝ} (hT : 0 ≤ T) (hc : 0 ≤ c) (hMpos : 0 < M) (hf : ContDiffOn ℝ 2 f (Icc 0 T)) (hf0 : DifferentiableAt ℝ f 0) (hM : ∀ t ∈ Ioo 0 T, deriv (deriv f) t ≤ M) (hslope : deriv f 0 ≤ -c) : f 0 - f (min T (c / M)) ≥ (c / 2) * min T (c / M) := by let s := min T (c / M) have hraw : f 0 - f s ≥ c * s - (M / 2) * s ^ 2 := by simpa [s, descentStep_of_pos hMpos] using (second_order_descent_gap hT hc hMpos.le hf hf0 hM hslope).2 have hsle : s ≤ c / M := min_le_right T (c / M) have hMs : s * M ≤ c := (le_div_iff₀ hMpos).mp hsle have hs0 : 0 ≤ s := le_min hT (div_nonneg hc hMpos.le) nlinarith -
first_order_descent_gaptheorem — With zero curvature, the endpoint step gives the full linear descent guaranteed by the negative initial slope.hypothesesf :ℝ → ℝc T :ℝhT :0 ≤ Thf :ContDiffOn ℝ 2 f (Icc 0 T)hf0 :DifferentiableAt ℝ f 0hslope :deriv f 0 ≤ -cconclusionf 0 - f T ≥ c * TProof (Lean source)
theorem first_order_descent_gap {f : ℝ → ℝ} {c T : ℝ} (hT : 0 ≤ T) (hf : ContDiffOn ℝ 2 f (Icc 0 T)) (hf0 : DifferentiableAt ℝ f 0) (hM : ∀ t ∈ Ioo 0 T, deriv (deriv f) t ≤ 0) (hslope : deriv f 0 ≤ -c) : f 0 - f T ≥ c * T := by have hub : f T ≤ f 0 + deriv f 0 * T := first_order_upper_bound hf hf0 hM (right_mem_Icc.mpr hT) have hslope_mul : deriv f 0 * T ≤ -c * T := mul_le_mul_of_nonneg_right hslope hT nlinarith -
second_order_descent_gap_halftheorem — In both zero and positive curvature regimes, the clipped quadratic-model step gives a uniform half-linear decrease.hypothesesf :ℝ → ℝM c T :ℝhT :0 ≤ Thc :0 ≤ chMnn :0 ≤ Mhf :ContDiffOn ℝ 2 f (Icc 0 T)hf0 :DifferentiableAt ℝ f 0hslope :deriv f 0 ≤ -cconclusionconclusion 1descentStep M c T ∈ Icc 0 Tconclusion 2f 0 - f (descentStep M c T) ≥ (c / 2) * descentStep M c TProof (Lean source)
theorem second_order_descent_gap_half {f : ℝ → ℝ} {M c T : ℝ} (hT : 0 ≤ T) (hc : 0 ≤ c) (hMnn : 0 ≤ M) (hf : ContDiffOn ℝ 2 f (Icc 0 T)) (hf0 : DifferentiableAt ℝ f 0) (hM : ∀ t ∈ Ioo 0 T, deriv (deriv f) t ≤ M) (hslope : deriv f 0 ≤ -c) : descentStep M c T ∈ Icc 0 T ∧ f 0 - f (descentStep M c T) ≥ (c / 2) * descentStep M c T := by refine ⟨descentStep_mem_Icc hMnn hc hT, ?_⟩ rcases hMnn.eq_or_lt with hMzero | hMpos · rw [← hMzero, descentStep_of_eq_zero] have hM0 : ∀ t ∈ Ioo 0 T, deriv (deriv f) t ≤ 0 := by simpa [← hMzero] using hM have hgap : f 0 - f T ≥ c * T := first_order_descent_gap hT hf hf0 hM0 hslope nlinarith · rw [descentStep_of_pos hMpos] exact second_order_descent_gap_min hT hc hMpos hf hf0 hM hslope
SingularValueWeyl 1 core · 4 supporting This module proves the indexed Weyl--Mirsky perturbation inequality for singular values of finite-dimensional real linear maps. ★ abs_singularValues_add_sub_singularValues_le_opNorm
Weyl perturbation inequality for singular values
This module proves the indexed Weyl--Mirsky perturbation inequality for singular values of finite-dimensional real linear maps. Its support lemmas express the two halves of the singular value min--max argument using subspaces, and the main result shows that each singular value is 1-Lipschitz in the operator norm, including Mathlib's zero-extended indices.
theorem abs_singularValues_add_sub_singularValues_le_opNorm reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a baseline linear map, an additive perturbation, and a singular-value index, the absolute change in the indexed singular value is at most the perturbation's operator norm.
Formal statement
hypotheses
V :
Type u_1
W :
Type u_2
A D :
V →ₗ[ℝ] W
j :
ℕ
conclusion
|(A + D).singularValues j - A.singularValues j| ≤ ‖D.toContinuousLinearMap‖
Proof (Lean source)
theorem abs_singularValues_add_sub_singularValues_le_opNorm
(A D : V →ₗ[ℝ] W) (j : ℕ) :
|(A + D).singularValues j - A.singularValues j| ≤ ‖D.toContinuousLinearMap‖ := by
rw [abs_le]
constructor
· have h := singularValues_add_le_add_opNorm (A + D) (-D) j
have hnorm : ‖(-D).toContinuousLinearMap‖ = ‖D.toContinuousLinearMap‖ := by simp
have hcancel : A + D + -D = A := by abel
rw [hcancel, hnorm] at h
linarith
· have h := singularValues_add_le_add_opNorm A D j
linarith
4 supporting declarations (lemmas, instances)
-
singularValues_le_of_large_subspacetheorem — Given a linear map, an in-range singular-value index, and a subspace whose codimension is at most that index, if the map is bounded by a scalar multiple of the norm on that subspace, then the indexed singular value is at most that scalar.hypothesesV :sharedType u_1W :sharedType u_2A :V →ₗ[ℝ] Wj :ℕhj :j < finrank ℝ VS :Submodule ℝ Vc :ℝhbound :∀ x : Vifx ∈ Sthen‖A x‖ ≤ c * ‖x‖conclusionA.singularValues j ≤ cProof (Lean source)
theorem singularValues_le_of_large_subspace (A : V →ₗ[ℝ] W) {j : ℕ} (hj : j < finrank ℝ V) (S : Submodule ℝ V) (hdim : finrank ℝ V ≤ finrank ℝ S + j) {c : ℝ} (hbound : ∀ x : V, x ∈ S → ‖A x‖ ≤ c * ‖x‖) : A.singularValues j ≤ c := by let e : Fin (j + 1) → Fin (finrank ℝ V) := fun i => Fin.castLE (Nat.succ_le_iff.mpr hj) i let v : Fin (j + 1) → V := fun i => A.isSymmetric_adjoint_comp_self.eigenvectorBasis rfl (e i) let lam : Fin (j + 1) → ℝ := fun i => A.isSymmetric_adjoint_comp_self.eigenvalues rfl (e i) have hv : Orthonormal ℝ v := A.isSymmetric_adjoint_comp_self.eigenvectorBasis rfl |>.orthonormal.comp e (Fin.castLE_injective _) let U : Submodule ℝ V := span ℝ (range v) have hU : finrank ℝ U = j + 1 := by simpa [U] using finrank_span_eq_card hv.linearIndependent have hinfpos : 0 < finrank ℝ (U ⊓ S : Submodule ℝ V) := by have hformula := U.finrank_sup_add_finrank_inf_eq S have hsup := Submodule.finrank_le (U ⊔ S) rw [hU] at hformula omega have hinfne : U ⊓ S ≠ ⊥ := by intro h rw [h, finrank_bot] at hinfpos omega obtain ⟨x, hxUS, hx0⟩ := Submodule.exists_mem_ne_zero_of_ne_bot hinfne have hxU : x ∈ U := hxUS.1 have hxS : x ∈ S := hxUS.2 obtain ⟨a, ha⟩ := (Submodule.mem_span_range_iff_exists_fun ℝ).mp hxU have hx : (∑ i, a i • v i) = x := ha have hxnorm : ‖x‖ ^ 2 = ∑ i, (a i) ^ 2 := by rw [← hx, @norm_sq_eq_re_inner ℝ V] simpa [pow_two] using hv.inner_sum a a univ have hAe (i : Fin (j + 1)) : A.adjoint (A (v i)) = lam i • v i := by change (A.adjoint ∘ₗ A) _ = _ exact A.isSymmetric_adjoint_comp_self.apply_eigenvectorBasis rfl _ have hTx : A.adjoint (A (∑ i, a i • v i)) = ∑ i, (lam i * a i) • v i := by simp [map_sum, map_smul, hAe, smul_smul, mul_comm] have hAxnorm : ‖A x‖ ^ 2 = ∑ i, lam i * (a i) ^ 2 := by rw [← hx, @norm_sq_eq_re_inner ℝ W, ← A.adjoint_inner_left, hTx] simpa [mul_assoc, mul_left_comm, mul_comm, pow_two] using hv.inner_sum (fun i => lam i * a i) a univ have hlam (i : Fin (j + 1)) : A.singularValues j ^ 2 ≤ lam i := by rw [A.sq_singularValues_fin rfl ⟨j, hj⟩] exact A.isSymmetric_adjoint_comp_self.eigenvalues_antitone rfl (show e i ≤ (⟨j, hj⟩ : Fin (finrank ℝ V)) from Fin.le_iff_val_le_val.mpr (Nat.le_of_lt_succ i.isLt)) have hsq : (A.singularValues j * ‖x‖) ^ 2 ≤ ‖A x‖ ^ 2 := by rw [mul_pow, hxnorm, hAxnorm, Finset.mul_sum] exact Finset.sum_le_sum fun i _ => mul_le_mul_of_nonneg_right (hlam i) (sq_nonneg (a i)) have hlower : A.singularValues j * ‖x‖ ≤ ‖A x‖ := by exact (sq_le_sq₀ (mul_nonneg (A.singularValues_nonneg j) (norm_nonneg x)) (norm_nonneg (A x))).mp hsq have hupper := hbound x hxS have hnormpos : 0 < ‖x‖ := norm_pos_iff.mpr hx0 nlinarith -
exists_large_subspace_norm_le_singularValuestheorem — Given a linear map and an in-range singular-value index, there is a subspace whose codimension is at most that index and on which the map is bounded by the indexed singular value.hypothesesProof (Lean source)
theorem exists_large_subspace_norm_le_singularValues (A : V →ₗ[ℝ] W) {j : ℕ} (hj : j < finrank ℝ V) : ∃ S : Submodule ℝ V, finrank ℝ V ≤ finrank ℝ S + j ∧ ∀ x : V, x ∈ S → ‖A x‖ ≤ A.singularValues j * ‖x‖ := by classical let hT := A.isSymmetric_adjoint_comp_self let b := hT.eigenvectorBasis rfl let I := {i : Fin (finrank ℝ V) // j ≤ i.1} let S := span ℝ (range (fun i : I ↦ b i.1)) refine ⟨S, ?_, ?_⟩ · have hli : LinearIndependent ℝ (fun i : I ↦ b i.1) := b.orthonormal.linearIndependent.comp _ Subtype.val_injective have hdim : finrank ℝ S = card I := finrank_span_eq_card hli have hhead : card {i : Fin (finrank ℝ V) // ¬j ≤ i.1} = j := by simpa only [not_le, Fintype.card_fin] using (Fintype.card_congr (Fin.castLEOrderIso (le_of_lt hj)).symm.toEquiv) have hsplit := Fintype.card_subtype_compl (fun i : Fin (finrank ℝ V) ↦ j ≤ i.1) rw [hdim] dsimp [I] have hsplit' : j = finrank ℝ V - card {i : Fin (finrank ℝ V) // j ≤ i.1} := hhead.symm.trans (by simpa only [Fintype.card_fin] using hsplit) omega · intro x hx have hcoord {i : Fin (finrank ℝ V)} (hi : i.1 < j) : ⟪b i, x⟫_ℝ = 0 := by rcases (Submodule.mem_span_range_iff_exists_fun ℝ).mp hx with ⟨c, hc⟩ rw [← hc] simp only [inner_sum, real_inner_smul_right] apply Finset.sum_eq_zero intro k _ have hik : i ≠ k.1 := by intro h subst i omega rw [b.orthonormal.2 hik] simp have hof (r : ℝ) : (RCLike.ofReal r : ℝ) = r := by calc (RCLike.ofReal r : ℝ) = RCLike.re (RCLike.ofReal r : ℝ) := (RCLike.re_to_real).symm _ = r := RCLike.ofReal_re r have hnorm_sq : ‖A x‖ ^ 2 = ∑ i : Fin (finrank ℝ V), hT.eigenvalues rfl i * ‖⟪b i, x⟫_ℝ‖ ^ 2 := by calc ‖A x‖ ^ 2 = inner ℝ (A x) (A x) := (real_inner_self_eq_norm_sq _).symm _ = inner ℝ x ((A.adjoint ∘ₗ A) x) := by change inner ℝ (A x) (A x) = inner ℝ x (A.adjoint (A x)) exact (A.adjoint_inner_right x (A x)).symm _ = ∑ i, inner ℝ x (b i) * inner ℝ (b i) ((A.adjoint ∘ₗ A) x) := (b.sum_inner_mul_inner x ((A.adjoint ∘ₗ A) x)).symm _ = ∑ i, hT.eigenvalues rfl i * ‖inner ℝ (b i) x‖ ^ 2 := by apply Finset.sum_congr rfl intro i _ rw [← hT (b i) x, hT.apply_eigenvectorBasis] simp only [real_inner_smul_left, hof] rw [real_inner_comm x (b i)] simp only [Real.norm_eq_abs, sq_abs] ring apply (sq_le_sq₀ (norm_nonneg _) (mul_nonneg (A.singularValues_nonneg j) (norm_nonneg _))).mp rw [mul_pow] calc ‖A x‖ ^ 2 = ∑ i : Fin (finrank ℝ V), hT.eigenvalues rfl i * ‖inner ℝ (b i) x‖ ^ 2 := hnorm_sq _ ≤ ∑ i : Fin (finrank ℝ V), A.singularValues j ^ 2 * ‖inner ℝ (b i) x‖ ^ 2 := by apply Finset.sum_le_sum intro i _ by_cases hi : j ≤ i.1 · rw [A.sq_singularValues_fin rfl ⟨j, hj⟩] exact mul_le_mul_of_nonneg_right (hT.eigenvalues_antitone rfl hi) (sq_nonneg _) · have hc := hcoord (Nat.lt_of_not_ge hi) rw [hc, norm_zero, zero_pow (by omega : 2 ≠ 0), mul_zero, mul_zero] _ = A.singularValues j ^ 2 * ∑ i : Fin (finrank ℝ V), ‖inner ℝ (b i) x‖ ^ 2 := by rw [Finset.mul_sum] _ = A.singularValues j ^ 2 * ‖x‖ ^ 2 := by rw [b.sum_sq_norm_inner_right] -
singularValues_add_le_add_opNormtheorem — Given a baseline linear map, an additive perturbation, and a singular-value index, the perturbation can increase that indexed singular value by no more than its operator norm.hypothesesV :sharedType u_1W :sharedType u_2A D :V →ₗ[ℝ] Wj :ℕconclusion(A + D).singularValues j ≤ A.singularValues j + ‖D.toContinuousLinearMap‖Proof (Lean source)
theorem singularValues_add_le_add_opNorm (A D : V →ₗ[ℝ] W) (j : ℕ) : (A + D).singularValues j ≤ A.singularValues j + ‖D.toContinuousLinearMap‖ := by by_cases hj : j < finrank ℝ V · obtain ⟨S, hdim, hA⟩ := exists_large_subspace_norm_le_singularValues A hj apply singularValues_le_of_large_subspace (A + D) hj S hdim intro x hx calc ‖(A + D) x‖ ≤ ‖A x‖ + ‖D x‖ := by simpa only [LinearMap.add_apply] using norm_add_le (A x) (D x) _ ≤ A.singularValues j * ‖x‖ + ‖D.toContinuousLinearMap‖ * ‖x‖ := add_le_add (hA x hx) (D.toContinuousLinearMap.le_opNorm x) _ = (A.singularValues j + ‖D.toContinuousLinearMap‖) * ‖x‖ := by ring · have hdim : finrank ℝ V ≤ j := Nat.le_of_not_gt hj simp only [LinearMap.singularValues_of_finrank_le _ hdim, zero_add] exact norm_nonneg _ -
abs_singularValues_add_sub_singularValues_letheorem — Given a baseline continuous linear map, an additive continuous perturbation, and a singular-value index, the absolute change in the indexed singular value is at most the perturbation's operator norm.hypothesesV :sharedType u_1W :sharedType u_2A D :V →L[ℝ] Wj :ℕconclusion|(A + D).toLinearMap.singularValues j - A.toLinearMap.singularValues j| ≤ ‖D‖Proof (Lean source)
theorem ContinuousLinearMap.abs_singularValues_add_sub_singularValues_le (A D : V →L[ℝ] W) (j : ℕ) : |(A + D).toLinearMap.singularValues j - A.toLinearMap.singularValues j| ≤ ‖D‖ := by have hD : D.toLinearMap.toContinuousLinearMap = D := by ext x; rfl simpa [hD] using abs_singularValues_add_sub_singularValues_le_opNorm A.toLinearMap D.toLinearMap j
SmoothReciprocal 2 core · 3 supporting The reciprocal x ↦ x⁻¹ is singular at 0. ★ recipC_contDiff
A globally C¹ reciprocal with a floor near the singularity
The reciprocal x ↦ x⁻¹ is singular at 0. recipC ε is a modification that agrees with x⁻¹
on x ≥ ε/2 but is smoothly damped to 0 on the neighbourhood of the singularity, so it is
globally C¹ on all of ℝ. This is the reusable core of the "globally C¹ extension of an
objective that is singular on the boundary of its feasible box" pattern: multiply the singular part
by a Real.smoothTransition cutoff that is 1 on the feasible region and 0 past the boundary.
def recipC reviewed
⚑ flagged
Causalean.Mathlib
Given a real cutoff scale and a real argument , the floored reciprocal is multiplied by the smooth transition evaluated at . This definition applies for every real cutoff scale, including zero and negative values.
Definition (Lean source)
parameters
ε :
ℝ
x :
ℝ
def
recipC ε x :
ℝ
given by
Real.smoothTransition ((x - ε / 4) / (ε / 4)) * x⁻¹
lemma recipC_contDiff reviewed
⚑ flagged
Causalean.Mathlib
Global continuous differentiability of the floored reciprocal. For a strictly positive threshold ε, the floored reciprocal recipC ε is continuously differentiable on all of the reals.
Proof (Lean source)
@[fun_prop]
lemma recipC_contDiff (ε : ℝ) (hε : 0 < ε) : ContDiff ℝ 1 (recipC ε) :=
recipC_contDiff_of 1 ε hε
3 supporting declarations (lemmas, instances)
-
recipC_eq_invlemma — On the region x ≥ ε/2 (with ε > 0) the floored reciprocal is exactly x⁻¹, because the smooth cutoff has already saturated to 1 there.Proof (Lean source)
lemma recipC_eq_inv {ε x : ℝ} (hε : 0 < ε) (hx : ε / 2 ≤ x) : recipC ε x = x⁻¹ := by unfold recipC have hden : 0 < ε / 4 := by positivity have hone : 1 ≤ (x - ε / 4) / (ε / 4) := by rw [le_div_iff₀ hden] linarith rw [Real.smoothTransition.one_of_one_le hone] ring -
recipC_contDiff_oflemma — The floored reciprocal is globally Cⁿ on all of ℝ, for EVERY smoothness order n: near the singularity the smooth cutoff vanishes to infinite order, absorbing the blow-up of x⁻¹, and away from the singularity it is a product of Cⁿ functions.Proof (Lean source)
lemma recipC_contDiff_of (n : ℕ∞) (ε : ℝ) (hε : 0 < ε) : ContDiff ℝ n (recipC ε) := by rw [contDiff_iff_contDiffAt] intro x unfold recipC by_cases hx : x < ε / 4 · have hev : (fun y : ℝ => Real.smoothTransition ((y - ε / 4) / (ε / 4)) * y⁻¹) =ᶠ[nhds x] fun _ => 0 := by filter_upwards [Iio_mem_nhds hx] with y hy have harg : (y - ε / 4) / (ε / 4) ≤ 0 := by have hden : 0 < ε / 4 := by positivity exact div_nonpos_of_nonpos_of_nonneg (by linarith [show y < ε / 4 from hy]) hden.le rw [Real.smoothTransition.zero_of_nonpos harg] simp exact (contDiffAt_const : ContDiffAt ℝ n (fun _ : ℝ => (0 : ℝ)) x).congr_of_eventuallyEq hev · have hxpos : x ≠ 0 := by have hxge : ε / 4 ≤ x := le_of_not_gt hx have hpos : 0 < x := by linarith exact ne_of_gt hpos have hcut : ContDiffAt ℝ n (fun y : ℝ => Real.smoothTransition ((y - ε / 4) / (ε / 4))) x := by have hlin : ContDiff ℝ n (fun y : ℝ => (y - ε / 4) / (ε / 4)) := by fun_prop exact (Real.smoothTransition.contDiff.comp hlin).contDiffAt have hinv : ContDiffAt ℝ n (fun y : ℝ => y⁻¹) x := contDiffAt_inv ℝ hxpos exact hcut.mul hinv -
recipC_contDiff_twolemma — recipC ε is globally C². Specialization of recipC_contDiff_of; this is the order the reciprocal-product envelope's directional curvature modulus needs.Proof (Lean source)
@[fun_prop] lemma recipC_contDiff_two (ε : ℝ) (hε : 0 < ε) : ContDiff ℝ 2 (recipC ε) := recipC_contDiff_of 2 ε hε
TwoByTwoSpectralProjector 4 core · 9 supporting This module turns the two explicit roots into an algebraic projector onto the upper eigenspace of a real symmetric two-by-two matrix. ★ topProjector_isOrthogonalProjectorOntoTop
Choice-free top spectral projector in dimension two
This module turns the two explicit roots into an algebraic projector onto the upper eigenspace of a real symmetric two-by-two matrix. The formula is independent of any sign or basis choice for an eigenvector and is continuously differentiable on the strict-gap region.
def outerProjector reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-vector, its outer-product matrix has entries ; it has rank at most one (exactly one for a nonzero vector) and is the orthogonal projector onto the vector's direction when the vector has unit length.
def topProjector reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-by-two matrix, the algebraic upper spectral-projector candidate is its lower-root-shifted matrix divided by the gap between its explicit roots.
def IsOrthogonalProjectorOntoTop reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-by-two matrix and a candidate matrix, the property of being the orthogonal projector onto the upper-root eigenspace means that the candidate is symmetric, idempotent, and fixes exactly the upper-root eigenvectors.
theorem topProjector_isOrthogonalProjectorOntoTop reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Given a real two-by-two matrix that is symmetric and has distinct explicit roots, its algebraic quotient is the orthogonal projector onto the upper-root eigenspace.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem topProjector_isOrthogonalProjectorOntoTop {G : Matrix (Fin 2) (Fin 2) ℝ}
(hG : G.IsHermitian) (hgap : G ∈ strictGapSet) :
IsOrthogonalProjectorOntoTop G (topProjector G) := by
exact ⟨topProjector_isHermitian hG, topProjector_mul_self hG hgap,
topProjector_mulVec_eq_iff hG hgap⟩
9 supporting declarations (lemmas, instances)
-
topProjector_mulVec_eq_ifftheorem — Given a real symmetric two-by-two matrix with distinct explicit roots and a two-vector, the algebraic projector fixes that vector exactly when it is an upper-root eigenvector.hypothesesconclusionProof (Lean source)
theorem topProjector_mulVec_eq_iff {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G.IsHermitian) (hgap : G ∈ strictGapSet) (x : Fin 2 → ℝ) : (topProjector G).mulVec x = x ↔ G.mulVec x = lambda₁ G • x := by have hne : lambda₁ G - lambda₂ G ≠ 0 := ne_of_gt (sub_pos.mpr hgap) constructor <;> intro h <;> funext i · have hi := congrFun h i fin_cases i all_goals simp [topProjector, mulVec] at hi ⊢ field_simp [hne] at hi linarith · have hi := congrFun h i fin_cases i all_goals simp [topProjector, mulVec] at hi ⊢ field_simp [hne] linarith -
topProjector_mulVec_eq_zero_ifftheorem — Given a real symmetric two-by-two matrix with distinct explicit roots and a two-vector, the algebraic projector sends that vector to zero exactly when it is a lower-root eigenvector.hypothesesconclusionProof (Lean source)
theorem topProjector_mulVec_eq_zero_iff {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G.IsHermitian) (hgap : G ∈ strictGapSet) (x : Fin 2 → ℝ) : (topProjector G).mulVec x = 0 ↔ G.mulVec x = lambda₂ G • x := by have hne : lambda₁ G - lambda₂ G ≠ 0 := ne_of_gt (sub_pos.mpr hgap) constructor <;> intro h <;> funext i · have hi := congrFun h i fin_cases i all_goals simp [topProjector, mulVec] at hi ⊢ field_simp [hne] at hi linarith · have hi := congrFun h i fin_cases i all_goals simp [topProjector, mulVec] at hi ⊢ field_simp [hne] linarith -
topProjector_isHermitiantheorem — Given a real two-by-two matrix that is symmetric, its algebraic upper projector is symmetric.Proof (Lean source)
theorem topProjector_isHermitian {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G.IsHermitian) : (topProjector G).IsHermitian := by unfold topProjector apply (hG.sub (Matrix.isHermitian_one.smul ?_)).smul · simp [isSelfAdjoint_iff] · simp [isSelfAdjoint_iff] -
topProjector_mul_selftheorem — Given a real two-by-two matrix that is symmetric and has distinct explicit roots, its algebraic upper projector is idempotent.hypothesesconclusionProof (Lean source)
theorem topProjector_mul_self {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G.IsHermitian) (hgap : G ∈ strictGapSet) : topProjector G * topProjector G = topProjector G := by have hne : lambda₁ G - lambda₂ G ≠ 0 := ne_of_gt (sub_pos.mpr hgap) have hsym : G 1 0 = G 0 1 := by simpa using hG.apply 0 1 have hsum := lambda₁_add_lambda₂ G have hprod := lambda₁_mul_lambda₂ hG rw [Matrix.det_fin_two, hsym] at hprod have ha : lambda₁ G = G 0 0 + G 1 1 - lambda₂ G := by linarith [hsum] have hb : lambda₂ G ^ 2 - (G 0 0 + G 1 1) * lambda₂ G + (G 0 0 * G 1 1 - G 0 1 * G 0 1) = 0 := by rw [← hprod, ← hsum] ring ext i j fin_cases i <;> fin_cases j <;> simp [topProjector, Matrix.mul_apply] <;> field_simp [hne] <;> (try rw [hsym]) <;> rw [ha] <;> nlinarith [hb] -
topProjector_eq_outerProjectortheorem — Given a real symmetric two-by-two matrix with distinct explicit roots and a unit upper-root eigenvector, the algebraic upper projector equals that vector's outer-product projector.hypotheseshG :G.IsHermitianhgap :G ∈ strictGapSetv :Fin 2 → ℝhv_unit :dotProduct v v = 1hv_eig :G.mulVec v = lambda₁ G • vconclusiontopProjector G = outerProjector vProof (Lean source)
theorem topProjector_eq_outerProjector {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G.IsHermitian) (hgap : G ∈ strictGapSet) {v : Fin 2 → ℝ} (hv_unit : dotProduct v v = 1) (hv_eig : G.mulVec v = lambda₁ G • v) : topProjector G = outerProjector v := by have hne : lambda₁ G - lambda₂ G ≠ 0 := ne_of_gt (sub_pos.mpr hgap) have hsym : G 1 0 = G 0 1 := by simpa using hG.apply 0 1 have hsum := lambda₁_add_lambda₂ G have ha : lambda₁ G = G 0 0 + G 1 1 - lambda₂ G := by linarith [hsum] have h0 := congrFun hv_eig 0 have h1 := congrFun hv_eig 1 simp [mulVec] at h0 h1 rw [hsym, ha] at h1 rw [ha] at h0 simp [dotProduct] at hv_unit have hr0 : G 0 1 * v 1 = (G 1 1 - lambda₂ G) * v 0 := by linarith [h0] have hr1 : G 0 1 * v 0 = (G 0 0 - lambda₂ G) * v 1 := by linarith [h1] have h00 : G 0 0 - lambda₂ G = (lambda₁ G - lambda₂ G) * (v 0 * v 0) := by calc G 0 0 - lambda₂ G = (G 0 0 - lambda₂ G) * (v 0 * v 0 + v 1 * v 1) := by rw [hv_unit] ring _ = (G 0 0 - lambda₂ G) * (v 0 * v 0) + (G 0 1 * v 0) * v 1 := by rw [hr1]; ring _ = (G 0 0 - lambda₂ G) * (v 0 * v 0) + (G 0 1 * v 1) * v 0 := by ring _ = (G 0 0 + G 1 1 - 2 * lambda₂ G) * (v 0 * v 0) := by rw [hr0] ring _ = (lambda₁ G - lambda₂ G) * (v 0 * v 0) := by rw [ha]; ring have h11 : G 1 1 - lambda₂ G = (lambda₁ G - lambda₂ G) * (v 1 * v 1) := by calc G 1 1 - lambda₂ G = (G 1 1 - lambda₂ G) * (v 0 * v 0 + v 1 * v 1) := by rw [hv_unit] ring _ = (G 0 1 * v 1) * v 0 + (G 1 1 - lambda₂ G) * (v 1 * v 1) := by rw [hr0]; ring _ = (G 0 1 * v 0) * v 1 + (G 1 1 - lambda₂ G) * (v 1 * v 1) := by ring _ = (G 0 0 + G 1 1 - 2 * lambda₂ G) * (v 1 * v 1) := by rw [hr1] ring _ = (lambda₁ G - lambda₂ G) * (v 1 * v 1) := by rw [ha]; ring have h01 : G 0 1 = (lambda₁ G - lambda₂ G) * (v 0 * v 1) := by calc G 0 1 = G 0 1 * (v 0 * v 0 + v 1 * v 1) := by rw [hv_unit] ring _ = (G 0 1 * v 0) * v 0 + (G 0 1 * v 1) * v 1 := by ring _ = (G 0 0 + G 1 1 - 2 * lambda₂ G) * (v 0 * v 1) := by rw [hr0, hr1] ring _ = (lambda₁ G - lambda₂ G) * (v 0 * v 1) := by rw [ha]; ring ext i j fin_cases i <;> fin_cases j <;> simp [topProjector, outerProjector] <;> field_simp [hne] <;> (try rw [hsym]) <;> nlinarith [h00, h01, h11] -
outerProjector_eq_of_topEigenvectorstheorem — Given a real symmetric two-by-two matrix with distinct explicit roots and two unit upper-root eigenvectors, their outer-product projectors coincide.hypotheseshG :G.IsHermitianhgap :G ∈ strictGapSetv w :Fin 2 → ℝhv_unit :dotProduct v v = 1hv_eig :G.mulVec v = lambda₁ G • vhw_unit :dotProduct w w = 1hw_eig :G.mulVec w = lambda₁ G • wconclusionouterProjector v = outerProjector wProof (Lean source)
theorem outerProjector_eq_of_topEigenvectors {G : Matrix (Fin 2) (Fin 2) ℝ} (hG : G.IsHermitian) (hgap : G ∈ strictGapSet) {v w : Fin 2 → ℝ} (hv_unit : dotProduct v v = 1) (hv_eig : G.mulVec v = lambda₁ G • v) (hw_unit : dotProduct w w = 1) (hw_eig : G.mulVec w = lambda₁ G • w) : outerProjector v = outerProjector w := by rw [← topProjector_eq_outerProjector hG hgap hv_unit hv_eig, ← topProjector_eq_outerProjector hG hgap hw_unit hw_eig] -
outerProjector_negtheorem — Given a real two-vector, negating it leaves its outer-product projector unchanged.Proof (Lean source)
theorem outerProjector_neg (v : Fin 2 → ℝ) : outerProjector (-v) = outerProjector v := by ext i j simp [outerProjector] -
contDiffAt_topProjectortheorem — Given a real two-by-two matrix with distinct explicit roots, its algebraic upper projector varies continuously differentiably near that matrix.Proof (Lean source)
theorem contDiffAt_topProjector {G : Matrix (Fin 2) (Fin 2) ℝ} (hgap : G ∈ strictGapSet) : ContDiffAt ℝ 1 topProjector G := by have hne : lambda₁ G - lambda₂ G ≠ 0 := ne_of_gt (sub_pos.mpr hgap) have hscalar : ContDiffAt ℝ 1 (fun A => (lambda₁ A - lambda₂ A)⁻¹) G := ((contDiffAt_lambda₁ hgap).sub (contDiffAt_lambda₂ hgap)).inv hne have hmatrix : ContDiffAt ℝ 1 (fun A : Matrix (Fin 2) (Fin 2) ℝ => A - lambda₂ A • (1 : Matrix (Fin 2) (Fin 2) ℝ)) G := contDiffAt_id.sub ((contDiffAt_lambda₂ hgap).smul_const 1) change ContDiffAt ℝ 1 (fun A : Matrix (Fin 2) (Fin 2) ℝ => (lambda₁ A - lambda₂ A)⁻¹ • (A - lambda₂ A • (1 : Matrix (Fin 2) (Fin 2) ℝ))) G exact hscalar.smul hmatrix -
contDiffOn_topProjectortheorem — The algebraic upper projector is continuously differentiable throughout the strict-gap region.conclusionProof (Lean source)
theorem contDiffOn_topProjector : ContDiffOn ℝ 1 topProjector strictGapSet := by intro G hgap exact (contDiffAt_topProjector hgap).contDiffWithinAt
WeightedCauchySchwarz 2 core · 2 supporting Mathlib's discrete Cauchy–Schwarz Finset.sum_mul_sq_le_sq_mul_sq is stated for the *unweighted* inner product. ★ weighted_inner_sq_le★ abs_weighted_inner_le
Cauchy–Schwarz against a finite nonnegative weight vector
Mathlib's discrete Cauchy–Schwarz Finset.sum_mul_sq_le_sq_mul_sq is stated for the
unweighted inner product. Weighted versions (⟨f, g⟩_w = Σ wᵢ fᵢ gᵢ for a
nonnegative weight vector w) get re-derived by hand all over the library, so this
module records them once, over an arbitrary finite support.
* weighted_inner_sq_le — squared form (Σ wᵢ fᵢ gᵢ)² ≤ (Σ wᵢ fᵢ²)(Σ wᵢ gᵢ²).
* abs_weighted_inner_le — square-root form with an absolute value on the left.
* abs_weighted_mean_le_sqrt_weighted_sq — the subprobability-weight (Σ wᵢ ≤ 1)
specialization |Σ wᵢ fᵢ| ≤ √(Σ wᵢ fᵢ²), i.e. Jensen for x ↦ x².
* weighted_sqrt_le_sqrt_weighted — Jensen for √·: Σ wᵢ √qᵢ ≤ √(Σ wᵢ qᵢ).
All four follow from the unweighted inequality by substituting f ↦ √w · f,
g ↦ √w · g and simplifying with Real.sq_sqrt.
lemma weighted_inner_sq_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Weighted Cauchy-Schwarz inequality on a finite support, squared form. Weighting a finite collection of index points by nonnegative weights, the square of the weighted inner product of two real-valued functions is at most the product of their weighted sums of squares.
Formal statement
hypotheses
conclusion
(∑ i ∈ s, w i * (f i * g i)) ^ 2 ≤ (∑ i ∈ s, w i * f i ^ 2) * (∑ i ∈ s, w i * g i ^ 2)
Proof (Lean source)
lemma weighted_inner_sq_le (s : Finset ι) (w f g : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) :
(∑ i ∈ s, w i * (f i * g i)) ^ 2 ≤
(∑ i ∈ s, w i * f i ^ 2) * (∑ i ∈ s, w i * g i ^ 2) := by
have hprod : ∀ i ∈ s,
sqrt (w i) * f i * (sqrt (w i) * g i) = w i * (f i * g i) := by
intro i hi
have : sqrt (w i) * sqrt (w i) = w i := Real.mul_self_sqrt (hw i hi)
calc sqrt (w i) * f i * (sqrt (w i) * g i)
= sqrt (w i) * sqrt (w i) * (f i * g i) := by ring
_ = w i * (f i * g i) := by rw [this]
have hsq : ∀ (h : ι → ℝ) (i : ι) (_ : i ∈ s),
(sqrt (w i) * h i) ^ 2 = w i * h i ^ 2 := by
intro h i hi
rw [mul_pow, Real.sq_sqrt (hw i hi)]
have hsumprod :
∑ i ∈ s, sqrt (w i) * f i * (sqrt (w i) * g i) =
∑ i ∈ s, w i * (f i * g i) := by
apply Finset.sum_congr rfl
intro i hi
exact hprod i hi
have hsumsq (h : ι → ℝ) :
∑ i ∈ s, (sqrt (w i) * h i) ^ 2 = ∑ i ∈ s, w i * h i ^ 2 := by
apply Finset.sum_congr rfl
intro i hi
exact hsq h i hi
have key := Finset.sum_mul_sq_le_sq_mul_sq s
(fun i => sqrt (w i) * f i) (fun i => sqrt (w i) * g i)
rw [hsumprod, hsumsq f, hsumsq g] at key
exact key
lemma abs_weighted_inner_le reviewed
⚑ flagged
Causalean.Mathlib.Analysis
Weighted Cauchy-Schwarz inequality on a finite support, square-root form. With nonnegative weights, the absolute value of the weighted inner product of two real-valued functions is at most the product of the square roots of their weighted sums of squares.
Formal statement
Proof (Lean source)
lemma abs_weighted_inner_le (s : Finset ι) (w f g : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) :
|∑ i ∈ s, w i * (f i * g i)| ≤
sqrt (∑ i ∈ s, w i * f i ^ 2) * sqrt (∑ i ∈ s, w i * g i ^ 2) := by
have hP : (0 : ℝ) ≤ ∑ i ∈ s, w i * f i ^ 2 :=
sum_nonneg fun i hi => mul_nonneg (hw i hi) (sq_nonneg _)
have hstep : |∑ i ∈ s, w i * (f i * g i)|
≤ sqrt ((∑ i ∈ s, w i * f i ^ 2) * (∑ i ∈ s, w i * g i ^ 2)) := by
rw [← Real.sqrt_sq_eq_abs]
exact Real.sqrt_le_sqrt (weighted_inner_sq_le s w f g hw)
rwa [Real.sqrt_mul hP] at hstep
2 supporting declarations (lemmas, instances)
-
abs_weighted_mean_le_sqrt_weighted_sqlemma — Weighted mean is dominated by the weighted root-mean-square. For weights that are nonnegative and sum to at most one, the absolute value of the weighted average of a real-valued function is at most the square root of the weighted average of its square.hypothesesProof (Lean source)
lemma abs_weighted_mean_le_sqrt_weighted_sq (s : Finset ι) (w f : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (c : ℝ) (hmass : ∑ i ∈ s, w i ≤ c) : |∑ i ∈ s, w i * f i| ≤ sqrt c * sqrt (∑ i ∈ s, w i * f i ^ 2) := by have key := abs_weighted_inner_le s w f (fun _ => 1) hw simp only [mul_one, one_pow] at key have hsqrt : sqrt (∑ i ∈ s, w i) ≤ sqrt c := by have := Real.sqrt_le_sqrt hmass exact this calc _ ≤ sqrt (∑ i ∈ s, w i * f i ^ 2) * sqrt (∑ i ∈ s, w i) := key _ ≤ sqrt (∑ i ∈ s, w i * f i ^ 2) * sqrt c := mul_le_mul_of_nonneg_left hsqrt (Real.sqrt_nonneg _) _ = _ := mul_comm _ _ -
weighted_sqrt_le_sqrt_weightedlemma — Jensen's inequality for the square root. Averaging nonnegative values with weights that are nonnegative and sum to at most one, the weighted average of their square roots is at most the square root of their weighted average.hypothesesι :sharedType u_1s :Finset ιw q :ι → ℝhw :∀ i ∈ s, 0 ≤ w ic :ℝhmass :∑ i ∈ s, w i ≤ chq :∀ i ∈ s, 0 ≤ q iProof (Lean source)
lemma weighted_sqrt_le_sqrt_weighted (s : Finset ι) (w q : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (c : ℝ) (hmass : ∑ i ∈ s, w i ≤ c) (hq : ∀ i ∈ s, 0 ≤ q i) : ∑ i ∈ s, w i * sqrt (q i) ≤ sqrt c * sqrt (∑ i ∈ s, w i * q i) := by have key := abs_weighted_mean_le_sqrt_weighted_sq s w (fun i => sqrt (q i)) hw c hmass have hrw : ∀ i ∈ s, w i * sqrt (q i) ^ 2 = w i * q i := by intro i hi; rw [Real.sq_sqrt (hq i hi)] have hsumrw : ∑ i ∈ s, w i * sqrt (q i) ^ 2 = ∑ i ∈ s, w i * q i := by apply Finset.sum_congr rfl intro i hi exact hrw i hi rw [hsumrw] at key exact le_trans (le_abs_self _) key