PlaneScalarMildTruncation.lean`

18 declarations, 0 contain sorry, 0 declared as axioms

Compatibility of finite-jet mild solutions under lossless truncation.

def OAI.ForcedComputation.PlaneScalarMild.truncatePath line 14
Source documentation
Truncate every value of a continuous jet path.
```
def truncatePath (k n : ℕ) (hkn : k ≤ n) (T : ℝ) :
    WeaklySingular.Path (Jet n) T →L[ℝ] WeaklySingular.Path (Jet k) T :=
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet
theorem OAI.ForcedComputation.PlaneScalarMild.truncatePath_apply line 20
theorem OAI.ForcedComputation.PlaneScalarMild.extendPath_truncate line 24
theorem OAI.ForcedComputation.PlaneScalarMild.truncatePath_eq_of_functions line 30
Source documentation
Any two jet paths representing the same scalar function agree after truncation.
```
theorem truncatePath_eq_of_functions (k n : ℕ) (hkn : k ≤ n) (T : ℝ)
    (u : WeaklySingular.Path (Jet n) T) (v : WeaklySingular.Path (Jet k) T)
    (h : ∀ t x, BoundedSpatialJets.function Plane ℝ n (u t) x =
      BoundedSpatialJets.function Plane ℝ k (v t) x) :
    truncatePath k n hkn T u = v := by
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.PlaneScalarMild.truncatePath

theorem OAI.ForcedComputation.PlaneScalarMild.coefficient_truncate_of_functions line 46

Source documentation

Representing the same coefficient function forces compatibility of its finite jets.

theorem coefficient_truncate_of_functions (k n : ℕ) (hkn : k ≤ n) (T : ℝ)
    (b : C(Icc (0 : ℝ) T, Jet n)) (c : C(Icc (0 : ℝ) T, Jet k))
    (h : ∀ t x, BoundedSpatialJets.function Plane ℝ n (b t) x =
      BoundedSpatialJets.function Plane ℝ k (c t) x) (t : Icc (0 : ℝ) T) :
    BoundedSpatialJets.truncateCLM Plane ℝ k n hkn (b t) = c t := by
…

Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.BoundedSpatialJets.function, OAI.ForcedComputation.BoundedSpatialJets.truncateCLM

theorem OAI.ForcedComputation.PlaneScalarMild.multiplication_truncate line 58
theorem OAI.ForcedComputation.PlaneScalarMild.rawHeatKernel_truncate line 69
theorem OAI.ForcedComputation.PlaneScalarMild.gradientKernel_truncate line 80
theorem OAI.ForcedComputation.PlaneScalarMild.rawKernels_truncate line 92
theorem OAI.ForcedComputation.PlaneScalarMild.rawKernel_path_integrable line 100
Source documentation
A continuous source path gives Bochner-integrable heat and gradient integrands.
```
theorem rawKernel_path_integrable {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν) (k : ℕ)
    (u : WeaklySingular.Path (Jet k) T)
    (i : Fin 3) (t : Icc (0 : ℝ) T) :
    IntervalIntegrable (fun s => rawKernels hν k i (t.val-s)
      (WeaklySingular.extendPath (Jet k) hT u s)) volume 0 t.val := by
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.PlaneScalarMild.rawKernels, OAI.ForcedComputation.WeaklySingular.extendPath
theorem OAI.ForcedComputation.PlaneScalarMild.mild_integrand_integrable line 137
Source documentation
The actual coefficient/kernel integrands are integrable at the singular endpoint.
```
theorem mild_integrand_integrable {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν) (k : ℕ)
    (b : C(Icc (0 : ℝ) T, Jet k)) (u : WeaklySingular.Path (Jet k) T)
    (i : Fin 3) (t : Icc (0 : ℝ) T) :
    IntervalIntegrable (fun s => rawKernels hν k i (t.val-s)
      (multiplication k (b (projIcc 0 T hT s))
        (WeaklySingular.extendPath (Jet k) hT u s))) volume 0 t.val := by
…
```
Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.rawKernels, OAI.ForcedComputation.PlaneScalarMild.multiplication, OAI.ForcedComputation.WeaklySingular.extendPath
theorem OAI.ForcedComputation.PlaneScalarMild.map_integral_eq line 151
theorem OAI.ForcedComputation.PlaneScalarMild.map_add_finite_sum line 158

