The function ψ
Equations
- ShortVariables.termψ = Lean.ParserDescr.node `ShortVariables.termψ 1024 (Lean.ParserDescr.symbol "ψ")
Instances For
theorem
DoublingMeasure.volume_ball_two_le_same_repeat
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
(x : X)
(r : ℝ)
(n : ℕ)
:
MeasureTheory.volume.real (Metric.ball x (2 ^ n * r)) ≤ ↑(defaultA a) ^ n * MeasureTheory.volume.real (Metric.ball x r)
Apply volume_ball_two_le_same
n
times.
theorem
integrable_Ks_x
{X : Type u_1}
{a : ℕ}
{q : ℝ}
{K : X → X → ℂ}
{σ₁ : X → ℤ}
{σ₂ : X → ℤ}
{F : Set X}
{G : Set X}
[PseudoMetricSpace X]
[ProofData a q K σ₁ σ₂ F G]
{s : ℤ}
{x : X}
(hD : 1 < ↑(defaultD a))
:
MeasureTheory.Integrable (Ks s x) MeasureTheory.volume
The function y ↦ Ks s x y
is integrable.