2
$\begingroup$

I want to understand Mathlib/MeasureTheory, and in particular I want to understand Mathlib/MeasureTheory/Integral. I'm having difficulty with the notation. I struggle to find the correct file to "start" with when reading a new part of Mathlib, so I typically tend to find something that seems sufficiently basic which I want to learn about and start tracing dependencies. (If anyone has a better way, please help me...) I'm struggling to understand some of the notation I'm finding. For example, go to MeasureTheory/Integral/SetToL1.lean. We find the code

/-- Extend `Set α → E →L[ℝ] F` to `(α →₁ₛ[μ] E) →L[𝕜] F`. -/
def setToL1SCLM' {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C)
    (h_smul : ∀ c : 𝕜, ∀ s x, T s (c • x) = c • T s x) : (α →₁ₛ[μ] E) →L[𝕜] F :=
  LinearMap.mkContinuous
    ⟨⟨setToL1S T, setToL1S_add T (fun _ => hT.eq_zero_of_measure_zero) hT.1⟩,
      setToL1S_smul T (fun _ => hT.eq_zero_of_measure_zero) hT.1 h_smul⟩
    C fun f => norm_setToL1S_le T hT.2 f

Take E →L[ℝ] F, for instance, though I could have chosen quite a few examples. When I hover over it, it calls itself a continuous map between modules, but doesn't give a location in Mathlib to find this explanation. Needless to say

/-- Extend `Set α → E →L[ℝ] F` to `(α →₁ₛ[μ] E) →L[𝕜] F`. -/

means nothing to me right now. Hence: Is there a "nice" path through which to explore Mathlib/MeasureTheory?

$\endgroup$

1 Answer 1

3
$\begingroup$

You could start with reading the relevant chapter of Mathematics in Lean. You can also right click and choose "Go to definition" when you see an unknown notation or definition.

$\endgroup$
1
  • $\begingroup$ Didn't know that existed. Thank you. $\endgroup$
    – Alex Byard
    Sep 24, 2023 at 2:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.