mcshane_at_rat
plain-language theorem explainer
Analysts constructing Lipschitz extensions from dense subsets cite this result to confirm that the McShane envelope agrees with the original function at every rational point. Given an L-Lipschitz g_rat on the rationals, the infimum over q of g_rat(q) plus L times the distance to q0 recovers g_rat(q0) exactly. The argument uses order antisymmetry after establishing the infimum is at most the value at q0 via the bounded-below lemma and at least that value via the Lipschitz inequality.
Claim. Let $g : ℚ → ℝ$ satisfy $|g(q_1) - g(q_2)| ≤ L |q_1 - q_2|$ for all rationals $q_1, q_2$ and some $L ≥ 0$. Then for any rational $q_0$, $inf_{q ∈ ℚ} (g(q) + L |q_0 - q|) = g(q_0)$.
background
The module develops tools for equicontinuity in Galerkin approximations by extending Lipschitz maps from rationals to reals via the McShane formula. The map g_rat records values at rational points and obeys a uniform Lipschitz condition with constant L; the McShane upper extension at t is defined by the infimum of g_rat(q) + L|t - q| over q in Q. This construction produces an L-Lipschitz function on R that agrees with g_rat on the dense set Q.
proof idea
The term proof applies le_antisymm. The upper bound follows from ciInf_le_of_le using the bounded-below witness supplied by mcshane_bddBelow at q0, followed by simp. The lower bound follows from le_ciInf: the Lipschitz hypothesis supplies |g_rat(q0) - g_rat(q)| ≤ L |q0 - q|, which rearranges to the required inequality by linarith.
why it matters
The lemma is invoked inside lipschitz_dense_extension, which builds the full extension to R and proves that uniformly Lipschitz approximating sequences converge pointwise to the extension. In the Recognition Science setting the result supports equicontinuity arguments for Galerkin sequences in the Navier-Stokes equations, ensuring that limits of rational approximations remain faithful to the original data on the dense set.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.