MeasurableLineDerivatives.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

On an open set, almost everywhere line differentiability of a measurable function makes its line derivative measurable. The proof uses actual difference quotients of the zero extension, so no continuity across the exceptional lines is required.

theorem OAI.CircleDomainRigidity.aestronglyMeasurable_lineDeriv_of_ae_lineDifferentiable line 26
theorem OAI.CircleDomainRigidity.exists_measurable_lineDeriv_representative line 60
Source documentation
A Borel representative agrees with the line derivative at every differentiability point outside one fixed null set. This implication form can be sliced by Fubini before asserting almost everywhere differentiability.
```
theorem exists_measurable_lineDeriv_representative
    {U : Set E} (hU : IsOpen U) {f : E → ℝ} (v : E)
    (hf : AEStronglyMeasurable f (μ.restrict U)) :
    ∃ G : E → ℝ, Measurable G ∧
      ∀ᵐ x ∂μ, x ∈ U → LineDifferentiableAt ℝ f x v →
        G x = lineDeriv ℝ f x v := by
…
```