filter only goal

Stream: general

[Patrick Massot]

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]

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

[Bryan Gin-ge Chen]

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]

I knew I saw it somewhere!

[Patrick Massot]

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]

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

[Patrick Massot]

And the lemma has half a dozen variations.

[Patrick Massot]

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]

now the naming system isn't scaling

[Mario Carneiro]

This theorem needs a doc comment

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

Oops, that's not this variation.

[Patrick Massot]

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

[Mario Carneiro]

So the point of the theorem is differentiating an integral?

[Patrick Massot]

sure

[Patrick Massot]

hence the has_deriv_at_integral_on

[Mario Carneiro]

I would start with that

[Mario Carneiro]

add qualifiers when it starts to conflict with other theorems

[Sebastien Gouezel]

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]

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.