WeaklySingularWeighted.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Integrable majorants and exponential damping of weakly singular Volterra operators.

theorem OAI.ForcedComputation.WeaklySingular.norm_integralOperator_le_integral line 17

Source documentation

Any integrable nonnegative kernel majorant bounds the path operator norm.

theorem norm_integralOperator_le_integral {T : ℝ} (hT : 0 ≤ T)
    (K : ℝ → E →L[ℝ] E) (hK : ContinuousOn K (Ioi 0))
    (C : ℝ) (hC : 0 ≤ C) (hbound : ∀ r, 0 ≤ r → ‖K r‖ ≤ C * inverseSqrt r)
    (b : ℝ → ℝ) (hbi : IntervalIntegrable b volume 0 T)
    (hb : ∀ r ∈ Icc 0 T, 0 ≤ b r) (hKb : ∀ r ∈ Icc 0 T, ‖K r‖ ≤ b r) :
    ‖integralOperator E hT K hK C hC hbound‖ ≤ ∫ r in 0..T, b r := by
…

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

def OAI.ForcedComputation.WeaklySingular.weightedProfile line 52
Source documentation
The scalar majorant after exponential time weighting.
```
def weightedProfile (rate r : ℝ) : ℝ := Real.exp (-rate * r) * inverseSqrt r
```
Mentions: OAI.ForcedComputation.WeaklySingular.inverseSqrt
theorem OAI.ForcedComputation.WeaklySingular.weightedProfile_nonneg line 54
theorem OAI.ForcedComputation.WeaklySingular.weightedProfile_integrable line 57
theorem OAI.ForcedComputation.WeaklySingular.weightedProfile_le line 62
theorem OAI.ForcedComputation.WeaklySingular.weightedProfile_integral_tendsto line 70
Source documentation
On every finite interval the exponentially weighted singular mass tends to zero.
```
theorem weightedProfile_integral_tendsto {T : ℝ} (hT : 0 ≤ T) :
    Tendsto (fun rate : ℝ => ∫ r in 0..T, weightedProfile rate r) atTop (𝓝 0) := by
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.weightedProfile
def OAI.ForcedComputation.WeaklySingular.weightedKernel line 94
Source documentation
Exponential conjugation changes only the time kernel.
```
def weightedKernel (rate : ℝ) (K : ℝ → E →L[ℝ] E) (r : ℝ) : E →L[ℝ] E :=
…
```
theorem OAI.ForcedComputation.WeaklySingular.weightedKernel_continuous line 97
theorem OAI.ForcedComputation.WeaklySingular.weightedKernel_bound line 101
theorem OAI.ForcedComputation.WeaklySingular.norm_weightedIntegralOperator_le line 113
theorem OAI.ForcedComputation.WeaklySingular.exists_weightedIntegralOperator_norm_lt line 132
Source documentation
Weighting makes the Volterra operator arbitrarily small without shortening the interval.
```
theorem exists_weightedIntegralOperator_norm_lt {T C : ℝ} (hT : 0 ≤ T)
    (K : ℝ → E →L[ℝ] E) (hK : ContinuousOn K (Ioi 0)) (hC : 0 ≤ C)
    (hbound : ∀ r, 0 ≤ r → ‖K r‖ ≤ C * inverseSqrt r) {q : ℝ} (hq : 0 < q) :
    ∃ rate : ℝ, ∃ hrate : 0 ≤ rate,
      ‖integralOperator E hT (weightedKernel E rate K) (weightedKernel_continuous E rate K hK)
        C hC (weightedKernel_bound E hrate hC K hbound)‖ < q := by
…
```
Mentions: OAI.ForcedComputation.WeaklySingular.inverseSqrt, OAI.ForcedComputation.WeaklySingular.integralOperator, OAI.ForcedComputation.WeaklySingular.weightedKernel, OAI.ForcedComputation.WeaklySingular.weightedKernel_continuous, OAI.ForcedComputation.WeaklySingular.weightedKernel_bound