OAI/MathematicalPhysics/NavierStokes/ForcedComputation/Scalar/PlaneScalarMildPeriodicity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Spatial periodicity of the actual scalar mild solution, by translation and uniqueness.

  1. def OAI.ForcedComputation.PlaneScalarMild.translationPath line 14
  2. theorem OAI.ForcedComputation.PlaneScalarMild.translationPath_apply line 20
  3. theorem OAI.ForcedComputation.PlaneScalarMild.extendPath_translation line 24
  4. theorem OAI.ForcedComputation.PlaneScalarMild.multiplication_translation line 29
  5. theorem OAI.ForcedComputation.PlaneScalarMild.rawHeatKernel_translation line 39
  6. theorem OAI.ForcedComputation.PlaneScalarMild.gradientKernel_translation line 49
  7. theorem OAI.ForcedComputation.PlaneScalarMild.rawKernels_translation line 60
  8. theorem OAI.ForcedComputation.PlaneScalarMild.evolutionOperator_translation line 67
  9. theorem OAI.ForcedComputation.PlaneScalarMild.translate_mild_integrand line 76
  10. theorem OAI.ForcedComputation.PlaneScalarMild.translate_mild_integral line 91
  11. theorem OAI.ForcedComputation.PlaneScalarMild.map_add_sum line 105
  12. theorem OAI.ForcedComputation.PlaneScalarMild.mildSolution_translation line 111

    Source documentation

    A translation preserving the data also preserves the unique mild solution.

    theorem mildSolution_translation {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (k : ℕ) (a : Plane) (b : Fin 3 → C(Icc (0 : ℝ) T, Jet k))
    (hb : ∀ i t, BoundedSpatialJets.translationCLM Plane ℝ k a (b i t) = b i t)
    (g : WeaklySingular.Path (Jet k) T)
    (hg : ∀ t, BoundedSpatialJets.translationCLM Plane ℝ k a (g t) = g t) :
    translationPath k a T (mildSolution hT hν k b g) = mildSolution hT hν k b g := by
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.Jet, OAI.ForcedComputation.BoundedSpatialJets.translationCLM, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.PlaneScalarMild.translationPath, OAI.ForcedComputation.PlaneScalarMild.mildSolution

  13. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.affinePath_translation line 129
  14. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solution_periodic line 163

    Source documentation

    Periodicity is inherited by the actual compatible mild solution, not merely its data.

    theorem solution_periodic {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν) (D : CompatibleData T)
    (hI : ∀ k, PlanePeriodic (BoundedSpatialJets.function Plane ℝ k (D.initial k)))
    (hg : ∀ k t, PlanePeriodic (BoundedSpatialJets.function Plane ℝ k (D.source k t)))
    (hb : ∀ k i t, PlanePeriodic (BoundedSpatialJets.function Plane ℝ k (D.coefficient k i t)))
    (t : Icc (0 : ℝ) T) : PlanePeriodic (D.solution hT hν t) := by
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.PlanePeriodic, OAI.ForcedComputation.BoundedSpatialJets.function

  15. theorem OAI.ForcedComputation.PlaneScalarMild.CompatibleData.solution_periodic_of_representatives line 189

    Source documentation

    Actual periodic field representations supply all translation-invariance hypotheses.

    theorem solution_periodic_of_representatives {T ν : ℝ} (hT : 0 ≤ T) (hν : 0 < ν)
    (D : CompatibleData T) {w₀ : Plane → ℝ} (hpw : PlanePeriodic w₀)
    {h : ℝ × Plane → ℝ} (hph : ∀ t, PlanePeriodic (fun x => h (t,x)))
    {b : Fin 3 → ℝ × Plane → ℝ} (hpb : ∀ i t, PlanePeriodic (fun x => b i (t,x)))
    (hinit : ∀ k x, BoundedSpatialJets.function Plane ℝ k (D.initial k) x = w₀ x)
    (hsource : ∀ k t x, BoundedSpatialJets.function Plane ℝ k (D.source k t) x = h (t.val,x))
    (hcoeff : ∀ k i t x, BoundedSpatialJets.function Plane ℝ k (D.coefficient k i t) x = b i (t.val,x))
    (t : Icc (0 : ℝ) T) : PlanePeriodic (D.solution hT hν t) := by
…

    Mentions: OAI.ForcedComputation.PlaneScalarMild.CompatibleData, OAI.ForcedComputation.PlanePeriodic, OAI.ForcedComputation.BoundedSpatialJets.function