Documentation

LeanPool.AnomalousDiffusion.AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath

Recovering an integral path from the scalar weak time equation #

Separated tests against a fixed spatial Fourier mode give a scalar distributional equation. Subtracting the forcing primitive turns it into zero pairing against all compactly supported interior tests, where the distribution separation lemma applies.

source
noncomputable def AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath.terminalPrimitive (g : ℝ → ℝ) (t : ℝ) :
ℝ

A smooth compactly supported interior function has a smooth terminal primitive.

Equations
Instances For
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath.terminalPrimitive_hasDerivAt {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (t : ℝ) :
    HasDerivAt (terminalPrimitive g) (-g t) t
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath.terminalPrimitive_deriv {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) :
    deriv (terminalPrimitive g) = fun (t : ℝ) => -g t
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath.terminalPrimitive_contDiff {g : ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) :
    ContDiff ℝ (↑⊤) (terminalPrimitive g)
    source
    theorem AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath.terminalPrimitive_zero_of_ge_one {g : ℝ → ℝ} (hgSupport : tsupport g ⊆ Set.Ioo 0 1) (t : ℝ) (ht : 1 ≤ t) :
    terminalPrimitive g t = 0
    source
    def AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath.clampUnitTime (t : ℝ) :
    ℝ

    Clamp real time to the closed unit interval for a weak scalar path.

    Equations
    Instances For
      source
      theorem AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath.clampUnitTime_continuous :
      Continuous clampUnitTime
      source
      theorem AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath.clampUnitTime_mem (t : ℝ) :
      clampUnitTime t ∈ Set.Icc 0 1
      source
      theorem AVenhance.Infra.Parabolic.WeakUniqueness.ScalarPath.clampUnitTime_eq {t : ℝ} (ht : t ∈ Set.Icc 0 1) :
      clampUnitTime t = t
      source
      theorem AVenhance.Infra.Parabolic.WeakUniqueness.scalar_weak_tests_imply_integral_path {u q : ℝ → ℝ} {u₀ : ℝ} (hu : ContinuousOn u (Set.Icc 0 1)) (hq : IntervalIntegrable q MeasureTheory.volume 0 1) (hweak : ∀ (η : ℝ → ℝ), ContDiff ℝ (↑⊤) η → (∀ (t : ℝ), 1 ≤ t → η t = 0) → ∫ (t : ℝ) in 0..1, -u t * deriv η t + q t * η t = u₀ * η 0) (t : ℝ) :
      t ∈ Set.Icc 0 1 → u t = u₀ - ∫ (s : ℝ) in 0..t, q s

      A scalar weak time equation with integrable forcing has the corresponding absolutely continuous integral path.