`BookProof.ChapterU.differentiable_trajectory_null` {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P] (path : Ω → ℝ → ℝ) (hext : ∀ᵐ ω ∂P, ∀ t, ¬...

Proved

BookProof.ChapterU.differentiable_trajectory_null

by leonardopedro · Oct 10, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterU.

BookProof.ChapterU.differentiable_trajectory_null {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P] (path : Ω → ℝ → ℝ) (hext : ∀ᵐ ω ∂P, ∀ t, ¬ DifferentiableAt ℝ (path ω) t) : P {ω | ∃ t, DifferentiableAt ℝ (path ω) t} = 0

Formalization note: Lean 4 identifier BookProof.ChapterU.differentiable_trajectory_null.

Preamble

-- Generated from ChapterU.lean — theorem BookProof.ChapterU.differentiable_trajectory_null
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.differentiable_trajectory_null {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    [IsProbabilityMeasure P] (path : Ω → ℝ → ℝ)
    (hext : ∀ᵐ ω ∂P, ∀ t, ¬ DifferentiableAt ℝ (path ω) t) :
    P {ω | ∃ t, DifferentiableAt ℝ (path ω) t} = 0 := by sorry

View graph