Kakeya problem

Stream: maths

[Kevin Buzzard]

My former PhD student Bodan Arsovski just wandered into the room I'm in; he recently proved a p-adic version of the Kakeya conjecture. I know nothing about this stuff. I attempted to formalise a statement of the usual conjecture (over the reals), which seemed to work OK, but when I tried with the p-adics I ran into problems because the p-adics don't have a canonical measure on them.

import number_theory.padics.hensel
import data.polynomial.degree.lemmas
import measure_theory.measure.hausdorff
import data.real.ereal

open_locale measure_theory

example (n : ℕ) (hn : 0 < n) (p : ℕ) (X : set (fin n → ℝ)) (hX : ∀ v : fin n → ℝ, ∥v∥ = 1 → ∃ b, ∀ m, 0 ≤ m ∧ m ≤ 1 → b + m * v ∈ X) :
  μH[n] X = n :=
begin
  sorry
end

instance (n p : ℕ) [fact (nat.prime p)] : measurable_space (fin n → ℚ_[p]) := sorry

instance (n p : ℕ) [fact (nat.prime p)] : borel_space (fin n → ℚ_[p]) := sorry

example (n : ℕ) (hn : 0 < n) (p : ℕ) [fact (nat.prime p)] (X : set (fin n → ℚ_[p])) (hX : ∀ v : fin n → ℚ_[p],
  ∥v∥ = 1 → ∃ b, ∀ m : ℚ_[p], ∥m∥ ≤ 1 → b + m • v ∈ X) :
  μH[n] X = n :=
begin
  sorry
end

How am I supposed to be filling in those instances? The measure we want is Haar measure. Unrelated question: I was surprised m * v worked for reals but I had to use m • v for the p-adics.

[Johan Commelin]

Can you just assume you have a random measure and then add [haar_measure ℚ_[p]] to make sure it is a well-behaved measure?

[Johan Commelin]

Or maybe [haar_measure (fin n → ℚ_[p])] even.

[Yaël Dillies]

docs#measure_theory.measure.haar_measure (three measure in the name :frowning:) is a specific measure, not a typeclass saying that a measure is the Haar measure.

[Yaël Dillies]

What you want is docs#measure_theory.measure.is_haar_measure.

[Yaël Dillies]

But, given that the type is concrete, we should construct the measure.

[Patrick Massot]

(deleted)

[Yaël Dillies]

To answer your question, Kevin, the sorry should be something like add_haar_measure K where K : set (fin n → ℚ_[p]) is a compact set of nonempty interior.

[Johan Commelin]

But using is_add_haar_measure is more flexible right?

[Yaël Dillies]

Are you ever going to endow the same type with two different Haar measures?

[Yaël Dillies]

It kind of feels like assuming order_bot ℕ because "that's more general".

[Floris van Doorn]

I think you are quite likely to use more than one measure on a type like fin n → ℚ_[p]:
(1) add_haar_measure
(2) docs#measure_theory.measure.pi of add Haar measures

[Yaël Dillies]

Aren't those the same (at least up to scaling)?

[Johan Commelin]

Do you think TC is impressed by that fact?

[Yaël Dillies]

Well, that means we must provide the Haar measure on ℚ_[p], then we'll automatically get the Haar measure on fin n → ℚ_[p].

[Kevin Buzzard]

But it worked for the reals, and Floris' objections apply there too!

[Yaël Dillies]

Like, what's special about this situation?

[Floris van Doorn]

I'm not sure. It might be that choosing a Haar measure on ℚ_[p] and then working with that will be fine. But I wouldn't be surprised that at some point you'd have to change the measure, and have to do a bit of work using the uniqueness of Haar measures to derive what you want for the other measure.
I don't think the story is different for the reals. And a lemma like docs#measure_theory.measure.map_linear_map_add_haar_pi_eq_smul_add_haar shows that sometimes you have to translate from a specific Haar measure to an arbitrary Haar measure. If you only have to do this a handful of times that might be fine though.

[Sebastien Gouezel]

Haar mesure is unique up to scaling, but the scaling is not canonical in a general space. For instance, in a product space, the product measure and the Hausdorff measure may be different.

[Johan Commelin]

Before reviewing @Sebastien Gouezel's work, I had never heard of Besicovitch before. Now I'm looking at https://en.wikipedia.org/wiki/Kakeya_set and :tada: the name pops up again.

[Kevin Buzzard]

Swinnerton-Dyer used to talk fondly about Besicovitch after he'd had a couple of pints of cider.