Zulip Chat Archive

Stream: general

Topic: filter only goal


view this post on Zulip Patrick Massot (Aug 24 2020 at 19:23):

It would be nice to have a tactic state filter displaying only goals. I just ran an apply spawning 8 goals, and I'd like to quickly check whether they all seem provable.

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:23):

Btw, is there any news about the fight to make widget filters persistent?

view this post on Zulip Bryan Gin-ge Chen (Aug 24 2020 at 19:25):

I don't know what the story for the widget tactic state filters is, but if you have the tactic state in text mode, the "goals only" filter should do this, right?

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:28):

I knew I saw it somewhere!

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:28):

But I couldn't find it in the drop-down menu. The issue is it hasn't been ported to the widget view.

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:50):

Can someone remind me how the naming convention works when you have 8 explicit arguments to a lemma?

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:52):

And the lemma has half a dozen variations.

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:54):

Something like:

lemma has_deriv_at_integral_on_of_dominated_loc_of_deriv_le
  {α : Type*} [measurable_space α] {μ : measure α}
  {E : Type*} [normed_group E] [second_countable_topology E] [normed_space  E]
  [complete_space E] [measurable_space E] [borel_space E]
  {F :   α  E} {F' :   α  E} {x₀ : }
  {s : set α} {bound : α  } {ε : }
  (ε_pos : 0 < ε)
  (hF_meas :  x in 𝓝 x₀, measurable (F x))
  (hF_int : integrable_on (F x₀) s μ)
  (hF'_meas :  x  ball x₀ ε, measurable (F' x))
  (h_bound :  a  μ.restrict s,  x  ball x₀ ε, F' x a  bound a)
  (bound_measurable : measurable (bound : α  ))
  (bound_integrable : integrable_on bound s μ)
  (h_diff :  a  (μ.restrict s),  x  ball x₀ ε, has_deriv_at (λ x, F x a) (F' x a) x) :
  has_deriv_at (λn,  a in s, F n a μ) ( a in s, F' x₀ a μ) x₀

view this post on Zulip Kenny Lau (Aug 24 2020 at 19:57):

now the naming system isn't scaling

view this post on Zulip Mario Carneiro (Aug 24 2020 at 20:17):

This theorem needs a doc comment

view this post on Zulip Mario Carneiro (Aug 24 2020 at 20:17):

and the name should be similar words as what you write in the doc comment

view this post on Zulip Patrick Massot (Aug 24 2020 at 20:19):

/-- Differentiation under the integral assuming 8 things, including a local domination and Lipschitz condition-/

view this post on Zulip Patrick Massot (Aug 24 2020 at 20:20):

Oops, that's not this variation.

view this post on Zulip Patrick Massot (Aug 24 2020 at 20:20):

I meant `/-- Differentiation under the integral assuming 8 things, including a local domination and derivative bound. -/

view this post on Zulip Mario Carneiro (Aug 24 2020 at 20:21):

So the point of the theorem is differentiating an integral?

view this post on Zulip Patrick Massot (Aug 24 2020 at 20:21):

sure

view this post on Zulip Patrick Massot (Aug 24 2020 at 20:21):

hence the has_deriv_at_integral_on

view this post on Zulip Mario Carneiro (Aug 24 2020 at 20:22):

I would start with that

view this post on Zulip Mario Carneiro (Aug 24 2020 at 20:22):

add qualifiers when it starts to conflict with other theorems

view this post on Zulip Sebastien Gouezel (Aug 24 2020 at 20:26):

Not sure you need to state it with μ.restrict s: if you have a version without the s (with usual integral for the full measure) and if you apply it to μ.restrict s, doesn't it give exactly the statement you wrote?

view this post on Zulip Patrick Massot (Aug 24 2020 at 20:27):

Yes indeed, the proof is exactly applying the absolute result, but I thought we still wanted the statement. Maybe not actually, but the absolute result is not much easier to name.


Last updated: May 14 2021 at 12:18 UTC