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.
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
[Merged by Bors] - feat: a function with vanishing integral against smooth functions supported in U is ae zero in U #8805
Conversation
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.
Looks very good, thanks!
intro g g_smth g_supp | ||
classical | ||
have cpt := g_supp.image continuous_induced_dom | ||
let g' x := if hx : x ∈ U then g ⟨x, hx⟩ else 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.
Could you instead define g'
as Function.extend Subtype.val g 0
, and prove in separate lemmas that the extension of a smooth compactly supported function is smooth and compactly supported?
theorem liftPropAt_iff_comp_subtype_val (hG : LocalInvariantProp G G' P) {U : Opens M} | ||
(f : M → M') (x : U) : | ||
LiftPropAt P f x ↔ LiftPropAt P (f ∘ Subtype.val) x := by | ||
congrm ?_ ∧ ?_ | ||
· simp_rw [continuousWithinAt_univ, U.openEmbedding'.continuousAt_iff] | ||
· apply hG.congr_iff | ||
exact (U.chartAt_subtype_val_symm_eventuallyEq).fun_comp (chartAt H' (f x) ∘ f) | ||
|
||
theorem liftPropAt_iff_comp_inclusion (hG : LocalInvariantProp G G' P) {U V : Opens M} (hUV : U ≤ V) | ||
(f : V → M') (x : U) : | ||
LiftPropAt P f (Set.inclusion hUV x) ↔ LiftPropAt P (f ∘ Set.inclusion hUV : U → M') x := by | ||
congrm ?_ ∧ ?_ | ||
· simp [continuousWithinAt_univ, | ||
· simp_rw [continuousWithinAt_univ, | ||
(TopologicalSpace.Opens.openEmbedding_of_le hUV).continuousAt_iff] | ||
· apply hG.congr_iff | ||
exact (TopologicalSpace.Opens.chartAt_inclusion_symm_eventuallyEq hUV).fun_comp | ||
(chartAt H' (f (Set.inclusion hUV x)) ∘ f) | ||
#align structure_groupoid.local_invariant_prop.lift_prop_at_iff_comp_inclusion StructureGroupoid.LocalInvariantProp.liftPropAt_iff_comp_inclusion | ||
|
||
theorem liftProp_subtype_val {Q : (H → H) → Set H → H → Prop} (hG : LocalInvariantProp G G Q) | ||
(hQ : ∀ y, Q id univ y) (U : Opens M) : | ||
LiftProp Q (Subtype.val : U → M) := by | ||
intro x | ||
show LiftPropAt Q (id ∘ Subtype.val) x | ||
rw [← hG.liftPropAt_iff_comp_subtype_val] | ||
apply hG.liftProp_id hQ |
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.
cc author of #19416 @hrmacbeth in case I'm missing some easy way to deduce smooth_subtype_iff
.
bors r+ |
…ported in U is ae zero in U (#8805) A stronger version of #8800, the differences are: + assume either `IsSigmaCompact U` or `SigmaCompactSpace M`; + only need test functions satisfying `tsupport g ⊆ U` rather than `support g ⊆ U`; + requires `LocallyIntegrableOn` U rather than `LocallyIntegrable` on the whole space. Also fills in some missing APIs around the manifold and measure theory libraries. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
Pull request successfully merged into master. Build succeeded: |
…ported in U is ae zero in U (#8805) A stronger version of #8800, the differences are: + assume either `IsSigmaCompact U` or `SigmaCompactSpace M`; + only need test functions satisfying `tsupport g ⊆ U` rather than `support g ⊆ U`; + requires `LocallyIntegrableOn` U rather than `LocallyIntegrable` on the whole space. Also fills in some missing APIs around the manifold and measure theory libraries. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
A stronger version of #8800, the differences are:
assume either
IsSigmaCompact U
orSigmaCompactSpace M
;only need test functions satisfying
tsupport g ⊆ U
rather thansupport g ⊆ U
;requires
LocallyIntegrableOn
U rather thanLocallyIntegrable
on the whole space.Also fills in some missing APIs around the manifold and measure theory libraries.