theorem OAI.ForcedComputation.PlaneScalarMild.rawKernelIntegral_truncate line 166

Source documentation

Truncation commutes with the actual unweighted heat and gradient integrals.

theorem rawKernelIntegral_truncate {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k n : ℕ) (hkn : k ≤ n) (u : WeaklySingular.Path (Jet n) T)
    (i : Fin 3) (t : Icc (0 : ℝ) T) :
    BoundedSpatialJets.truncateCLM Plane ℝ k n hkn
      (∫ s in 0..t.val, rawKernels hν n i (t.val-s)
        (WeaklySingular.extendPath (Jet n) hT u s)) =
      ∫ s in 0..t.val, rawKernels hν k i (t.val-s)
        (WeaklySingular.extendPath (Jet k) hT (truncatePath k n hkn T u) s) := by
…

Mentions: OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.BoundedSpatialJets.truncateCLM, OAI.ForcedComputation.PlaneScalarMild.rawKernels, OAI.ForcedComputation.WeaklySingular.extendPath, OAI.ForcedComputation.PlaneScalarMild.truncatePath

theorem OAI.ForcedComputation.PlaneScalarMild.truncate_integrand line 181
theorem OAI.ForcedComputation.PlaneScalarMild.truncate_integral_term line 199

theorem OAI.ForcedComputation.PlaneScalarMild.truncate_mild_equation line 217

Source documentation

A high-order solution truncates to the low-order equation with truncated data.

theorem truncate_mild_equation {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k n : ℕ) (hkn : k ≤ n)
    (b : Fin 3 → C(Icc (0 : ℝ) T, Jet n))
    (c : Fin 3 → C(Icc (0 : ℝ) T, Jet k))
    (hbc : ∀ i t, BoundedSpatialJets.truncateCLM Plane ℝ k n hkn (b i t) = c i t)
    (a u : WeaklySingular.Path (Jet n) T)
    (hu : ∀ t : Icc (0 : ℝ) T, u t = a t +
      ∑ i, ∫ s in 0..t.val, rawKernels hν n i (t.val-s)
        (multiplication n (b i (projIcc 0 T hT s))
          (WeaklySingular.extendPath (Jet n) hT u s))) :
    ∀ t : Icc (0 : ℝ) T, truncatePath k n hkn T u t = truncatePath k n hkn T a t +
      ∑ i, ∫ s in 0..t.val, rawKernels hν k i (t.val-s)
…

Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.BoundedSpatialJets.truncateCLM, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.rawKernels, OAI.ForcedComputation.PlaneScalarMild.multiplication, OAI.ForcedComputation.WeaklySingular.extendPath, OAI.ForcedComputation.PlaneScalarMild.truncatePath

theorem OAI.ForcedComputation.PlaneScalarMild.mild_solutions_compatible line 248

Source documentation

Uniqueness identifies solutions at different jet orders, independently of the chosen weight.

theorem mild_solutions_compatible {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k n : ℕ) (hkn : k ≤ n)
    (b : Fin 3 → C(Icc (0 : ℝ) T, Jet n))
    (c : Fin 3 → C(Icc (0 : ℝ) T, Jet k))
    (hbc : ∀ i t, BoundedSpatialJets.truncateCLM Plane ℝ k n hkn (b i t) = c i t)
    (a u : WeaklySingular.Path (Jet n) T) (v : WeaklySingular.Path (Jet k) T)
    (hu : ∀ t : Icc (0 : ℝ) T, u t = a t +
      ∑ i, ∫ s in 0..t.val, rawKernels hν n i (t.val-s)
        (multiplication n (b i (projIcc 0 T hT s))
          (WeaklySingular.extendPath (Jet n) hT u s)))
    (hv : ∀ t : Icc (0 : ℝ) T, v t = truncatePath k n hkn T a t +
      ∑ i, ∫ s in 0..t.val, rawKernels hν k i (t.val-s)
…