Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[Merged by Bors] - feat: Real.toNNReal_abs #11606

Closed
wants to merge 2 commits into from
Closed

[Merged by Bors] - feat: Real.toNNReal_abs #11606

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
2830ed2
feat; `Real.toNNReal_abs`
YaelDillies Mar 23, 2024
b01e82f
unused variable
YaelDillies Mar 23, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 0 additions & 4 deletions Mathlib/Analysis/Distribution/SchwartzSpace.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1068,10 +1068,6 @@ def integralCLM : 𝓢(D, V) →L[𝕜] V :=
rcases hμ.exists_integrable with ⟨n, h⟩
let m := (n, 0)
use Finset.Iic m, 2 ^ n * ∫ x : D, (1 + ‖x‖) ^ (- (n : ℝ)) ∂μ
have hpos : 0 ≤ ∫ x : D, (1 + ‖x‖) ^ (- (n : ℝ)) ∂μ := by
apply integral_nonneg
intro
positivity
refine ⟨by positivity, fun f ↦ (norm_integral_le_integral_norm f).trans ?_⟩
have h' : ∀ x, ‖f x‖ ≤ (1 + ‖x‖) ^ (-(n : ℝ)) *
(2 ^ n * ((Finset.Iic m).sup (fun m' => SchwartzMap.seminorm 𝕜 m'.1 m'.2) f)) := by
Expand Down
5 changes: 4 additions & 1 deletion Mathlib/Data/Real/NNReal.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@
import Mathlib.Order.ConditionallyCompleteLattice.Group
import Mathlib.Tactic.GCongr.Core

#align_import data.real.nnreal from "leanprover-community/mathlib"@"de29c328903507bb7aff506af9135f4bdaf1849c"
#align_import data.real.nnreal from "leanprover-community/mathlib"@"b1abe23ae96fef89ad30d9f4362c307f72a55010"

Check notice on line 15 in Mathlib/Data/Real/NNReal.lean

View workflow job for this annotation

GitHub Actions / Add annotations

Synchronization 

See review instructions and diff at
https://leanprover-community.github.io/mathlib-port-status/file/data/real/nnreal?range=de29c328903507bb7aff506af9135f4bdaf1849c..b1abe23ae96fef89ad30d9f4362c307f72a55010

/-!
# Nonnegative real numbers
Expand Down Expand Up @@ -1180,6 +1180,9 @@
max_le (le_abs_self _) (abs_nonneg _)
#align real.coe_to_nnreal_le Real.coe_toNNReal_le

@[simp] lemma toNNReal_abs (x : ℝ) : |x|.toNNReal = nnabs x := NNReal.coe_injective <| by simp
#align real.to_nnreal_abs Real.toNNReal_abs

theorem cast_natAbs_eq_nnabs_cast (n : ℤ) : (n.natAbs : ℝ≥0) = nnabs n := by
ext
rw [NNReal.coe_nat_cast, Int.cast_natAbs, Real.coe_nnabs, Int.cast_abs]
Expand Down
Loading