r-irbe Lean 4 Real Analysis & Topology
Guide to formalizing analysis and topology in Lean 4 using Mathlib's filter-based approach.
Routing
- USE FOR: real analysis, functional analysis, topology, and measure theory in Lean 4 / Mathlib — continuous functions, derivatives, integrals, metric / normed spaces, filter-based convergence, contraction mappings, convex analysis, spectral theory, and the real-valued bridges from a Nat-scaled model.
- DO NOT USE FOR: stochastic / probabilistic convergence (delegate to
@lean-math-stochastic); deterministic dynamical-system stability proofs (delegate to@lean-math-dynamical); pure optimization (delegate to@lean-math-optimization); typeclass-tower reasoning (delegate to@lean-math-foundations); writing one specific proof (delegate to@lean-proof). - TRIGGERS: continuous, derivative, integral, metric space, normed space, filter, convergence, topology, measure space, contraction, Banach.
Workflow
- Map the problem to Mathlib's filter-based architecture (Part 1) — most analysis goals can be phrased as
Tendsto … atToporContinuousAt. - Locate the relevant Part below (continuity, derivatives, integrals, normed spaces, measure theory) and apply the pattern.
- If the result is a concrete proof obligation, handoff to
@lean-proof; if it depends on a foundational instance, handoff to@lean-math-foundations.
Recovery & STOP
- STOP if the lemma you need is not in Mathlib at the current pin — escalate to
@lean-researchto verify, then@lean-proofto author a local helper. - STOP if a classical-only result is invoked and the project has documented constructive constraints — escalate to
@lean-review-council.
Handoffs
- Predecessors:
agent:gateway,skill:lean-proof(mid-proof convergence goal),skill:lean-research(when a survey turns up an analysis API). - Successors:
skill:lean-proof(apply the analysis pattern),skill:lean-proof-review(audit the resulting proof),skill:lean-math-foundations(when the goal collapses to a typeclass-tower issue).
Detailed reference
Full encyclopaedia content (Parts 1 through 8) lives in
references/lean4-math-analysis.md. Load that file
when authoring; the SKILL.md only carries the dispatch contract and
the high-frequency pitfalls / recipes (kept inline below).
| Part | Topic | Covers |
|---|---|---|
| Part 1 | Mathlib's Analysis Architecture | filter-based convergence, topological-space layering |
| Part 2 | Continuity and Limits | Continuous, ContinuousAt, ContinuousOn, Tendsto |
| Part 3 | Differentiation | HasDerivAt, deriv, fderiv, mean-value theorem |
| Part 4 | Metric Spaces and Contraction | MetricSpace, LipschitzWith, ContractingWith, completeness |
| Part 5 | Convex Analysis | ConvexOn, ConvexHull, Jensen's inequality |
| Part 6 | Measure Theory Essentials | MeasureSpace, MeasureTheory.integral, intervalIntegral |
| Part 7 | Research Council Integration | (also kept inline below) — analysis-domain dispatch matrix |
| Part 8 | Host-Repository Analysis Extensions | repository-local Lyapunov / contraction / convex-on-Nat bridges |
Part 8 — Pitfalls
| Pitfall | Symptom | Fix |
|---|---|---|
ℝ vs ℝ≥0 confusion |
Type mismatch on nonneg results | Use .toReal or NNReal.coe_* lemmas |
| Filter direction wrong | atTop vs atBot |
Check: are you going to ∞ or 0? |
Missing CompleteSpace |
Contraction theorem won't apply | Add hypothesis or use instCompleteSpaceReal |
norm vs abs |
‖x‖ vs ` |
x |
| Derivative of composed function | HasDerivAt won't compose automatically |
Use HasDerivAt.comp explicitly |
| Measure vs volume | Wrong default measure | Specify volume or MeasureTheory.MeasureSpace.volume |
Part 9 — Tactic Priority for Analysis Goals
When a goal sits in the analysis family, try these in order before reaching for manual .comp chains:
fun_prop— Mathlib's general property-prover forContinuous,Measurable,Differentiable,StronglyMeasurableon composed functions. Prefer this over manualContinuous.comp/Differentiable.compchains.continuity— older specialised continuity solver; still helpful whenfun_propmisses a Mathlib lemma.measurability— forMeasurable/AEMeasurable/StronglyMeasurablegoals; complementsfun_prop.positivity— for0 < x/0 ≤ xgoals involvingexp,log, norms, integrals; pairs well withgcongrfor inequality chaining.gcongr— generalised congruence; replaces a longMonoOn.*chain for≤between integrals, norms, suprema, etc.bound— newer Mathlib bound-prover; useful whenpositivitycan't close (e.g., requires a hypothesis to bound).norm_num/nlinarith— pure numeric / nonlinear arithmetic; last-resort closers for concrete numeric bounds.
If nothing fires, fall back to explicit apply HasDerivAt.comp, apply Continuous.comp, etc. — but those are last-resort.
Part 10 — Filter-Convergence Escape Hatches
When Tendsto won't simp:
eventually_atToprewrites∀ᶠ n in atTop, P nto∃ N, ∀ n ≥ N, P n— switch when classical existence is easier than filter algebra.Filter.tendsto_atTop_atTop— discretef n → ∞: prove∀ b, ∃ N, ∀ n ≥ N, b ≤ f n.Tendsto.comp— composition of limits; the most common building block.Filter.eventually_iff_exists_mem— convert between∀ᶠand explicit set membership.Metric.tendsto_atTop— for metric-space convergence, use theε / δform directly when filter-arithmetic gets stuck.
When integration limits won't compute:
MeasureTheory.integral_congr_ae— change the integrand on a null set without re-proving integrability.MeasureTheory.intervalIntegral.integral_congr— change of variables on a compact interval.MeasureTheory.lintegral_lt_top_iff_finite_set_of_pos— when proving anlintegralis finite, this often beats direct estimation.
See also
../../references/lean4-math-analysis.md— Real Analysis & Topology Encyclopaedia (full encyclopaedia, extracted from this skill)../../templates/Template_Analysis.md— Template: Real analysis (continuity, Lipschitz, sqrt)../../references/lean4-proof-strategy.md— Proof strategy & error priority../../references/lean4-tactic-hierarchy.md— Tactic priority for analysis goals