-
Notifications
You must be signed in to change notification settings - Fork 298
feat(analysis/normed_space/box_subadditive): define box_(sub|sup|)additive_on
#4913
Conversation
🎉 Great news! Looks like all the dependencies have been resolved:
💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I have a lot of minor comments (mostly adding more docstrings), but I like it a lot anyway :-)
A function `f : (ι → ℝ) → (ι → ℝ) → M` is called | ||
`box_subadditive_on`/`box_additive_on`/`box_supadditive_on` a set `s` if for any `l u : ι → ℝ`, `l ≤ | ||
u`, `Icc l u ⊆ s` and any hyperplane `x i = c`, `l i ≤ c ≤ u i`, the sum of the values of `f` on the | ||
two subboxes `[l, u] ∩ {x | x i ≤ c}` and `[l, u] ∩ {x | c ≤ x i}` is greater than or | ||
equal/equal/less than or equal to its value on `[l, u]`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This docstring is hard to understand. Do you mean that you think of the value f l u
as the value of the function on the box with lower corner l
and upper corner u
, i.e., the set Icc l u
, that you denote with the usual interval notation [l, u]
?
The main result of this file is theorem `box_subadditive_on.eq_zero_of_forall_is_o_prod`. It says | ||
that `f l u = 0` provided that `f` is `box_subadditive_on` the interval `[l, u]`, `l ≤ u`, and | ||
for any `p ∈ [l, u]` we have `f l' u' = o(volume [l', u'])` as both `l'` tends to `p` along | ||
`[l, p]`, `u'` tends to `p` along `[p, u]`, and the subbox `[l', u']` is homothetic to `[l, u]`. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Could you give a motivation for this statement, and maybe also a sketch of proof?
tendsto_inf.2 ⟨tendsto_right_nhds_fix hf hg I, tendsto_principal.2 $ eventually_of_forall $ | ||
λ n, ⟨(fix_mem_seq hf hg I n).2, seq_right_mono hf hg I (zero_le n)⟩⟩ | ||
|
||
lemma le_mul_of_forall_eventually_le_mul (hle : l ≤ u) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
docstring? (This is really more general than the next one, so it deserves a docstring IMHO)
|
||
open asymptotics function | ||
|
||
lemma eq_zero_of_forall_is_o (hle : l ≤ u) (hf : box_subadditive_on (λ x y, ∥f x y∥) (Icc l u)) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
docstring
(hg : box_supadditive_on (λ x y, ∥g x y∥) (Icc l u)) | ||
(Hc : ∀ (b ∈ Icc l u), is_o (λ p : _ × ℝ, uncurry f p.1) (λ p, uncurry g p.1) | ||
((𝓝[Icc l b] b ×ᶠ 𝓝[Icc b u] b ×ᶠ 𝓝[Ioi 0] 0) ⊓ 𝓟 {p | p.1.2 - p.1.1 = p.2 • (u - l)})) | ||
: f l u = 0 := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
move colon to the previous line
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
norm_cast
lemmas, golf proofs #4911