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

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ForcedComputation.WeaklySingular.coefficientOperator line 17

   Source documentation

   Pointwise action of a continuous coefficient on a continuous path.

   def coefficientOperator {T : ℝ} (A : C(Icc (0 : ℝ) T, E →L[ℝ] E)) :
       Path E T →L[ℝ] Path E T :=
   …

   Mentions: OAI.ForcedComputation.WeaklySingular.Path

2. theorem OAI.ForcedComputation.WeaklySingular.coefficientOperator_apply line 41
3. theorem OAI.ForcedComputation.WeaklySingular.norm_coefficientOperator_le line 45
4. def OAI.ForcedComputation.WeaklySingular.weightOperator line 57

   Source documentation

   Multiplication by an exponential scalar weight on the time interval.

   def weightOperator (T rate : ℝ) : Path E T →L[ℝ] Path E T :=
   …

   Mentions: OAI.ForcedComputation.WeaklySingular.Path

5. theorem OAI.ForcedComputation.WeaklySingular.weightOperator_apply line 63
6. theorem OAI.ForcedComputation.WeaklySingular.weightOperator_inverse line 66
7. theorem OAI.ForcedComputation.WeaklySingular.weightOperator_injective line 74
8. def OAI.ForcedComputation.WeaklySingular.familyOperator line 82

   Source documentation

   A finite sum of genuine Volterra integrals with continuous coefficient paths.

   def familyOperator {T : ℝ} (hT : 0 ≤ T)
       (K : ι → ℝ → E →L[ℝ] E) (hK : ∀ i, ContinuousOn (K i) (Ioi 0))
       (C : ι → ℝ) (hC : ∀ i, 0 ≤ C i)
       (hbound : ∀ i r, 0 ≤ r → ‖K i r‖ ≤ C i * inverseSqrt r)
       (A : ι → C(Icc (0 : ℝ) T, E →L[ℝ] E)) (rate : ℝ) (hrate : 0 ≤ rate) :
       Path E T →L[ℝ] Path E T :=
   …

   Mentions: OAI.ForcedComputation.WeaklySingular.inverseSqrt, OAI.ForcedComputation.WeaklySingular.Path

9. theorem OAI.ForcedComputation.WeaklySingular.familyOperator_apply line 92
10. theorem OAI.ForcedComputation.WeaklySingular.familyOperator_zero_apply line 111
11. theorem OAI.ForcedComputation.WeaklySingular.norm_familyOperator_le line 122
12. theorem OAI.ForcedComputation.WeaklySingular.exists_familyOperator_contraction line 141
13. theorem OAI.ForcedComputation.WeaklySingular.weight_familyOperator line 155
14. theorem OAI.ForcedComputation.WeaklySingular.exists_unique_family_equation line 185

    Source documentation

    A finite family of weakly singular kernels has a unique continuous solution on any finite slab.

    theorem exists_unique_family_equation {T : ℝ} (hT : 0 ≤ T)
        (K : ι → ℝ → E →L[ℝ] E) (hK : ∀ i, ContinuousOn (K i) (Ioi 0))
        (C : ι → ℝ) (hC : ∀ i, 0 ≤ C i)
        (hbound : ∀ i r, 0 ≤ r → ‖K i r‖ ≤ C i * inverseSqrt r)
        (A : ι → C(Icc (0 : ℝ) T, E →L[ℝ] E)) (a : Path E T) :
        ∃! u : Path E T, u = a + familyOperator E hT K hK C hC hbound A 0 le_rfl u := by
    …

    Mentions: OAI.ForcedComputation.WeaklySingular.inverseSqrt, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.WeaklySingular.familyOperator

15. theorem OAI.ForcedComputation.WeaklySingular.exists_unique_integral_equation line 213

    Source documentation

    Pointwise form of the unique equation, with the actual finite sum of time integrals.

    theorem exists_unique_integral_equation {T : ℝ} (hT : 0 ≤ T)
        (K : ι → ℝ → E →L[ℝ] E) (hK : ∀ i, ContinuousOn (K i) (Ioi 0))
        (C : ι → ℝ) (hC : ∀ i, 0 ≤ C i)
        (hbound : ∀ i r, 0 ≤ r → ‖K i r‖ ≤ C i * inverseSqrt r)
        (A : ι → C(Icc (0 : ℝ) T, E →L[ℝ] E)) (a : Path E T) :
        ∃! u : Path E T, ∀ t : Icc (0 : ℝ) T, u t = a t +
          ∑ i, ∫ s in 0..t.val,
            K i (t.val-s) (A i (projIcc 0 T hT s) (extendPath E hT u s)) := by
    …

    Mentions: OAI.ForcedComputation.WeaklySingular.inverseSqrt, OAI.ForcedComputation.WeaklySingular.Path, OAI.ForcedComputation.WeaklySingular.extendPath