`BookProof.ChapterU.no_differentiable_trajectory` {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P] (path : Ω → ℝ → ℝ) (hext : ∀ᵐ ω ∂P, ∀ t, ¬...
ProvedBookProof.ChapterU.no_differentiable_trajectorytheoremstimepiece
Prove the following Lean 4 theorem from ChapterU.
BookProof.ChapterU.no_differentiable_trajectory {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P] (path : Ω → ℝ → ℝ) (hext : ∀ᵐ ω ∂P, ∀ t, ¬ DifferentiableAt ℝ (path ω) t) : P {ω | ∃ t, DifferentiableAt ℝ (path ω) t}ᶜ = 1
Formalization note: Lean 4 identifier BookProof.ChapterU.no_differentiable_trajectory.
Preamble
-- Generated from ChapterU.lean — theorem BookProof.ChapterU.no_differentiable_trajectory
import Mathlib
import Definitions.Def_ChapterU
open BookProof.ChapterU
open MeasureTheory
open scoped ENNReal ProbabilityTheory TensorProduct
variable {X : Type*} [MeasurableSpace X]
variable (R M N : Type*) [CommRing R] [AddCommGroup M] [Module R M]
[AddCommGroup N] [Module R N]Formal statement
theorem BookProof.ChapterU.no_differentiable_trajectory {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
[IsProbabilityMeasure P] (path : Ω → ℝ → ℝ)
(hext : ∀ᵐ ω ∂P, ∀ t, ¬ DifferentiableAt ℝ (path ω) t) :
P {ω | ∃ t, DifferentiableAt ℝ (path ω) t}ᶜ = 1 := by sorry