## Stream: general

### Topic: filter only goal

#### 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.

#### Patrick Massot (Aug 24 2020 at 19:23):

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

#### 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?

#### Patrick Massot (Aug 24 2020 at 19:28):

I knew I saw it somewhere!

#### 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.

#### 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?

#### Patrick Massot (Aug 24 2020 at 19:52):

And the lemma has half a dozen variations.

#### 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₀


#### Kenny Lau (Aug 24 2020 at 19:57):

now the naming system isn't scaling

#### Mario Carneiro (Aug 24 2020 at 20:17):

This theorem needs a doc comment

#### Mario Carneiro (Aug 24 2020 at 20:17):

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

#### Patrick Massot (Aug 24 2020 at 20:19):

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

#### Patrick Massot (Aug 24 2020 at 20:20):

Oops, that's not this variation.

#### Patrick Massot (Aug 24 2020 at 20:20):

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

#### Mario Carneiro (Aug 24 2020 at 20:21):

So the point of the theorem is differentiating an integral?

sure

#### Patrick Massot (Aug 24 2020 at 20:21):

hence the has_deriv_at_integral_on

#### Mario Carneiro (Aug 24 2020 at 20:22):

add qualifiers when it starts to conflict with other theorems

#### 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?

#### 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