Imports
Position operators
i. Overview
In this module we introduce several position operators for quantum mechanics on Space d.
ii. Key results
Definitions:
positionCLM : (components of) the position vector operator acting on Schwartz maps
𝓢(Space d, ℂ) by multiplication by xᵢ.
radiusRegPowCLM : operator acting on Schwartz maps by multiplication by
(‖x‖² + ε²)^(s/2), a smooth regularization of ‖x‖ˢ.
positionOperator : a self-adjoint multiplication operator acting on SpaceDHilbertSpace d.
readiusRegPowOperator : a self-adjoint multiplication operator acting on SpaceDHilbertSpace d.
Notation:
𝐱 for positionCLM
𝐫₀ for radiusRegPowCLM
𝐫 for radiusPowLM
iii. Table of contents
iv. References
@[ expose ] public section
A. Schwartz operators
A.1. Position vector
Component i of the position operator is the continuous linear map
from 𝓢(Space d, ℂ) to itself which maps ψ to xᵢψ.
def positionCLM : 𝓢( Space d , ℂ ) →L[ ℂ ] 𝓢( Space d , ℂ ) :=
SchwartzMap.smulLeftCLM ℂ ( Complex.ofRealCLM ∘L coordCLM i )
A.2. Radius powers (regularized)
The radius operator to power s, regularized by ε ≠ 0, is the continuous linear map
from 𝓢(Space d, ℂ) to itself which maps ψ to (‖x‖² + ε²)^(s/2) • ψ.
def radiusRegPowCLM { d : ℕ } ( ε : ℝ ˣ ) ( s : ℝ ) : 𝓢( Space d , ℂ ) →L[ ℂ ] 𝓢( Space d , ℂ ) :=
SchwartzMap.smulLeftCLM ℂ ( Complex.ofReal ∘ normRegularizedPow d ε s )
@[ inherit_doc radiusRegPowCLM ]
notation "𝐫₀" => radiusRegPowCLM @[ inherit_doc radiusRegPowCLM ]
notation "𝐫₀[" d' "]" => radiusRegPowCLM ( d := d' ) lemma radiusRegPowCLM_apply_fun { d : ℕ } ( ε : ℝ ˣ ) ( s : ℝ ) ( ψ : 𝓢( Space d , ℂ ) ) :
𝐫₀ ε s ψ = fun x ↦ ( ‖ x ‖ ^ 2 + ε ^ 2 ) ^ ( s / 2 ) • ψ x := by d : ℕ ε : ℝ ˣ s : ℝ ψ : 𝓢( Space d , ℂ ) ⊢ ⇑ ( ( 𝐫₀ ε s ) ψ ) = fun x => ( ‖ x ‖ ^ 2 + ↑ ε ^ 2 ) ^ ( s / 2 ) • ψ x
ext x d : ℕ ε : ℝ ˣ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d ⊢ ( ( 𝐫₀ ε s ) ψ ) x = ( ‖ x ‖ ^ 2 + ↑ ε ^ 2 ) ^ ( s / 2 ) • ψ x
dsimp [ radiusRegPowCLM ] d : ℕ ε : ℝ ˣ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d ⊢ ( ( smulLeftCLM ℂ ( Complex.ofReal ∘ normRegularizedPow d (↑ ε ) s ) ) ψ ) x = ↑ ( ( ‖ x ‖ ^ 2 + ↑ ε ^ 2 ) ^ ( s / 2 ) ) * ψ x
refine smulLeftCLM_apply_apply ? _ ψ x d : ℕ ε : ℝ ˣ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d ⊢ HasTemperateGrowth ( Complex.ofReal ∘ normRegularizedPow d (↑ ε ) s )
exact HasTemperateGrowth.comp ( by d : ℕ ε : ℝ ˣ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d ⊢ HasTemperateGrowth Complex.ofReal fun_prop All goals completed! 🐙 ) ( normRegularizedPow_hasTemperateGrowth d ε s )
@[ simp ]
lemma radiusRegPowCLM_apply { d : ℕ } ( ε : ℝ ˣ ) ( s : ℝ ) ( ψ : 𝓢( Space d , ℂ ) ) ( x : Space d ) :
𝐫₀ ε s ψ x = ( ‖ x ‖ ^ 2 + ε ^ 2 ) ^ ( s / 2 ) • ψ x := by d : ℕ ε : ℝ ˣ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d ⊢ ( ( 𝐫₀ ε s ) ψ ) x = ( ‖ x ‖ ^ 2 + ↑ ε ^ 2 ) ^ ( s / 2 ) • ψ x
rw [ radiusRegPowCLM_apply_fun d : ℕ ε : ℝ ˣ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d ⊢ (fun x => ( ‖ x ‖ ^ 2 + ↑ ε ^ 2 ) ^ ( s / 2 ) • ψ x ) x = ( ‖ x ‖ ^ 2 + ↑ ε ^ 2 ) ^ ( s / 2 ) • ψ x All goals completed! 🐙 ] All goals completed! 🐙 @[ simp ]
lemma radiusRegPowCLM_comp_eq { d : ℕ } ( ε : ℝ ˣ ) ( s t : ℝ ) :
𝐫₀[ d ] ε s ∘L 𝐫₀ ε t = 𝐫₀ ε ( s + t ) := by d : ℕ ε : ℝ ˣ s : ℝ t : ℝ ⊢ 𝐫₀ ε s ∘SL 𝐫₀ ε t = 𝐫₀ ε ( s + t )
ext ψ x d : ℕ ε : ℝ ˣ s : ℝ t : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d ⊢ ( ( 𝐫₀ ε s ∘SL 𝐫₀ ε t ) ψ ) x = ( ( 𝐫₀ ε ( s + t ) ) ψ ) x
simp [ add_div , Real.rpow_add ( norm_sq_add_unit_sq_pos ε x ) , mul_assoc ] All goals completed! 🐙 @[ simp ]
lemma radiusRegPowCLM_zero { d : ℕ } ( ε : ℝ ˣ ) :
𝐫₀ ε 0 = ContinuousLinearMap.id ℂ 𝓢( Space d , ℂ ) := by d : ℕ ε : ℝ ˣ ⊢ 𝐫₀ ε 0 = ContinuousLinearMap.id ℂ 𝓢( Space d , ℂ )
ext d : ℕ ε : ℝ ˣ x✝¹ : 𝓢( Space d , ℂ ) x✝ : Space d ⊢ ( ( 𝐫₀ ε 0 ) x✝¹ ) x✝ = ( ( ContinuousLinearMap.id ℂ 𝓢( Space d , ℂ ) ) x✝¹ ) x✝
simp All goals completed! 🐙 lemma positionSqCLM_eq { d : ℕ } ( ε : ℝ ˣ ) :
∑ i , 𝐱 i ∘L 𝐱 i = 𝐫₀ ε 2 - ε . 1 ^ 2 • ContinuousLinearMap.id ℂ 𝓢( Space d , ℂ ) := by d : ℕ ε : ℝ ˣ ⊢ ∑ i , 𝐱 i ∘SL 𝐱 i = 𝐫₀ ε 2 - ↑ ε ^ 2 • ContinuousLinearMap.id ℂ 𝓢( Space d , ℂ )
ext d : ℕ ε : ℝ ˣ x✝¹ : 𝓢( Space d , ℂ ) x✝ : Space d ⊢ ( (∑ i , 𝐱 i ∘SL 𝐱 i ) x✝¹ ) x✝ = ( ( 𝐫₀ ε 2 - ↑ ε ^ 2 • ContinuousLinearMap.id ℂ 𝓢( Space d , ℂ ) ) x✝¹ ) x✝
simp [ Space.norm_sq_eq , add_mul , ← mul_assoc , ← pow_two , Finset.sum_mul ] All goals completed! 🐙
A.3. Radius powers
The radius operator to power s is the linear map from 𝓢(Space d, ℂ) to Space d → ℂ that
maps ψ to x ↦ ‖x‖ˢψ(x) (which is 'nearly' Schwartz for general s).
def radiusPowLM { d : ℕ } ( s : ℝ ) : 𝓢( Space d , ℂ ) →ₗ[ ℂ ] Space d → ℂ where
toFun ψ := ( fun x : Space d ↦ ‖ x ‖ ^ s ) • ψ
map_add' _ _ := by d✝ : ℕ μ : Measure ( Space d✝ ) i : Fin d✝ d : ℕ s : ℝ x✝¹ : 𝓢( Space d , ℂ ) x✝ : 𝓢( Space d , ℂ ) ⊢ (fun x => ‖ x ‖ ^ s ) • ⇑ ( x✝¹ + x✝ ) = (fun x => ‖ x ‖ ^ s ) • ⇑ x✝¹ + (fun x => ‖ x ‖ ^ s ) • ⇑ x✝ rw [ ← smul_add d✝ : ℕ μ : Measure ( Space d✝ ) i : Fin d✝ d : ℕ s : ℝ x✝¹ : 𝓢( Space d , ℂ ) x✝ : 𝓢( Space d , ℂ ) ⊢ (fun x => ‖ x ‖ ^ s ) • ⇑ ( x✝¹ + x✝ ) = (fun x => ‖ x ‖ ^ s ) • ( ⇑ x✝¹ + ⇑ x✝ ) d✝ : ℕ μ : Measure ( Space d✝ ) i : Fin d✝ d : ℕ s : ℝ x✝¹ : 𝓢( Space d , ℂ ) x✝ : 𝓢( Space d , ℂ ) ⊢ (fun x => ‖ x ‖ ^ s ) • ⇑ ( x✝¹ + x✝ ) = (fun x => ‖ x ‖ ^ s ) • ( ⇑ x✝¹ + ⇑ x✝ ) ] d✝ : ℕ μ : Measure ( Space d✝ ) i : Fin d✝ d : ℕ s : ℝ x✝¹ : 𝓢( Space d , ℂ ) x✝ : 𝓢( Space d , ℂ ) ⊢ (fun x => ‖ x ‖ ^ s ) • ⇑ ( x✝¹ + x✝ ) = (fun x => ‖ x ‖ ^ s ) • ( ⇑ x✝¹ + ⇑ x✝ ) ; rfl All goals completed! 🐙
map_smul' _ _ := by d✝ : ℕ μ : Measure ( Space d✝ ) i : Fin d✝ d : ℕ s : ℝ x✝¹ : ℂ x✝ : 𝓢( Space d , ℂ ) ⊢ (fun x => ‖ x ‖ ^ s ) • ⇑ ( x✝¹ • x✝ ) = ( RingHom.id ℂ ) x✝¹ • (fun x => ‖ x ‖ ^ s ) • ⇑ x✝ rw [ smul_comm d✝ : ℕ μ : Measure ( Space d✝ ) i : Fin d✝ d : ℕ s : ℝ x✝¹ : ℂ x✝ : 𝓢( Space d , ℂ ) ⊢ (fun x => ‖ x ‖ ^ s ) • ⇑ ( x✝¹ • x✝ ) = (fun x => ‖ x ‖ ^ s ) • ( RingHom.id ℂ ) x✝¹ • ⇑ x✝ d✝ : ℕ μ : Measure ( Space d✝ ) i : Fin d✝ d : ℕ s : ℝ x✝¹ : ℂ x✝ : 𝓢( Space d , ℂ ) ⊢ (fun x => ‖ x ‖ ^ s ) • ⇑ ( x✝¹ • x✝ ) = (fun x => ‖ x ‖ ^ s ) • ( RingHom.id ℂ ) x✝¹ • ⇑ x✝ ] d✝ : ℕ μ : Measure ( Space d✝ ) i : Fin d✝ d : ℕ s : ℝ x✝¹ : ℂ x✝ : 𝓢( Space d , ℂ ) ⊢ (fun x => ‖ x ‖ ^ s ) • ⇑ ( x✝¹ • x✝ ) = (fun x => ‖ x ‖ ^ s ) • ( RingHom.id ℂ ) x✝¹ • ⇑ x✝ ; rfl All goals completed! 🐙
x ↦ ‖x‖ˢψ(x) is smooth away from x = 0.
@[ fun_prop ]
lemma radiusPowLM_apply_contDiffAt { d : ℕ } ( s : ℝ ) ( n : ℕ∞ ) ( ψ : 𝓢( Space d , ℂ ) ) { x : Space d }
( hx : x ≠ 0 ) : ContDiffAt ℝ n ( 𝐫 s ψ ) x := by d : ℕ s : ℝ n : ℕ∞ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 ⊢ ContDiffAt ℝ (↑ n ) ( ( 𝐫 s ) ψ ) x
refine ContDiffAt.smul ? _ ( ψ . contDiffAt n ) d : ℕ s : ℝ n : ℕ∞ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 ⊢ ContDiffAt ℝ (↑ n ) (fun x => ‖ x ‖ ^ s ) x
have h ( x : Space d ) : ‖ x ‖ ^ s = ( inner ℝ x x ) ^ ( s / 2 ) := by d : ℕ s : ℝ n : ℕ∞ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 ⊢ ContDiffAt ℝ (↑ n ) ( ( 𝐫 s ) ψ ) x d : ℕ s : ℝ n : ℕ∞ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 h : ∀ ( x : Space d ), ‖ x ‖ ^ s = inner ℝ x x ^ ( s / 2 ) ⊢ ContDiffAt ℝ (↑ n ) (fun x => ‖ x ‖ ^ s ) x
simp [ ← Real.rpow_natCast_mul , mul_div_cancel₀ ] d : ℕ s : ℝ n : ℕ∞ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 h : ∀ ( x : Space d ), ‖ x ‖ ^ s = inner ℝ x x ^ ( s / 2 ) ⊢ ContDiffAt ℝ (↑ n ) (fun x => ‖ x ‖ ^ s ) x d : ℕ s : ℝ n : ℕ∞ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 h : ∀ ( x : Space d ), ‖ x ‖ ^ s = inner ℝ x x ^ ( s / 2 ) ⊢ ContDiffAt ℝ (↑ n ) (fun x => ‖ x ‖ ^ s ) x
simp only [ h ] d : ℕ s : ℝ n : ℕ∞ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 h : ∀ ( x : Space d ), ‖ x ‖ ^ s = inner ℝ x x ^ ( s / 2 ) ⊢ ContDiffAt ℝ (↑ n ) (fun x => inner ℝ x x ^ ( s / 2 ) ) x
exact ContDiffAt.rpow_const_of_ne ( by d : ℕ s : ℝ n : ℕ∞ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 h : ∀ ( x : Space d ), ‖ x ‖ ^ s = inner ℝ x x ^ ( s / 2 ) ⊢ ContDiffAt ℝ (↑ n ) (fun x => inner ℝ x x ) x fun_prop All goals completed! 🐙 ) ( inner_self_ne_zero . mpr hx )
x ↦ ‖x‖ˢψ(x) is strongly measurable.
x ↦ ‖x‖ˢψ(x) is square-integrable provided s is not too negative.
lemma radiusPowLM_apply_memHS { d : ℕ } ( s : ℝ ) ( ψ : 𝓢( Space d , ℂ ) ) ( a : ℕ )
( hψ : ψ ∈ PolyBddSchwartzMap d a ) ( h : 0 < d + 2 * ( a + s ) ) :
MemHS ( 𝐫 s ψ ) := by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) ⊢ MemHS ( ( 𝐫 s ) ψ )
rcases Nat.eq_zero_or_pos d with ( rfl | hd ) inl s : ℝ a : ℕ ψ : 𝓢( Space 0 , ℂ ) hψ : ψ ∈ PolyBddSchwartzMap 0 ↑ a h : 0 < ↑ 0 + 2 * ( ↑ a + s ) ⊢ MemHS ( ( 𝐫 s ) ψ ) inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 ⊢ MemHS ( ( 𝐫 s ) ψ )
· inl s : ℝ a : ℕ ψ : 𝓢( Space 0 , ℂ ) hψ : ψ ∈ PolyBddSchwartzMap 0 ↑ a h : 0 < ↑ 0 + 2 * ( ↑ a + s ) ⊢ MemHS ( ( 𝐫 s ) ψ ) simp only [ MemHS , MemLp.of_discrete ] All goals completed! 🐙
· inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 ⊢ MemHS ( ( 𝐫 s ) ψ ) have : NeZero d := ⟨ hd . ne' ⟩ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d ⊢ MemHS ( ( 𝐫 s ) ψ )
refine ( memLp_two_iff_integrable_sq_norm ( by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d ⊢ AEStronglyMeasurable ( ( 𝐫 s ) ψ ) volume fun_prop All goals completed! 🐙 ) ) . mpr ⟨ by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d ⊢ AEStronglyMeasurable (fun x => ‖ ( 𝐫 s ) ψ x ‖ ^ 2 ) volume fun_prop All goals completed! 🐙 , ? _ ⟩
suffices ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this✝ : NeZero d this : ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ ⊢ HasFiniteIntegral (fun x => ‖ ( 𝐫 s ) ψ x ‖ ^ 2 ) volume inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
have hInt ( x : Space d ) : ‖ 𝐫 s ψ x ‖ ^ 2 = ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) := by
simp [ radiusPowLM , mul_pow , mul_comm , Real.rpow_mul ] d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this✝ : NeZero d this : ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ hInt : ∀ ( x : Space d ), ‖ ( 𝐫 s ) ψ x ‖ ^ 2 = ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ⊢ HasFiniteIntegral (fun x => ‖ ( 𝐫 s ) ψ x ‖ ^ 2 ) volume inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this✝ : NeZero d this : ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ hInt : ∀ ( x : Space d ), ‖ ( 𝐫 s ) ψ x ‖ ^ 2 = ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ⊢ HasFiniteIntegral (fun x => ‖ ( 𝐫 s ) ψ x ‖ ^ 2 ) volume inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
simpa only [ HasFiniteIntegral , hInt ] inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
have lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ } ,
IntegrableOn ( fun x ↦ ‖ x ‖ ^ p ) S → ∀ { G : Space d → ENNReal } ,
∫⁻ x in S , G x ≤ ∫⁻ x in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ →
∫⁻ x in S , G x < ⊤ := by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) ⊢ MemHS ( ( 𝐫 s ) ψ ) inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
intro S C p hp G hG d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d S : Set ( Space d ) C : ℝ p : ℝ hp : IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume G : Space d → ENNReal hG : ∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ ⊢ ∫⁻ ( x : Space d ) in S , G x < ⊤ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
refine hG . trans_lt ? _ d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d S : Set ( Space d ) C : ℝ p : ℝ hp : IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume G : Space d → ENNReal hG : ∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ ⊢ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ < ⊤ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
rw [ lintegral_const_mul _ ( by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d S : Set ( Space d ) C : ℝ p : ℝ hp : IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume G : Space d → ENNReal hG : ∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ ⊢ Measurable fun x => ‖ ‖ x ‖ ^ p ‖ₑ d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d S : Set ( Space d ) C : ℝ p : ℝ hp : IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume G : Space d → ENNReal hG : ∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ ⊢ ‖ C ^ 2 ‖ₑ * ∫⁻ ( a : Space d ) in S , ‖ ‖ a ‖ ^ p ‖ₑ < ⊤ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ fun_prop All goals completed! 🐙 d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d S : Set ( Space d ) C : ℝ p : ℝ hp : IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume G : Space d → ENNReal hG : ∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ ⊢ ‖ C ^ 2 ‖ₑ * ∫⁻ ( a : Space d ) in S , ‖ ‖ a ‖ ^ p ‖ₑ < ⊤ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ ) ] d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d S : Set ( Space d ) C : ℝ p : ℝ hp : IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume G : Space d → ENNReal hG : ∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ ⊢ ‖ C ^ 2 ‖ₑ * ∫⁻ ( a : Space d ) in S , ‖ ‖ a ‖ ^ p ‖ₑ < ⊤ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
exact ENNReal.mul_lt_top enorm_lt_top hp . hasFiniteIntegral inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
rw [ ← lintegral_add_compl _ ( measurableSet_ball ( x := 0 ) ( ε := 1 ) ) , inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ( ∫⁻ ( x : Space d ) in Metric.ball 0 1 , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ) +
∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ <
⊤ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) in Metric.ball 0 1 , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ ∧
∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ ENNReal.add_lt_top inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) in Metric.ball 0 1 , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ ∧
∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) in Metric.ball 0 1 , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ ∧
∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ ] inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) in Metric.ball 0 1 , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ ∧
∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
constructor inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) in Metric.ball 0 1 , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
· inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) in Metric.ball 0 1 , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
obtain ⟨ C , hC_pos , hC ⟩ := hψ a ( le_refl _ ) inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C ⊢ ∫⁻ ( x : Space d ) in Metric.ball 0 1 , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
suffices hBound : ∀ᵐ x , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( 2 * ( a + s ) ) ‖ₑ by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C hBound : ∀ᵐ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ ⊢ ∫⁻ ( x : Space d ) in Metric.ball 0 1 , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C ⊢ ∀ᵐ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ
exact lintegral_lt_top_aux ( ( integrableOn_norm_rpow_ball_iff Real.zero_lt_one _ ) . mpr h )
( setLIntegral_mono_ae' measurableSet_ball ( Eventually.mono hBound fun _ h' _ ↦ h' ) ) inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C ⊢ ∀ᵐ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C ⊢ ∀ᵐ ( x : Space d ) , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ
apply ae_iff . mpr inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C ⊢ volume { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } = 0
refine measure_mono_null ? _ ( measure_singleton 0 ) inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C ⊢ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } ⊆ { 0 }
intro x hx inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } ⊢ x ∈ { 0 }
by_contra hx' inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : x ∉ { 0 } ⊢ False
apply hx inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : x ∉ { 0 } ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ
apply norm_pos_iff . mpr at hx' inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ
simp_rw [ inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ ← enorm_mul , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 * ‖ x ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ enorm_le_iff_norm_le , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ ≤ ‖ C ^ 2 * ‖ x ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ mul_add , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ ≤ ‖ C ^ 2 * ‖ x ‖ ^ ( 2 * ↑ a + 2 * s ) ‖ Real.rpow_add hx' , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ ≤ ‖ C ^ 2 * ( ‖ x ‖ ^ ( 2 * ↑ a ) * ‖ x ‖ ^ ( 2 * s ) ) ‖ norm_mul , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 ‖ * ‖ ‖ x ‖ ^ ( 2 * s ) ‖ ≤ ‖ C ^ 2 ‖ * ( ‖ ‖ x ‖ ^ ( 2 * ↑ a ) ‖ * ‖ ‖ x ‖ ^ ( 2 * s ) ‖ ) ← mul_assoc inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 ‖ * ‖ ‖ x ‖ ^ ( 2 * s ) ‖ ≤ ‖ C ^ 2 ‖ * ‖ ‖ x ‖ ^ ( 2 * ↑ a ) ‖ * ‖ ‖ x ‖ ^ ( 2 * s ) ‖ ]
refine mul_le_mul_of_nonneg_right ? _ ( norm_nonneg _ ) inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 ‖ ≤ ‖ C ^ 2 ‖ * ‖ ‖ x ‖ ^ ( 2 * ↑ a ) ‖
simp_rw [ inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 ‖ ≤ ‖ C ^ 2 ‖ * ‖ ‖ x ‖ ^ ( 2 * ↑ a ) ‖ ← Nat.cast_two ( R := ℝ ) , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 ‖ ≤ ‖ C ^ 2 ‖ * ‖ ‖ x ‖ ^ ( ↑ 2 * ↑ a ) ‖ mul_comm , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 ‖ ≤ ‖ C ^ 2 ‖ * ‖ ‖ x ‖ ^ ( ↑ a * ↑ 2 ) ‖ Real.rpow_mul_natCast hx' . le , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 ‖ ≤ ‖ C ^ 2 ‖ * ‖ ( ‖ x ‖ ^ ↑ a ) ^ 2 ‖ norm_pow , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ‖ ^ 2 ≤ ‖ C ‖ ^ 2 * ‖ ‖ x ‖ ^ ↑ a ‖ ^ 2 ← mul_pow , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ‖ ^ 2 ≤ ( ‖ C ‖ * ‖ ‖ x ‖ ^ ↑ a ‖ ) ^ 2
norm_norm , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 ≤ ( ‖ C ‖ * ‖ ‖ x ‖ ^ ↑ a ‖ ) ^ 2 Real.norm_eq_abs , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 ≤ ( | C | * | ‖ x ‖ ^ ↑ a | ) ^ 2 abs_of_pos hC_pos , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 ≤ ( C * | ‖ x ‖ ^ ↑ a | ) ^ 2 abs_of_nonneg ( Real.rpow_nonneg hx' . le _ ) inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 ≤ ( C * ‖ x ‖ ^ ↑ a ) ^ 2 ]
apply ( sq_le_sq₀ ( norm_nonneg _ ) ( by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ 0 ≤ C * ‖ x ‖ ^ ↑ a positivity All goals completed! 🐙 ) ) . mpr
apply ( inv_mul_le_iff₀' ( by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ 0 < ‖ x ‖ ^ ↑ a positivity All goals completed! 🐙 ) ) . mp
rw [ ← Real.rpow_neg_one , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ( ‖ x ‖ ^ ↑ a ) ^ (- 1 ) * ‖ ψ x ‖ ≤ C inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C ← Real.rpow_mul hx' . le , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( ↑ a * - 1 ) * ‖ ψ x ‖ ≤ C inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C mul_comm _ ( - 1 ) , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - 1 * ↑ a ) * ‖ ψ x ‖ ≤ C inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C neg_mul , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ( 1 * ↑ a ) ) * ‖ ψ x ‖ ≤ C inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C one_mul , inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C
Real.rpow_neg_natCast inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C ] inr.left d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ { a_1 | ¬ ‖ ‖ ψ a_1 ‖ ^ 2 * ‖ a_1 ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ a_1 ‖ ^ ( 2 * ( ↑ a + s ) ) ‖ₑ } hx' : 0 < ‖ x ‖ ⊢ ‖ x ‖ ^ ( - ↑ a ) * ‖ ψ x ‖ ≤ C
exact hC x All goals completed! 🐙
· inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ ⊢ ∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
obtain ⟨ C , hC_pos , hC ⟩ := ψ . decay ( ⌈ s ⌉ . toNat + d ) 0 inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ⌈ s ⌉ . toNat + d ) * ‖ iteratedFDeriv ℝ 0 (⇑ ψ ) x ‖ ≤ C ⊢ ∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
simp only [ norm_iteratedFDeriv_zero , ← Real.rpow_natCast , Nat.cast_add ] at hC inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C ⊢ ∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤
suffices hBound : ∀ x ∈ ( Metric.ball 0 1 ) ᶜ ,
‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * d : ℝ ) ‖ₑ by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C hBound : ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ ⊢ ∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C ⊢ ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ
have hd' : ( d + - 2 * d : ℝ ) < 0 := by simp [ hd ] d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C hBound : ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ hd' : ↑ d + - 2 * ↑ d < 0 ⊢ ∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C ⊢ ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C hBound : ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ hd' : ↑ d + - 2 * ↑ d < 0 ⊢ ∫⁻ ( x : Space d ) in ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ < ⊤ inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C ⊢ ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ
exact lintegral_lt_top_aux ( ( integrableOn_norm_rpow_ball_compl_iff zero_lt_one _ ) . mpr hd' )
( setLIntegral_mono' ( by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C hBound : ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ hd' : ↑ d + - 2 * ↑ d < 0 ⊢ MeasurableSet ( Metric.ball 0 1 ) ᶜ inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C ⊢ ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ measurability All goals completed! 🐙 inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C ⊢ ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ ) hBound ) inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C ⊢ ∀ x ∈ ( Metric.ball 0 1 ) ᶜ , ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ
intro x hx inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : x ∈ ( Metric.ball 0 1 ) ᶜ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ
simp only [ Set.mem_compl_iff , Metric.mem_ball , dist_zero_right , not_lt ] at hx inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ
simp_rw [ inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ ← enorm_mul , inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ₑ ≤ ‖ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ₑ enorm_le_iff_norm_le , inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ‖ ≤ ‖ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ norm_mul , inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ^ 2 ‖ * ‖ ‖ x ‖ ^ ( 2 * s ) ‖ ≤ ‖ C ^ 2 ‖ * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ norm_pow , inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ ‖ ‖ ψ x ‖ ‖ ^ 2 * ‖ ‖ x ‖ ^ ( 2 * s ) ‖ ≤ ‖ C ‖ ^ 2 * ‖ ‖ x ‖ ^ ( - 2 * ↑ d ) ‖ Real.norm_eq_abs , inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ | ‖ ψ x ‖ | ^ 2 * | ‖ x ‖ ^ ( 2 * s ) | ≤ | C | ^ 2 * | ‖ x ‖ ^ ( - 2 * ↑ d ) | sq_abs , inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 * | ‖ x ‖ ^ ( 2 * s ) | ≤ C ^ 2 * | ‖ x ‖ ^ ( - 2 * ↑ d ) |
Real.abs_rpow_of_nonneg ( norm_nonneg _ ) , inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 * | ‖ x ‖ | ^ ( 2 * s ) ≤ C ^ 2 * | ‖ x ‖ | ^ ( - 2 * ↑ d ) abs_norm inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) ]
have hx' : 0 < ‖ x ‖ := by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) ⊢ MemHS ( ( 𝐫 s ) ψ ) inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) linarith inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d )
have hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ⌈ s ⌉ . toNat + d ) : ℝ ) := by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) ⊢ MemHS ( ( 𝐫 s ) ψ ) inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d )
rw [ Real.rpow_neg hx' . le d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ≤ C * ( ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⁻¹ d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ≤ C * ( ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⁻¹ inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) ] d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ ⊢ ‖ ψ x ‖ ≤ C * ( ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⁻¹ inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d )
exact ( le_mul_inv_iff₀' <| Real.rpow_pos_of_pos hx' _ ) . mpr ( hC x ) inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) inr.right d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d )
calc
_ ≤ ( C * ‖ x ‖ ^ ( - ( ⌈ s ⌉ . toNat + d ) : ℝ ) ) ^ 2 * ‖ x ‖ ^ ( 2 * s ) := by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ‖ ψ x ‖ ^ 2 * ‖ x ‖ ^ ( 2 * s ) ≤ ( C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ) ^ 2 * ‖ x ‖ ^ ( 2 * s )
refine mul_le_mul_of_nonneg_right ? _ ( Real.rpow_nonneg hx' . le _ ) d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ‖ ψ x ‖ ^ 2 ≤ ( C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ) ^ 2
exact pow_le_pow_left₀ ( norm_nonneg _ ) hψ 2 All goals completed! 🐙
_ = C ^ 2 * ‖ x ‖ ^ ( - 2 * d : ℝ ) * ‖ x ‖ ^ ( 2 * ( s - ⌈ s ⌉ . toNat ) : ℝ ) := by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ( C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ) ^ 2 * ‖ x ‖ ^ ( 2 * s ) = C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) * ‖ x ‖ ^ ( 2 * ( s - ↑ ⌈ s ⌉ . toNat ) )
simp_rw [ d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ( C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ) ^ 2 * ‖ x ‖ ^ ( 2 * s ) = C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) * ‖ x ‖ ^ ( 2 * ( s - ↑ ⌈ s ⌉ . toNat ) ) mul_pow , d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ C ^ 2 * ( ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ) ^ 2 * ‖ x ‖ ^ ( 2 * s ) = C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) * ‖ x ‖ ^ ( 2 * ( s - ↑ ⌈ s ⌉ . toNat ) ) ← Real.rpow_mul_natCast hx' . le , d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ C ^ 2 * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ↑ 2 ) * ‖ x ‖ ^ ( 2 * s ) = C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) * ‖ x ‖ ^ ( 2 * ( s - ↑ ⌈ s ⌉ . toNat ) ) mul_assoc , d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ C ^ 2 * ( ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ↑ 2 ) * ‖ x ‖ ^ ( 2 * s ) ) = C ^ 2 * ( ‖ x ‖ ^ ( - 2 * ↑ d ) * ‖ x ‖ ^ ( 2 * ( s - ↑ ⌈ s ⌉ . toNat ) ) ) ← Real.rpow_add hx' d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ C ^ 2 * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ↑ 2 + 2 * s ) = C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d + 2 * ( s - ↑ ⌈ s ⌉ . toNat ) ) ]
ring_nf All goals completed! 🐙
suffices s ≤ ⌈ s ⌉ . toNat by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this✝ : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) this : s ≤ ↑ ⌈ s ⌉ . toNat ⊢ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) * ‖ x ‖ ^ ( 2 * ( s - ↑ ⌈ s ⌉ . toNat ) ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) inr.right.calc.step d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ s ≤ ↑ ⌈ s ⌉ . toNat
have h' : 0 < C ^ 2 * ‖ x ‖ ^ ( - 2 * d : ℝ ) :=
mul_pos ( sq_pos_of_pos hC_pos ) ( Real.rpow_pos_of_pos hx' _ ) d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this✝ : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) this : s ≤ ↑ ⌈ s ⌉ . toNat h' : 0 < C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) ⊢ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) * ‖ x ‖ ^ ( 2 * ( s - ↑ ⌈ s ⌉ . toNat ) ) ≤ C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) inr.right.calc.step d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ s ≤ ↑ ⌈ s ⌉ . toNat
apply ( mul_le_iff_le_one_right h' ) . mpr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this✝ : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) this : s ≤ ↑ ⌈ s ⌉ . toNat h' : 0 < C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) ⊢ ‖ x ‖ ^ ( 2 * ( s - ↑ ⌈ s ⌉ . toNat ) ) ≤ 1 inr.right.calc.step d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ s ≤ ↑ ⌈ s ⌉ . toNat
exact Real.rpow_le_one_of_one_le_of_nonpos hx ( by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this✝ : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) this : s ≤ ↑ ⌈ s ⌉ . toNat h' : 0 < C ^ 2 * ‖ x ‖ ^ ( - 2 * ↑ d ) ⊢ 2 * ( s - ↑ ⌈ s ⌉ . toNat ) ≤ 0 inr.right.calc.step d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ s ≤ ↑ ⌈ s ⌉ . toNat linarith All goals completed! 🐙 inr.right.calc.step d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ s ≤ ↑ ⌈ s ⌉ . toNat ) inr.right.calc.step d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ s ≤ ↑ ⌈ s ⌉ . toNat
exact ( Int.le_ceil s ) . trans ( by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) a : ℕ hψ✝ : ψ ∈ PolyBddSchwartzMap d ↑ a h : 0 < ↑ d + 2 * ( ↑ a + s ) hd : d > 0 this : NeZero d lintegral_lt_top_aux : ∀ { S : Set ( Space d ) } { C p : ℝ },
IntegrableOn (fun x => ‖ x ‖ ^ p ) S volume →
∀ { G : Space d → ENNReal },
∫⁻ ( x : Space d ) in S , G x ≤ ∫⁻ ( x : Space d ) in S , ‖ C ^ 2 ‖ₑ * ‖ ‖ x ‖ ^ p ‖ₑ → ∫⁻ ( x : Space d ) in S , G x < ⊤ C : ℝ hC_pos : 0 < C hC : ∀ ( x : Space d ), ‖ x ‖ ^ ( ↑ ⌈ s ⌉ . toNat + ↑ d ) * ‖ ψ x ‖ ≤ C x : Space d hx : 1 ≤ ‖ x ‖ hx' : 0 < ‖ x ‖ hψ : ‖ ψ x ‖ ≤ C * ‖ x ‖ ^ ( - ( ↑ ⌈ s ⌉ . toNat + ↑ d ) ) ⊢ ↑ ⌈ s ⌉ ≤ ↑ ⌈ s ⌉ . toNat exact_mod_cast Int.self_le_toNat ⌈ s ⌉ All goals completed! 🐙 )
A.3.1. As limit of regularized operators
Neighborhoods of "0" in the non-zero reals, i.e. those sets containing (-ε,0) ∪ (0,ε) ⊆ ℝˣ
for some ε > 0.
abbrev nhdsZeroUnits : Filter ℝ ˣ := comap ( Units.coeHom ℝ ) ( nhds 0 )
𝐫[ε,s] ψ converges pointwise to 𝐫[s] ψ as ε → 0 except perhaps at x = 0.
lemma radiusRegPow_tendsto_radiusPow { d : ℕ } ( s : ℝ ) ( ψ : 𝓢( Space d , ℂ ) ) { x : Space d }
( hx : x ≠ 0 ) : Tendsto ( fun ε ↦ 𝐫₀ ε s ψ x ) nhdsZeroUnits ( nhds ( 𝐫 s ψ x ) ) := by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 ⊢ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) )
have hpow : ‖ x ‖ ^ s = ( ‖ x ‖ ^ 2 + 0 ^ 2 ) ^ ( s / 2 ) := by
simp [ ← Real.rpow_natCast_mul , mul_div_cancel₀ ] d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 hpow : ‖ x ‖ ^ s = ( ‖ x ‖ ^ 2 + 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) ) d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 hpow : ‖ x ‖ ^ s = ( ‖ x ‖ ^ 2 + 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) )
simp only [ radiusRegPowCLM_apply , radiusPowLM_apply , Complex.real_smul , hpow ] d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 hpow : ‖ x ‖ ^ s = ( ‖ x ‖ ^ 2 + 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun ε => ↑ ( ( ‖ x ‖ ^ 2 + ↑ ε ^ 2 ) ^ ( s / 2 ) ) * ψ x ) nhdsZeroUnits ( nhds ( ↑ ( ( ‖ x ‖ ^ 2 + 0 ^ 2 ) ^ ( s / 2 ) ) * ψ x ) )
refine Tendsto.mul_const ( ψ x ) <| Tendsto.ofReal ? _ d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 hpow : ‖ x ‖ ^ s = ( ‖ x ‖ ^ 2 + 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun ε => ( ‖ x ‖ ^ 2 + ↑ ε ^ 2 ) ^ ( s / 2 ) ) nhdsZeroUnits ( nhds ( ( ‖ x ‖ ^ 2 + 0 ^ 2 ) ^ ( s / 2 ) ) )
refine Tendsto.rpow_const ? _ ( Or.inl <| by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ≠ 0 hpow : ‖ x ‖ ^ s = ( ‖ x ‖ ^ 2 + 0 ^ 2 ) ^ ( s / 2 ) ⊢ ‖ x ‖ ^ 2 + 0 ^ 2 ≠ 0 simp [ hx ] All goals completed! 🐙 )
exact Tendsto.const_add _ <| Tendsto.pow tendsto_comap 2 All goals completed! 🐙
𝐫[ε,s] ψ converges pointwise to 𝐫[s] ψ as ε → 0 provided 𝐫[ε,s] ψ 0 is bounded.
lemma radiusRegPow_tendsto_radiusPow' { d : ℕ } ( s : ℝ ) ( ψ : 𝓢( Space d , ℂ ) ) ( h : 0 ≤ s ∨ ψ 0 = 0 ) :
Tendsto ( fun ε ↦ ⇑ ( 𝐫₀ ε s ψ ) ) nhdsZeroUnits ( nhds ( 𝐫 s ψ ) ) := by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) h : 0 ≤ s ∨ ψ 0 = 0 ⊢ Tendsto (fun ε => ⇑ ( ( 𝐫₀ ε s ) ψ ) ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ ) )
refine tendsto_pi_nhds . mpr fun x ↦ ? _ d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) h : 0 ≤ s ∨ ψ 0 = 0 x : Space d ⊢ Tendsto (fun i => ( ( 𝐫₀ i s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) )
rcases eq_zero_or_neZero x with ( rfl | hx ) inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) h : 0 ≤ s ∨ ψ 0 = 0 ⊢ Tendsto (fun i => ( ( 𝐫₀ i s ) ψ ) 0 ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ 0 ) ) inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) h : 0 ≤ s ∨ ψ 0 = 0 x : Space d hx : NeZero x ⊢ Tendsto (fun i => ( ( 𝐫₀ i s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) )
· inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) h : 0 ≤ s ∨ ψ 0 = 0 ⊢ Tendsto (fun i => ( ( 𝐫₀ i s ) ψ ) 0 ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ 0 ) ) rcases h with ( hs | hψ ) inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s ⊢ Tendsto (fun i => ( ( 𝐫₀ i s ) ψ ) 0 ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ 0 ) ) inl.inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hψ : ψ 0 = 0 ⊢ Tendsto (fun i => ( ( 𝐫₀ i s ) ψ ) 0 ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ 0 ) )
· inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s ⊢ Tendsto (fun i => ( ( 𝐫₀ i s ) ψ ) 0 ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ 0 ) ) simp only [ radiusRegPowCLM_apply , radiusPowLM_apply , Complex.real_smul , norm_zero ,
ne_eq , OfNat.ofNat_ne_zero , not_false_eq_true , zero_pow , zero_add ] inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( 0 ^ s ) * ψ 0 ) )
have : ( 0 : ℝ ) ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) := by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) h : 0 ≤ s ∨ ψ 0 = 0 ⊢ Tendsto (fun ε => ⇑ ( ( 𝐫₀ ε s ) ψ ) ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ ) ) inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( 0 ^ s ) * ψ 0 ) )
rw [ ← Real.rpow_natCast_mul ( le_refl 0 ) , d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s ⊢ 0 ^ s = 0 ^ ( ↑ 2 * ( s / 2 ) ) inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( 0 ^ s ) * ψ 0 ) ) Nat.cast_ofNat , d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s ⊢ 0 ^ s = 0 ^ ( 2 * ( s / 2 ) ) inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( 0 ^ s ) * ψ 0 ) ) mul_div_cancel₀ s ( by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s ⊢ 2 ≠ 0 inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( 0 ^ s ) * ψ 0 ) ) norm_num All goals completed! 🐙 inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( 0 ^ s ) * ψ 0 ) ) ) ] inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( 0 ^ s ) * ψ 0 ) ) inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( 0 ^ s ) * ψ 0 ) )
rw [ this inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( ( 0 ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) ) inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( ( 0 ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) ) ] inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ↑ ( ( ↑ i ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) nhdsZeroUnits ( nhds ( ↑ ( ( 0 ^ 2 ) ^ ( s / 2 ) ) * ψ 0 ) )
refine Tendsto.mul_const ( ψ 0 ) <| Tendsto.ofReal ? _ inl.inl d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ Tendsto (fun i => ( ↑ i ^ 2 ) ^ ( s / 2 ) ) nhdsZeroUnits ( nhds ( ( 0 ^ 2 ) ^ ( s / 2 ) ) )
exact Tendsto.rpow_const ( Tendsto.pow tendsto_comap 2 ) ( Or.inr <| by d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hs : 0 ≤ s this : 0 ^ s = ( 0 ^ 2 ) ^ ( s / 2 ) ⊢ 0 ≤ s / 2 linarith All goals completed! 🐙 )
· inl.inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) hψ : ψ 0 = 0 ⊢ Tendsto (fun i => ( ( 𝐫₀ i s ) ψ ) 0 ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ 0 ) ) simp [ hψ ] All goals completed! 🐙
· inr d : ℕ s : ℝ ψ : 𝓢( Space d , ℂ ) h : 0 ≤ s ∨ ψ 0 = 0 x : Space d hx : NeZero x ⊢ Tendsto (fun i => ( ( 𝐫₀ i s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) ) exact radiusRegPow_tendsto_radiusPow s ψ hx . ne All goals completed! 🐙
a.e. version of radiusRegPow_tendsto_radiusPow
lemma radiusRegPow_ae_tendsto_radiusPow { d : ℕ } [ NeZero d ] ( s : ℝ ) ( ψ : 𝓢( Space d , ℂ ) ) :
∀ᵐ x , Tendsto ( fun ε ↦ 𝐫₀ ε s ψ x ) nhdsZeroUnits ( nhds ( 𝐫 s ψ x ) ) := by d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) ⊢ ∀ᵐ ( x : Space d ) , Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) )
apply ae_iff . mpr d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) ⊢ volume { a | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) a ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ a ) ) } = 0
suffices h : { x | ¬ Tendsto ( fun ε ↦ 𝐫₀ ε s ψ x ) nhdsZeroUnits ( nhds ( 𝐫 s ψ x ) ) } ⊆ { 0 } by d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) h : { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) ) } ⊆ { 0 } ⊢ volume { a | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) a ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ a ) ) } = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) ⊢ { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) ) } ⊆ { 0 }
exact measure_mono_null h ( measure_singleton 0 ) d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) ⊢ { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) ) } ⊆ { 0 } d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) ⊢ { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) ) } ⊆ { 0 }
intro x hx d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ∈ { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) ) } ⊢ x ∈ { 0 }
by_contra hx' d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) x : Space d hx : x ∈ { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) ) } hx' : x ∉ { 0 } ⊢ False
exact hx <| radiusRegPow_tendsto_radiusPow s ψ hx' All goals completed! 🐙
lemma radiusRegPow_ae_tendsto_iff { d : ℕ } [ NeZero d ] { s : ℝ } { ψ : 𝓢( Space d , ℂ ) }
{ φ : Space d → ℂ } : ( ∀ᵐ x , Tendsto ( fun ε ↦ 𝐫₀ ε s ψ x ) nhdsZeroUnits ( nhds ( φ x ) ) )
↔ φ =ᵐ[ volume ] 𝐫 s ψ := by d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ ⊢ ( ∀ᵐ ( x : Space d ) , Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) ) ↔ φ =ᵐ[ volume ] ( 𝐫 s ) ψ
let t₁ := { x | ¬ Tendsto ( fun ε ↦ 𝐫₀ ε s ψ x ) nhdsZeroUnits ( nhds ( φ x ) ) } d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } ⊢ ( ∀ᵐ ( x : Space d ) , Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) ) ↔ φ =ᵐ[ volume ] ( 𝐫 s ) ψ
let t₂ := { x | φ x ≠ 𝐫 s ψ x } d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ ( ∀ᵐ ( x : Space d ) , Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) ) ↔ φ =ᵐ[ volume ] ( 𝐫 s ) ψ
show volume t₁ = 0 ↔ volume t₂ = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ volume t₁ = 0 ↔ volume t₂ = 0
suffices heq : t₁ ∪ { 0 } = t₂ ∪ { 0 } by d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } heq : t₁ ∪ { 0 } = t₂ ∪ { 0 } ⊢ volume t₁ = 0 ↔ volume t₂ = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ t₁ ∪ { 0 } = t₂ ∪ { 0 }
have hUnion : ∀ t : Set ( Space d ) , volume t = 0 ↔ volume ( t ∪ { 0 } ) = 0 :=
fun _ ↦ by d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } heq : t₁ ∪ { 0 } = t₂ ∪ { 0 } x✝ : Set ( Space d ) ⊢ volume x✝ = 0 ↔ volume ( x✝ ∪ { 0 } ) = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } heq : t₁ ∪ { 0 } = t₂ ∪ { 0 } hUnion : ∀ ( t : Set ( Space d ) ), volume t = 0 ↔ volume ( t ∪ { 0 } ) = 0 ⊢ volume t₁ = 0 ↔ volume t₂ = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ t₁ ∪ { 0 } = t₂ ∪ { 0 } simp only [ measure_union_null_iff , measure_singleton , and_true ] d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } heq : t₁ ∪ { 0 } = t₂ ∪ { 0 } hUnion : ∀ ( t : Set ( Space d ) ), volume t = 0 ↔ volume ( t ∪ { 0 } ) = 0 ⊢ volume t₁ = 0 ↔ volume t₂ = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ t₁ ∪ { 0 } = t₂ ∪ { 0 } d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } heq : t₁ ∪ { 0 } = t₂ ∪ { 0 } hUnion : ∀ ( t : Set ( Space d ) ), volume t = 0 ↔ volume ( t ∪ { 0 } ) = 0 ⊢ volume t₁ = 0 ↔ volume t₂ = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ t₁ ∪ { 0 } = t₂ ∪ { 0 }
rw [ hUnion t₁ , d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } heq : t₁ ∪ { 0 } = t₂ ∪ { 0 } hUnion : ∀ ( t : Set ( Space d ) ), volume t = 0 ↔ volume ( t ∪ { 0 } ) = 0 ⊢ volume ( t₁ ∪ { 0 } ) = 0 ↔ volume t₂ = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ t₁ ∪ { 0 } = t₂ ∪ { 0 } hUnion t₂ , d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } heq : t₁ ∪ { 0 } = t₂ ∪ { 0 } hUnion : ∀ ( t : Set ( Space d ) ), volume t = 0 ↔ volume ( t ∪ { 0 } ) = 0 ⊢ volume ( t₁ ∪ { 0 } ) = 0 ↔ volume ( t₂ ∪ { 0 } ) = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ t₁ ∪ { 0 } = t₂ ∪ { 0 } heq d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } heq : t₁ ∪ { 0 } = t₂ ∪ { 0 } hUnion : ∀ ( t : Set ( Space d ) ), volume t = 0 ↔ volume ( t ∪ { 0 } ) = 0 ⊢ volume ( t₂ ∪ { 0 } ) = 0 ↔ volume ( t₂ ∪ { 0 } ) = 0 d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ t₁ ∪ { 0 } = t₂ ∪ { 0 } ] d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ t₁ ∪ { 0 } = t₂ ∪ { 0 } d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ t₁ ∪ { 0 } = t₂ ∪ { 0 }
ext x d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } x : Space d ⊢ x ∈ t₁ ∪ { 0 } ↔ x ∈ t₂ ∪ { 0 }
rcases eq_zero_or_neZero x with ( rfl | hx ) inl d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ 0 ∈ t₁ ∪ { 0 } ↔ 0 ∈ t₂ ∪ { 0 } inr d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } x : Space d hx : NeZero x ⊢ x ∈ t₁ ∪ { 0 } ↔ x ∈ t₂ ∪ { 0 }
· inl d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } ⊢ 0 ∈ t₁ ∪ { 0 } ↔ 0 ∈ t₂ ∪ { 0 } simp All goals completed! 🐙
· inr d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } x : Space d hx : NeZero x ⊢ x ∈ t₁ ∪ { 0 } ↔ x ∈ t₂ ∪ { 0 } simp only [ Set.union_singleton , Set.mem_insert_iff , hx . ne , false_or ] inr d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } x : Space d hx : NeZero x ⊢ x ∈ t₁ ↔ x ∈ t₂
have hLim := radiusRegPow_tendsto_radiusPow s ψ hx . ne inr d : ℕ inst✝ : NeZero d s : ℝ ψ : 𝓢( Space d , ℂ ) φ : Space d → ℂ t₁ : Set ( Space d ) := { x | ¬ Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( φ x ) ) } t₂ : Set ( Space d ) := { x | φ x ≠ ( 𝐫 s ) ψ x } x : Space d hx : NeZero x hLim : Tendsto (fun ε => ( ( 𝐫₀ ε s ) ψ ) x ) nhdsZeroUnits ( nhds ( ( 𝐫 s ) ψ x ) ) ⊢ x ∈ t₁ ↔ x ∈ t₂
exact not_congr ⟨ fun h ↦ tendsto_nhds_unique h hLim , fun h ↦ h ▸ hLim ⟩ All goals completed! 🐙
B. Unbounded operators
B.1. Position vector
The operator on SpaceDHilbertSpace d acting by multiplication by fun x ↦ xᵢ.
B.2. Radius powers (regularized)
The operator on SpaceDHilbertSpace d acting by multiplication by
fun x ↦ (‖x‖² + ε²)^(s/2).
B.3. Radius powers
The operator on SpaceDHilbertSpace d acting by multiplication by fun x ↦ ‖x‖ˢ.