diff --git a/Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean b/Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean index 5c46fed99..f146f12c6 100644 --- a/Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean +++ b/Physlib/ClassicalMechanics/RigidBody/SolidSphere.lean @@ -51,8 +51,8 @@ lemma solidSphere_mass {d : ℕ} (m R : ℝ≥0) (hr : R ≠ 0) : (solidSphere d have h1 : (@volume (Space d.succ) measureSpaceOfInnerProductSpace).real (Metric.closedBall 0 R) ≠ 0 := by refine (measureReal_ne_zero_iff ?_).mpr ?_ - · apply Space.volume_closedBall_ne_top - · apply Space.volume_closedBall_ne_zero + · apply measure_closedBall_lt_top.ne + · apply (Metric.measure_closedBall_pos volume _ _).ne' have hr' := R.2 have hx : R.1 ≠ 0 := by simpa using hr apply lt_of_le_of_ne hr' (Ne.symm hx) diff --git a/Physlib/Electromagnetism/Current/InfiniteWire.lean b/Physlib/Electromagnetism/Current/InfiniteWire.lean index 7e6d5a4d2..f87c92906 100644 --- a/Physlib/Electromagnetism/Current/InfiniteWire.lean +++ b/Physlib/Electromagnetism/Current/InfiniteWire.lean @@ -117,7 +117,7 @@ noncomputable def infiniteWire (𝓕 : FreeSpace) (I : ℝ) : constantSliceDist 0 ((- I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun (x : Space 2) => Real.log ‖x‖ • Lorentz.Vector.basis (Sum.inr 0)) - (IsDistBounded.log_norm.smul_const _)) + ((IsDistBounded.log_norm (by norm_num)).smul_const _)) /-! @@ -155,7 +155,7 @@ lemma infiniteWire_vectorPotential (𝓕 : FreeSpace) (I : ℝ) : constantSliceDist 0 ((- I * 𝓕.μ₀ / (2 * Real.pi)) • distOfFunction (fun (x : Space 2) => Real.log ‖x‖ • EuclideanSpace.single 0 (1 : ℝ)) - (by apply IsDistBounded.log_norm.smul_const))) := by + (by apply (IsDistBounded.log_norm (by norm_num)).smul_const))) := by ext η i simp [vectorPotential, infiniteWire, constantTime_apply, constantSliceDist_apply, Lorentz.Vector.spatialCLM, distOfFunction_vector_eval, diff --git a/Physlib/Electromagnetism/PointParticle/ThreeDimension.lean b/Physlib/Electromagnetism/PointParticle/ThreeDimension.lean index ea35a1c45..465870ae5 100644 --- a/Physlib/Electromagnetism/PointParticle/ThreeDimension.lean +++ b/Physlib/Electromagnetism/PointParticle/ThreeDimension.lean @@ -157,7 +157,7 @@ lemma threeDimPointParticle_eq_distTranslate (𝓕 : FreeSpace) (q : ℝ) (r₀ distTranslate (basis.repr r₀) <| distOfFunction (fun x => (((q * 𝓕.μ₀ * 𝓕.c)/ (4 * π))* ‖x‖⁻¹) • Lorentz.Vector.basis (Sum.inl 0)) - ((IsDistBounded.inv.const_mul_fun _).smul_const _)) := by + (((IsDistBounded.inv (by norm_num)).const_mul_fun _).smul_const _)) := by rw [threeDimPointParticle] congr ext η @@ -187,8 +187,7 @@ lemma threeDimPointParticle_scalarPotential (𝓕 : FreeSpace) (q : ℝ) (r₀ : Lorentz.Vector.basis_apply, ↓reduceIte, mul_one, smul_eq_mul] rw [distOfFunction_mul_fun _ (IsDistBounded.inv_shift _), distOfFunction_mul_fun _ (IsDistBounded.inv_shift _)] - simp only [Nat.succ_eq_add_one, Nat.reduceAdd, ContinuousLinearMap.coe_smul', Pi.smul_apply, - smul_eq_mul] + simp only [ContinuousLinearMap.coe_smul', Pi.smul_apply, smul_eq_mul] ring_nf simp only [𝓕.c_sq, one_div, mul_inv_rev, mul_eq_mul_right_iff, inv_eq_zero, OfNat.ofNat_ne_zero, or_false] diff --git a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean index 9e177ed6c..a50407153 100644 --- a/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean +++ b/Physlib/QuantumMechanics/DDimensions/Operators/Position.lean @@ -220,7 +220,7 @@ lemma radiusPowLM_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a : MemHS (𝐫 s ψ) := by rcases Nat.eq_zero_or_pos d with (rfl | hd) · simp only [MemHS, MemLp.of_discrete] - · have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc + · have : NeZero d := ⟨hd.ne'⟩ refine (memLp_two_iff_integrable_sq_norm (by fun_prop)).mpr ⟨by fun_prop, ?_⟩ suffices ∫⁻ (x : Space d), ‖‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s)‖ₑ < ⊤ by have hInt (x : Space d) : ‖𝐫 s ψ x‖ ^ 2 = ‖ψ x‖ ^ 2 * ‖x‖ ^ (2 * s) := by @@ -237,7 +237,7 @@ lemma radiusPowLM_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a : _ = ‖C ^ 2‖ₑ * ∫⁻ (x : Space d) in (Metric.ball 0 1), ‖‖x‖ ^ (2 * (a + s))‖ₑ := lintegral_const_mul _ (by fun_prop) apply ENNReal.mul_lt_top enorm_lt_top - exact ((integrableOn_norm_rpow_ball_iff hd Real.zero_lt_one _).mpr h).hasFiniteIntegral + exact ((integrableOn_norm_rpow_ball_iff Real.zero_lt_one _).mpr h).hasFiniteIntegral apply ae_iff.mpr refine measure_mono_null ?_ (measure_singleton 0) intro x hx @@ -265,7 +265,7 @@ lemma radiusPowLM_apply_memHS {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, ℂ)) (a : lintegral_const_mul _ (by fun_prop) apply ENNReal.mul_lt_top enorm_lt_top have hd' : (d + -2 * d : ℝ) < 0 := by simp [hd] - exact ((integrableOn_norm_rpow_ball_compl_iff hd zero_lt_one _).mpr hd').hasFiniteIntegral + exact ((integrableOn_norm_rpow_ball_compl_iff zero_lt_one _).mpr hd').hasFiniteIntegral intro x hx simp only [Set.mem_compl_iff, Metric.mem_ball, dist_zero_right, not_lt] at hx simp_rw [← enorm_mul, enorm_le_iff_norm_le, norm_mul, norm_pow, Real.norm_eq_abs, sq_abs, @@ -336,26 +336,24 @@ lemma radiusRegPow_tendsto_radiusPow' {d : ℕ} (s : ℝ) (ψ : 𝓢(Space d, · exact radiusRegPow_tendsto_radiusPow s ψ hx.ne /-- a.e. version of `radiusRegPow_tendsto_radiusPow` -/ -lemma radiusRegPow_ae_tendsto_radiusPow {d : ℕ} (hd : 0 < d) (s : ℝ) (ψ : 𝓢(Space d, ℂ)) : +lemma radiusRegPow_ae_tendsto_radiusPow {d : ℕ} [NeZero d] (s : ℝ) (ψ : 𝓢(Space d, ℂ)) : ∀ᵐ x, Tendsto (fun ε ↦ 𝐫₀ ε s ψ x) nhdsZeroUnits (nhds (𝐫 s ψ x)) := by apply ae_iff.mpr suffices h : {x | ¬Tendsto (fun ε ↦ 𝐫₀ ε s ψ x) nhdsZeroUnits (nhds (𝐫 s ψ x))} ⊆ {0} by rcases Set.subset_singleton_iff_eq.mp h with (h' | h') · exact h' ▸ measure_empty - · have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc - exact h' ▸ measure_singleton 0 + · exact h' ▸ measure_singleton 0 intro x hx by_contra hx' exact hx <| radiusRegPow_tendsto_radiusPow s ψ hx' -lemma radiusRegPow_ae_tendsto_iff {d : ℕ} (hd : 0 < d) {s : ℝ} {ψ : 𝓢(Space d, ℂ)} +lemma radiusRegPow_ae_tendsto_iff {d : ℕ} [NeZero d] {s : ℝ} {ψ : 𝓢(Space d, ℂ)} {φ : Space d → ℂ} : (∀ᵐ x, Tendsto (fun ε ↦ 𝐫₀ ε s ψ x) nhdsZeroUnits (nhds (φ x))) ↔ φ =ᵐ[volume] 𝐫 s ψ := by let t₁ := {x | ¬Tendsto (fun ε ↦ 𝐫₀ ε s ψ x) nhdsZeroUnits (nhds (φ x))} let t₂ := {x | φ x ≠ 𝐫 s ψ x} show volume t₁ = 0 ↔ volume t₂ = 0 suffices heq : t₁ ∪ {0} = t₂ ∪ {0} by - have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc have hUnion : ∀ t : Set (Space d), volume t = 0 ↔ volume (t ∪ {0}) = 0 := fun _ ↦ by simp only [measure_union_null_iff, measure_singleton, and_true] rw [hUnion t₁, hUnion t₂, heq] diff --git a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean index 8449d469e..ff75caea1 100644 --- a/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean +++ b/Physlib/QuantumMechanics/DDimensions/SpaceDHilbertSpace/PolyBddSchwartzSubmodule.lean @@ -255,7 +255,7 @@ lemma dense_top (d : ℕ) : Dense (polyBddSchwartzSubmodule d ⊤ : Set (SpaceDH have hξ := L2.eLpNorm_rpow_two_norm_lt_top ξ simp_rw [eLpNorm_one_eq_lintegral_enorm, Real.rpow_ofNat, enorm_pow, enorm_norm] at hξ exact hξ - · have : Nontrivial (Space d) := Nat.succ_pred_eq_of_pos hd ▸ Space.instNontrivialSucc + · have : NeZero d := ⟨hd.ne'⟩ let C : ℝ := (ENNReal.ofReal (√Real.pi ^ d / Real.Gamma (d / 2 + 1))).toReal have hvolB : ⇑volume ∘ B = fun n ↦ ENNReal.ofReal (C * (b n).rOut ^ d) := by ext n diff --git a/Physlib/SpaceAndTime/Space/Basic.lean b/Physlib/SpaceAndTime/Space/Basic.lean index 7fb27fcd3..dfae07a05 100644 --- a/Physlib/SpaceAndTime/Space/Basic.lean +++ b/Physlib/SpaceAndTime/Space/Basic.lean @@ -240,12 +240,12 @@ noncomputable instance {d} : MetricSpace (Space d) where -/ -instance {d : ℕ} : Nontrivial (Space d.succ) where +instance instNontrivial {d : ℕ} [NeZero d] : Nontrivial (Space d) where exists_pair_ne := by obtain k := Classical.choice Space.instNonempty - obtain ⟨v1, hv⟩ := exists_ne (0 : EuclideanSpace ℝ (Fin d.succ)) + obtain ⟨v1, hv⟩ := exists_ne (0 : EuclideanSpace ℝ (Fin d)) use k, v1 +ᵥ k - simpa only [ne_eq, eq_vadd_iff_vsub_eq, vsub_self] using hv.symm + simpa [ne_eq, eq_vadd_iff_vsub_eq, vsub_self] using hv.symm /-! diff --git a/Physlib/SpaceAndTime/Space/Integrals/Basic.lean b/Physlib/SpaceAndTime/Space/Integrals/Basic.lean index 16ce76e9f..d84a36e95 100644 --- a/Physlib/SpaceAndTime/Space/Integrals/Basic.lean +++ b/Physlib/SpaceAndTime/Space/Integrals/Basic.lean @@ -21,10 +21,10 @@ We focus here on the volume measure, which is the usual measure on `Space d`, i. - `volume_eq_addHaar` : The volume measure on `Space d` is the same as the Haar measure associated with the basis of `Space d`. -- `integral_volume_eq_spherical` : The integral of a function over `Space d.succ` with +- `integral_volume_eq_spherical` : The integral of a function over `Space d` with respect to the volume measure can be expressed as an integral over the unit sphere and the positive reals. -- `lintegral_volume_eq_spherical` : The lower Lebesgue integral of a function over `Space d.succ` +- `lintegral_volume_eq_spherical` : The lower Lebesgue integral of a function over `Space d` with respect to the volume measure can be expressed as a lower Lebesgue integral over the unit sphere and the positive reals. @@ -45,40 +45,6 @@ open InnerProductSpace MeasureTheory lemma volume_eq_addHaar {d} : (volume (α := Space d)) = Space.basis.toBasis.addHaar := by exact (OrthonormalBasis.addHaar_eq_volume _).symm -lemma volume_closedBall_ne_zero {d : ℕ} (x : Space d.succ) {r : ℝ} (hr : 0 < r) : - volume (Metric.closedBall x r) ≠ 0 := by - obtain ⟨k,hk⟩ := Nat.even_or_odd' d.succ - rcases hk with hk | hk - · rw [InnerProductSpace.volume_closedBall_of_dim_even (k := k)] - simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq, mul_eq_zero, Nat.add_eq_zero_iff, - one_ne_zero, and_false, not_false_eq_true, pow_eq_zero_iff, ENNReal.ofReal_eq_zero, not_or, - not_le] - apply And.intro - · simp_all - · positivity - · simpa using hk - · rw [InnerProductSpace.volume_closedBall_of_dim_odd (k := k)] - simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq, mul_eq_zero, Nat.add_eq_zero_iff, - one_ne_zero, and_false, not_false_eq_true, pow_eq_zero_iff, ENNReal.ofReal_eq_zero, not_or, - not_le] - apply And.intro - · simp_all - · positivity - · simpa using hk - -lemma volume_closedBall_ne_top {d : ℕ} (x : Space d.succ) (r : ℝ) : - volume (Metric.closedBall x r) ≠ ⊤ := by - obtain ⟨k,hk⟩ := Nat.even_or_odd' d.succ - rcases hk with hk | hk - · rw [InnerProductSpace.volume_closedBall_of_dim_even (by simpa using hk)] - simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq] - apply not_eq_of_beq_eq_false - rfl - · rw [InnerProductSpace.volume_closedBall_of_dim_odd (by simpa using hk)] - simp only [Nat.succ_eq_add_one, finrank_eq_dim, ne_eq] - apply not_eq_of_beq_eq_false - rfl - @[simp] lemma volume_metricBall_three : volume (Metric.ball (0 : Space 3) 1) = ENNReal.ofReal (4 / 3 * Real.pi) := by @@ -128,24 +94,23 @@ lemma integral_one_dim_eq_integral_real {f : Space 1 → ℝ} : -/ -lemma integral_volume_eq_spherical (d : ℕ) (f : Space d.succ → F) +lemma integral_volume_eq_spherical (d : ℕ) [NeZero d] (f : Space d → F) [NormedAddCommGroup F] [NormedSpace ℝ F] : - ∫ x, f x ∂volume = ∫ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d.succ).toSphere.prod - (Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by + ∫ x, f x ∂volume = ∫ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d).toSphere.prod + (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := by rw [← MeasureTheory.MeasurePreserving.integral_comp (f := homeomorphUnitSphereProd _) (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd - (volume (α := Space d.succ))) - (Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d.succ)))] - simp only [Nat.succ_eq_add_one, homeomorphUnitSphereProd_apply_snd_coe, - homeomorphUnitSphereProd_apply_fst_coe] - let f' : (x : (Space d.succ)) → F := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x) + (volume (α := Space d))) + (Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d)))] + simp only [homeomorphUnitSphereProd_apply_snd_coe, homeomorphUnitSphereProd_apply_fst_coe] + let f' : (x : (Space d)) → F := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x) conv_rhs => enter [2, x] change f' x.1 rw [MeasureTheory.integral_subtype_comap (by simp), ← setIntegral_univ] simp [f'] refine integral_congr_ae ?_ - have h1 : ∀ᵐ x ∂(volume (α := Space d.succ)), x ≠ 0 := by + have h1 : ∀ᵐ x ∂(volume (α := Space d)), x ≠ 0 := by exact Measure.ae_ne volume 0 filter_upwards [Measure.ae_ne volume 0] with x hx congr @@ -156,14 +121,14 @@ lemma integral_volume_eq_spherical (d : ℕ) (f : Space d.succ → F) simp lemma integrable_spherical_of_integrable {d : ℕ} {F : Type*} - [NormedAddCommGroup F] [NormedSpace ℝ F] {f : Space d.succ → F} + [NormedAddCommGroup F] [NormedSpace ℝ F] {f : Space d → F} (hf : Integrable f volume) : Integrable - (fun x : ↑(Metric.sphere (0 : Space d.succ) 1) × Set.Ioi (0 : ℝ) => + (fun x : ↑(Metric.sphere (0 : Space d) 1) × Set.Ioi (0 : ℝ) => f (x.2.1 • x.1.1)) - (volume (α := Space d.succ).toSphere.prod - (Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by - let s : Set (Space d.succ) := {0}ᶜ + (volume (α := Space d).toSphere.prod + (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := by + let s : Set (Space d) := {0}ᶜ have h1 : Integrable (fun x : s => f x.1) (.comap (Subtype.val (p := fun x => x ∈ s)) volume) := by change Integrable (f ∘ Subtype.val) @@ -172,26 +137,26 @@ lemma integrable_spherical_of_integrable {d : ℕ} {F : Type*} · exact hf.integrableOn · simp [s] have he := MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd - (volume (α := Space d.succ)) + (volume (α := Space d)) have hcomp : Integrable - ((fun x : s => f x.1) ∘ (homeomorphUnitSphereProd (Space d.succ)).symm) - (volume (α := Space d.succ).toSphere.prod - (Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by + ((fun x : s => f x.1) ∘ (homeomorphUnitSphereProd (Space d)).symm) + (volume (α := Space d).toSphere.prod + (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := by rw [← he.integrable_comp_emb] · convert h1 - simp only [Nat.succ_eq_add_one, Function.comp_apply, Homeomorph.symm_apply_apply] - · exact Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d.succ)) + simp only [Function.comp_apply, Homeomorph.symm_apply_apply] + · exact Homeomorph.measurableEmbedding (homeomorphUnitSphereProd (Space d)) convert hcomp using 1 -lemma integral_volume_eq_spherical_iterated {d : ℕ} {F : Type*} - [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Space d.succ → F) +lemma integral_volume_eq_spherical_iterated {d : ℕ} [NeZero d] {F : Type*} + [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Space d → F) (hf : Integrable f volume) : - ∫ x : Space d.succ, f x = - ∫ n : ↑(Metric.sphere (0 : Space d.succ) 1), + ∫ x : Space d, f x = + ∫ n : ↑(Metric.sphere (0 : Space d) 1), ∫ r : Set.Ioi (0 : ℝ), f (r.1 • n.1) - ∂(Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1)) - ∂(volume (α := Space d.succ).toSphere) := by + ∂(Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1)) + ∂(volume (α := Space d).toSphere) := by rw [integral_volume_eq_spherical] rw [MeasureTheory.integral_prod] exact integrable_spherical_of_integrable hf @@ -226,14 +191,14 @@ instance : SFinite (@Measure.comap ↑(Set.Ioi 0) ℝ Subtype.instMeasurableSpac apply MeasurableEmbedding.subtype_coe simp -lemma integral_volume_eq_spherical_integral {d : ℕ} {F : Type*} - [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Space d.succ → F) +lemma integral_volume_eq_spherical_integral {d : ℕ} [NeZero d] {F : Type*} + [NormedAddCommGroup F] [NormedSpace ℝ F] (f : Space d → F) (hf : Integrable f volume) : - ∫ x : Space d.succ, f x = - ∫ n : ↑(Metric.sphere (0 : Space d.succ) 1), - ∫ r : Set.Ioi (0 : ℝ), (r.1 ^ d) • f (r.1 • n.1) + ∫ x : Space d, f x = + ∫ n : ↑(Metric.sphere (0 : Space d) 1), + ∫ r : Set.Ioi (0 : ℝ), (r.1 ^ (d - 1)) • f (r.1 • n.1) ∂(.comap Subtype.val volume) - ∂(volume (α := Space d.succ).toSphere) := by + ∂(volume (α := Space d).toSphere) := by rw [integral_volume_eq_spherical_iterated f hf] congr funext n @@ -242,7 +207,7 @@ lemma integral_volume_eq_spherical_integral {d : ℕ} {F : Type*} congr funext r have hr : 0 ≤ (r : ℝ) := le_of_lt r.2 - rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hr d)] + rw [NNReal.smul_def, Real.coe_toNNReal _ (pow_nonneg hr (d - 1))] /-! @@ -250,18 +215,18 @@ lemma integral_volume_eq_spherical_integral {d : ℕ} {F : Type*} -/ -lemma lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) : - ∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d.succ).toSphere.prod - (Measure.volumeIoiPow (Module.finrank ℝ (Space d.succ) - 1))) := by +lemma lintegral_volume_eq_spherical (d : ℕ) [NeZero d] + (f : Space d → ENNReal) (hf : Measurable f) : + ∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) ∂(volume (α := Space d).toSphere.prod + (Measure.volumeIoiPow (Module.finrank ℝ (Space d) - 1))) := by have h0 := MeasureTheory.MeasurePreserving.lintegral_comp (f := fun x => f (x.2.1 • x.1.1)) (g := homeomorphUnitSphereProd _) (MeasureTheory.Measure.measurePreserving_homeomorphUnitSphereProd - (volume (α := Space d.succ))) + (volume (α := Space d))) (by fun_prop) rw [← h0] - simp only [Nat.succ_eq_add_one, homeomorphUnitSphereProd_apply_snd_coe, - homeomorphUnitSphereProd_apply_fst_coe] - let f' : (x : (Space d.succ)) → ENNReal := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x) + simp only [homeomorphUnitSphereProd_apply_snd_coe, homeomorphUnitSphereProd_apply_fst_coe] + let f' : (x : (Space d)) → ENNReal := fun x => f (‖↑x‖ • ‖↑x‖⁻¹ • ↑x) conv_rhs => enter [2, x] change f' x.1 @@ -276,17 +241,17 @@ lemma lintegral_volume_eq_spherical (d : ℕ) (f : Space d.succ → ENNReal) (hf field_simp rw [one_smul] -lemma lintegral_volume_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal) (hf : Measurable f) : - ∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) * .ofReal (x.2.1 ^ d) - ∂(volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0)) := by +lemma lintegral_volume_eq_spherical_mul (d : ℕ) [NeZero d] + (f : Space d → ENNReal) (hf : Measurable f) : + ∫⁻ x, f x ∂volume = ∫⁻ x, f (x.2.1 • x.1.1) * .ofReal (x.2.1 ^ (d - 1)) + ∂(volume (α := Space d).toSphere.prod (Measure.volumeIoiPow 0)) := by rw [lintegral_volume_eq_spherical, Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right, MeasureTheory.lintegral_withDensity_eq_lintegral_mul, Measure.volumeIoiPow, MeasureTheory.prod_withDensity_right, MeasureTheory.lintegral_withDensity_eq_lintegral_mul] · refine lintegral_congr_ae ?_ - simp only [Nat.succ_eq_add_one, finrank_eq_dim, add_tsub_cancel_right, pow_zero, - ENNReal.ofReal_one] + simp only [finrank_eq_dim, pow_zero, ENNReal.ofReal_one] filter_upwards with x simp only [Pi.mul_apply, one_mul] ring diff --git a/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean b/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean index 0a058c613..2a3c13198 100644 --- a/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean +++ b/Physlib/SpaceAndTime/Space/Integrals/NormPow.lean @@ -68,32 +68,32 @@ lemma radial_jacobian_zpow_mul_self rw [zpow_natCast] private lemma radial_jacobian_zpow - {d p : ℕ} {q : ℤ} (hp_int : (p : ℤ) = q + (d.succ : ℤ)) + {d p : ℕ} [NeZero d] {q : ℤ} (hp_int : (p : ℤ) = q + (d : ℤ)) (hp_pos : 0 < p) {r : ℝ} (hr : 0 < r) : - r ^ d * r ^ q = r ^ (p - 1) := by + r ^ (d - 1) * r ^ q = r ^ (p - 1) := by have hz : r ≠ 0 := ne_of_gt hr calc - r ^ d * r ^ q - = r ^ ((d : ℤ) + q) := by - rw [← zpow_natCast r d, ← zpow_add₀ hz (d : ℤ) q] + r ^ (d - 1) * r ^ q + = r ^ ((d - 1 : ℤ) + q) := by + rw [← Nat.cast_pred (Nat.pos_of_neZero d), ← zpow_natCast, ← zpow_add₀ hz] _ = r ^ ((p - 1 : ℕ) : ℤ) := by congr 1; omega _ = r ^ (p - 1) := by rw [zpow_natCast] lemma radial_norm_power_spherical_integral_eq_space_integral - {d p : ℕ} {q : ℤ} (hp_int : (p : ℤ) = q + (d.succ : ℤ)) - (hp_pos : 0 < p) (η : 𝓢(Space d.succ, ℝ)) : - ∫ x : Space d.succ, η x * ‖x‖ ^ q = - ∫ (n : ↑(Metric.sphere (0 : Space d.succ) 1)), + {d p : ℕ} [NeZero d] {q : ℤ} (hp_int : (p : ℤ) = q + (d : ℤ)) + (hp_pos : 0 < p) (η : 𝓢(Space d, ℝ)) : + ∫ x : Space d, η x * ‖x‖ ^ q = + ∫ (n : ↑(Metric.sphere (0 : Space d) 1)), ∫ (r : Set.Ioi (0 : ℝ)), r.1 ^ (p - 1) * η (r.1 • n.1) ∂(.comap Subtype.val volume) - ∂(volume (α := Space d.succ).toSphere) := by - have hf : Integrable (fun x : Space d.succ => η x * ‖x‖ ^ q) volume := + ∂(volume (α := Space d).toSphere) := by + have hf : Integrable (fun x : Space d => η x * ‖x‖ ^ q) volume := IsDistBounded.integrable_space_mul (IsDistBounded.pow q (by omega)) η rw [integral_volume_eq_spherical_integral - (d := d) (fun x : Space d.succ => η x * ‖x‖ ^ q) hf] + (d := d) (fun x : Space d => η x * ‖x‖ ^ q) hf] congr funext n congr @@ -105,9 +105,8 @@ lemma radial_norm_power_spherical_integral_eq_space_integral ring /-- The function `x ↦ ‖x‖ᵖ` is integrable on `{x : Space d | 0 ≤ ‖x‖ < b}` iff `0 < d + p`. -/ -lemma integrableOn_norm_rpow_ball_iff {d : ℕ} (hd : 0 < d) {b : ℝ} (hb : 0 < b) (p : ℝ) : +lemma integrableOn_norm_rpow_ball_iff {d : ℕ} [NeZero d] {b : ℝ} (hb : 0 < b) (p : ℝ) : IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) (Metric.ball 0 b) ↔ 0 < d + p := by - have : Nontrivial (Space d) := (Nat.succ_pred_eq_of_pos hd) ▸ Space.instNontrivialSucc let f : Space d → ENNReal := (Metric.ball 0 b).indicator (fun x ↦ ‖‖x‖ ^ p‖ₑ) let g : ℝ → ℝ := (Set.Ioo 0 b).indicator (fun r ↦ r ^ p) have hfg : f =ᵐ[volume] fun x ↦ ‖g ‖x‖‖ₑ := by @@ -127,14 +126,14 @@ lemma integrableOn_norm_rpow_ball_iff {d : ℕ} (hd : 0 < d) {b : ℝ} (hb : 0 < · have hInter : Set.Ioo 0 b ∩ Set.Ioi 0 = Set.Ioo 0 b := by ext; grind simp_rw [integrable_fun_norm_addHaar, g, Space.finrank_eq_dim, npow_indicator_rpow_eq (Set.left_notMem_Ioo), - _root_.MeasureTheory.integrableOn_indicator_iff measurableSet_Ioo, hInter, Nat.cast_pred hd] + _root_.MeasureTheory.integrableOn_indicator_iff measurableSet_Ioo, hInter, + Nat.cast_pred (Nat.pos_of_neZero d)] rw [intervalIntegral.integrableOn_Ioo_rpow_iff hb, neg_lt_iff_pos_add'] ring_nf /-- The function `x ↦ ‖x‖ᵖ` is integrable on `{x : Space d | 0 < a ≤ ‖x‖}` iff `d + p < 0`. -/ -lemma integrableOn_norm_rpow_ball_compl_iff {d : ℕ} (hd : 0 < d) {a : ℝ} (ha : 0 < a) (p : ℝ) : +lemma integrableOn_norm_rpow_ball_compl_iff {d : ℕ} [NeZero d] {a : ℝ} (ha : 0 < a) (p : ℝ) : IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) (Metric.ball 0 a)ᶜ ↔ d + p < 0 := by - have : Nontrivial (Space d) := (Nat.succ_pred_eq_of_pos hd) ▸ Space.instNontrivialSucc let f : Space d → ENNReal := (Metric.ball 0 a)ᶜ.indicator (fun x ↦ ‖‖x‖ ^ p‖ₑ) let g : ℝ → ℝ := (Set.Ici a).indicator (fun r ↦ r ^ p) have hfg : f = fun x ↦ ‖g ‖x‖‖ₑ := by ext x; by_cases ‖x‖ ∈ Set.Ici a <;> simp_all [f, g] @@ -148,7 +147,8 @@ lemma integrableOn_norm_rpow_ball_compl_iff {d : ℕ} (hd : 0 < d) {a : ℝ} (ha · have hInter : Set.Ici a ∩ Set.Ioi 0 = Set.Ici a := by ext; grind simp_rw [integrable_fun_norm_addHaar, g, Space.finrank_eq_dim, npow_indicator_rpow_eq (Set.notMem_Ici.mpr ha), - _root_.MeasureTheory.integrableOn_indicator_iff measurableSet_Ici, hInter, Nat.cast_pred hd] + _root_.MeasureTheory.integrableOn_indicator_iff measurableSet_Ici, hInter, + Nat.cast_pred (Nat.pos_of_neZero d)] rw [integrableOn_Ici_iff_integrableOn_Ioi, integrableOn_Ioi_rpow_iff ha, lt_neg_iff_add_neg] ring_nf @@ -175,14 +175,14 @@ lemma integrableOn_norm_rpow_shell {d : ℕ} {a : ℝ} (ha : 0 < a) (b p : ℝ) /-- The function `x ↦ ‖x‖ᵖ` is integrable on a bounded neighborhood of the origin iff `0 < d + p`. -/ -lemma integrableOn_norm_rpow_iff_of_isBounded_nhds {d : ℕ} (hd : 0 < d) {s : Set (Space d)} +lemma integrableOn_norm_rpow_iff_of_isBounded_nhds {d : ℕ} [NeZero d] {s : Set (Space d)} (hs : Bornology.IsBounded s) (hs' : s ∈ nhds 0) (p : ℝ) : IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) s ↔ 0 < d + p := by obtain ⟨a, ha, ha'⟩ := Metric.eventually_nhds_iff_ball.mp hs' obtain ⟨b, hb, hb'⟩ := Bornology.IsBounded.subset_ball_lt hs 0 0 constructor <;> intro h - · exact (integrableOn_norm_rpow_ball_iff hd ha p).mp (IntegrableOn.mono_set h ha') - · exact IntegrableOn.mono_set ((integrableOn_norm_rpow_ball_iff hd hb p).mpr h) hb' + · exact (integrableOn_norm_rpow_ball_iff ha p).mp (IntegrableOn.mono_set h ha') + · exact IntegrableOn.mono_set ((integrableOn_norm_rpow_ball_iff hb p).mpr h) hb' /-- The function `x ↦ ‖x‖ᵖ` is integrable on a bounded subset with the origin in its exterior. -/ lemma integrableOn_norm_rpow_of_isBounded_compl_nhds {d : ℕ} {s : Set (Space d)} @@ -195,10 +195,10 @@ lemma integrableOn_norm_rpow_of_isBounded_compl_nhds {d : ℕ} {s : Set (Space d /-- The function `x ↦ ‖x‖ᵖ` is integrable on a subset with the origin in its exterior provided the decay at infinity is fast enough. -/ -lemma integrableOn_norm_rpow_of_compl_nhds {d : ℕ} (hd : 0 < d) {s : Set (Space d)} +lemma integrableOn_norm_rpow_of_compl_nhds {d : ℕ} [NeZero d] {s : Set (Space d)} (hs : sᶜ ∈ nhds 0) {p : ℝ} (h : d + p < 0) : IntegrableOn (fun x : Space d ↦ ‖x‖ ^ p) s := by obtain ⟨a, ha, ha'⟩ := Metric.eventually_nhds_iff_ball.mp hs have hs' : s ⊆ (Metric.ball 0 a)ᶜ := Set.subset_compl_comm.mp ha' - exact IntegrableOn.mono_set ((integrableOn_norm_rpow_ball_compl_iff hd ha p).mpr h) hs' + exact IntegrableOn.mono_set ((integrableOn_norm_rpow_ball_compl_iff ha p).mpr h) hs' end Space diff --git a/Physlib/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean b/Physlib/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean index 68d416cb2..dd20c2caa 100644 --- a/Physlib/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean +++ b/Physlib/SpaceAndTime/Space/Integrals/RadialAngularMeasure.lean @@ -111,18 +111,18 @@ lemma lintegral_radialMeasure {d : ℕ} (f : Space d → ENNReal) (hf : Measurab · fun_prop · fun_prop -lemma lintegral_radialMeasure_eq_spherical_mul (d : ℕ) (f : Space d.succ → ENNReal) - (hf : Measurable f) : +lemma lintegral_radialMeasure_eq_spherical_mul (d : ℕ) [NeZero d] + (f : Space d → ENNReal) (hf : Measurable f) : ∫⁻ x, f x ∂radialAngularMeasure = ∫⁻ x, f (x.2.1 • x.1.1) - ∂(volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0)) := by + ∂(volume (α := Space d).toSphere.prod (Measure.volumeIoiPow 0)) := by rw [lintegral_radialMeasure, lintegral_volume_eq_spherical_mul] apply lintegral_congr_ae filter_upwards with x have hx := x.2.2 - simp [Nat.succ_eq_add_one, -Subtype.coe_prop] at hx + simp [-Subtype.coe_prop] at hx simp [norm_smul] rw [abs_of_nonneg (le_of_lt x.2.2)] - trans ENNReal.ofReal (↑x.2 ^ d * (x.2.1 ^ d)⁻¹) * f (x.2.1 • ↑x.1.1) + trans ENNReal.ofReal (↑x.2 ^ (d - 1) * (x.2.1 ^ (d - 1))⁻¹) * f (x.2.1 • ↑x.1.1) · rw [ENNReal.ofReal_mul] ring have h2 := x.2.2 @@ -131,7 +131,7 @@ lemma lintegral_radialMeasure_eq_spherical_mul (d : ℕ) (f : Space d.succ → E trans ENNReal.ofReal 1 * f (x.2.1 • ↑x.1.1) · congr field_simp - simp only [ENNReal.ofReal_one, Nat.succ_eq_add_one, one_mul] + simp only [ENNReal.ofReal_one, one_mul] fun_prop fun_prop @@ -195,10 +195,10 @@ lemma integrable_radialAngularMeasure_iff {d : ℕ} {f : Space d → F} : rw [Real.toNNReal_of_nonneg (by positivity), NNReal.smul_def, coe_mk] omit [NormedSpace ℝ F] in -lemma integrable_radialAngularMeasure_of_spherical {d : ℕ} (f : Space d.succ → F) +lemma integrable_radialAngularMeasure_of_spherical {d : ℕ} [NeZero d] (f : Space d → F) (hae : StronglyMeasurable f) (hf : Integrable (fun x => f (x.2.1 • x.1.1)) - (volume (α := Space d.succ).toSphere.prod (Measure.volumeIoiPow 0))) : + (volume (α := Space d).toSphere.prod (Measure.volumeIoiPow 0))) : Integrable f radialAngularMeasure := by refine ⟨StronglyMeasurable.aestronglyMeasurable hae, ?_⟩ rw [hasFiniteIntegral_iff_norm, lintegral_radialMeasure_eq_spherical_mul _ _ diff --git a/Physlib/SpaceAndTime/Space/IsDistBounded.lean b/Physlib/SpaceAndTime/Space/IsDistBounded.lean index 947ec5ae6..82ede10e5 100644 --- a/Physlib/SpaceAndTime/Space/IsDistBounded.lean +++ b/Physlib/SpaceAndTime/Space/IsDistBounded.lean @@ -83,7 +83,7 @@ open MeasureTheory -/ -/-- The boundedness condition on a function ` EuclideanSpace ℝ (Fin dm1.succ) → F` +/-- The boundedness condition on a function `Space d → F` for it to form a distribution. -/ @[fun_prop] def IsDistBounded {d : ℕ} (f : Space d → F) : Prop := @@ -911,10 +911,9 @@ lemma pow_shift {d : ℕ} (n : ℤ) rfl @[fun_prop] -lemma inv_shift {d : ℕ} - (g : Space d.succ.succ) : - IsDistBounded (d := d.succ.succ) (fun x => ‖x - g‖⁻¹) := by - convert IsDistBounded.pow_shift (d := d.succ.succ) (-1) g (by simp) using 1 +lemma inv_shift {d : ℕ} (g : Space d) (hd : 2 ≤ d := by omega) : + IsDistBounded (d := d) (fun x => ‖x - g‖⁻¹) := by + convert IsDistBounded.pow_shift (d := d) (-1) g (by omega) using 1 ext1 x simp @[fun_prop] @@ -970,9 +969,9 @@ lemma norm_add {d : ℕ} (g : Space d) : simp @[fun_prop] -lemma inv {n : ℕ} : - IsDistBounded (d := n.succ.succ) (fun x => ‖x‖⁻¹) := by - convert IsDistBounded.pow (d := n.succ.succ) (-1) (by simp) using 1 +lemma inv {d : ℕ} (hd: 2 ≤ d := by omega): + IsDistBounded (d := d) (fun x => ‖x‖⁻¹) := by + convert IsDistBounded.pow (d := d) (-1) (by omega) using 1 ext1 x simp @@ -983,14 +982,14 @@ lemma norm {d : ℕ} : IsDistBounded (d := d) (fun x => ‖x‖) := by simp @[fun_prop] -lemma log_norm {d : ℕ} : - IsDistBounded (d := d.succ.succ) (fun x => Real.log ‖x‖) := by +lemma log_norm {d : ℕ} (hd : 2 ≤ d := by omega) : + IsDistBounded (d := d) (fun x => Real.log ‖x‖) := by apply IsDistBounded.mono (f := fun x => ‖x‖⁻¹ + ‖x‖) · fun_prop · apply AEMeasurable.aestronglyMeasurable fun_prop · intro x - simp only [Nat.succ_eq_add_one, Real.norm_eq_abs] + simp only [Real.norm_eq_abs] conv_rhs => rw [abs_of_nonneg (by positivity)] have h1 := Real.neg_inv_le_log (x := ‖x‖) (by positivity) have h2 := Real.log_le_rpow_div (x := ‖x‖) (by positivity) (ε := 1) (by positivity) @@ -1285,14 +1284,13 @@ lemma isDistBounded_mul_inner_of_smul_norm {d : ℕ} {f : Space d → ℝ} convert hf.isDistBounded_smul_inner_of_smul_norm hae y using 2 @[fun_prop] -lemma mul_inner_pow_neg_two {d : ℕ} - (y : Space d.succ.succ) : +lemma mul_inner_pow_neg_two {d : ℕ} (y : Space d) (hd : 2 ≤ d := by omega) : IsDistBounded (fun x => ⟪y, x⟫_ℝ * ‖x‖ ^ (- 2 : ℤ)) := by apply IsDistBounded.mono (f := fun x => (‖y‖ * ‖x‖) * ‖x‖ ^ (- 2 : ℤ)) · simp [mul_assoc] apply IsDistBounded.const_mul_fun apply IsDistBounded.congr (f := fun x => ‖x‖ ^ (- 1 : ℤ)) - · apply IsDistBounded.pow (d := d.succ.succ) (-1) (by simp) + · apply IsDistBounded.pow (d := d) (-1) (by omega) · apply AEMeasurable.aestronglyMeasurable fun_prop · intro x diff --git a/Physlib/SpaceAndTime/Space/Module.lean b/Physlib/SpaceAndTime/Space/Module.lean index 7e1856539..f86704220 100644 --- a/Physlib/SpaceAndTime/Space/Module.lean +++ b/Physlib/SpaceAndTime/Space/Module.lean @@ -279,9 +279,9 @@ instance {d} : InnerProductSpace ℝ (Space d) where simp only [smul_vadd_zero, inner_vadd_zero, conj_trivial] exact InnerProductSpace.smul_left v1 v2 a -lemma norm_smul_sphere {d : ℕ} (n : ↑(Metric.sphere (0 : Space d.succ) 1)) +lemma norm_smul_sphere {d : ℕ} (n : ↑(Metric.sphere (0 : Space d) 1)) {r : ℝ} (hr : 0 ≤ r) : - ‖(r • (n : Space d.succ))‖ = r := by + ‖(r • (n : Space d))‖ = r := by simp [norm_smul, mem_sphere_zero_iff_norm.mp n.2, abs_of_nonneg hr] /-!