Toby Cathcart Burn

Stream: new members

[Toby Cathcart Burn]

Hi, I'm Toby. I have an undergraduate degree in Maths & Comp Sci and I've studied some aspects of logic and type systems as a Computer Science graduate student.
I'm trying to formalize a proof of correctness for a calculation of the area of the Pythagoras tree https://penteract.github.io/pythagTree.html, mostly for the purpose of learning lean.

[Toby Cathcart Burn]

I'm currently struggling to find a result in Mathlib which says that affine maps on ℝ×ℝ preserve measurability of sets. Formally:

theorem affine_Measurable (f : (ℝ × ℝ) →ᵃ[ℝ] (ℝ × ℝ)) {s : Set (ℝ×ℝ)} (h : MeasurableSet s ) : MeasurableSet (f '' s) := by
  sorry

Alternatively, I could use a proof that Lebesgue measurable sets satisfy Carathéodory's criterion:

theorem R2Caratheodory {s : Set (ℝ×ℝ) } {t : Set (ℝ×ℝ) } (h : MeasurableSet s) :
    MeasureTheory.volume s = MeasureTheory.volume (t ∩ s) + MeasureTheory.volume (t \ s) := by
  sorry

As far as I can tell, this theorem is true, and the framework for it is in Mathlib (https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/OuterMeasure/Caratheodory.html), but I can't find a theorem in Mathlib linking Carathéodory's criterion with the Lebesgue measure on ℝ. I haven't studied measure theory, so I might be missing something.

[Toby Cathcart Burn]

I've also heard that lean can have problems with large computations. The calculation involves a system of around 8000 linear equations of the form 4a=b+c+d+e. The system can be reduced in size by a factor of 8 if you account for symmetries. Is it practical to verify a solution to such a system in lean when the solution involves rational numbers which have up to 110 digits in numerator and denominator?

[Aaron Liu]

It's probably doable, though it might take a few minutes.