Much Less than Operator

Stream: maths

[Colin Jones ⚛️]

I was reading some literature in physics that used the much less than operator "<<" in one of the simplifications and was wondering if it was possible to do in Lean. Here's the simplification that the authors did:

$$\begin{equation} a << 1 \land 1 << c \end{equation}$$ $$\begin{equation} V = \frac{ab}{(1 - a)(1 + (c - 1)a)} \implies V = \frac{ab}{1 + ca} \end{equation}$$

I believe that it would be impossible to rationalize the above logic because its a rather subjective simplification (why not take away the a*b for instance?). But, I'm curious to know Zulip's thoughts on this subject.

I've also provided a supplementary Lean 4 code for the operator.

import Mathlib

variable (X Y a b c : ℝ)

def MuchLessThan : Prop := ∃ k : ℝ, 0 < k ∧ X*k = Y

notation " << " => MuchLessThan

example (h : X < Y) : << X Y := by
  dsimp [MuchLessThan]
  use (Y / X)
  sorry
  -- Not true because X = 0

example (h : << a 1) (h1 : V = a*b / ((1 - a)*(1 + (c - 1)*a))) :
  V = a*b / (1 + c*a) := by sorry

[Colin Jones ⚛️]

Please note it's an example definition from what I could find on the internet

[Matt Diamond]

the definition needs a bit of work... by the current definition, any two positive real numbers are each MuchLessThan the other, and the same goes for any two negative real numbers

[Kyle Miller]

Quick thought: I think << makes sense, but with some more sophisticated setup, where it's not a relation between particular variables, but a relation more on filters (docs#Filter). If you're not familiar with filters, this might seem totally out there, but it seems like filters in different forms are key to understanding these sorts of properties that are not literally true, but true in a tendency sense.

The underlying idea here expanded out (which filters should be able to make cleaner) is that you want to translate "for all x such that 1 << x, P x" to "there exists k such that 1 < k and for all x such that k < x, P x". It's a truth about something that eventually is true for all big enough x.

[Kyle Miller]

Of course, that could be recast as "there exists k >= 1 such that for all a >= k, P (a * 1)", to make it look more like this scalar version you have formalized.

[Ira Fesefeldt]

I believe related to filters: I usually associate the 'much less than' operation with asymptotic growth between functions. I don't know enough about physics to know if that's also the understanding here. But if you consider variables a and c as sequence that move away from 1 (in their respective directions), you could maybe make sense of it?

[Eric Wieser]

Yes, I think the answer here is to talk about asymptotics along filters

[Eric Wieser]

I think this is close to the correct statement?

import Mathlib

set_option autoImplicit false
open scoped Asymptotics

def aFilter : Filter ℝ := 𝓝[>] 0 ⊓ .principal (Set.Ioo 0 1)
def cFilter : Filter ℝ := .atTop ⊓ .principal (Set.Ioi 1)

example (b : ℝ) : (fun (a, c) => a*b / ((1 - a)*(1 + (c - 1)*a))) ~[aFilter ×ˢ cFilter] (fun (a, c) => a*b / (1 + c*a)) := by
  sorry

[Eric Wieser]

I made it to here before realizing something was wrong:

example (b : ℝ) : (fun (a, c) => a*b / ((1 - a)*(1 + (c - 1)*a))) ~[aFilter ×ˢ cFilter] (fun (a, c) => a*b / (1 + c*a)) := by
  -- simp [aFilter, cFilter]
  refine .div ?_ ?_
  · rfl
  · ring_nf
    conv_lhs =>
      enter [x]
      rw [sub_add_eq_add_sub, sub_add_eq_add_sub, add_sub_assoc, mul_comm]
    refine .add_isLittleO (.refl) ?_
    rw [@Asymptotics.isLittleO_iff]
    intros r hr
    dsimp [aFilter, cFilter]
    simp_rw [Filter.prod_inf, Filter.inf_prod, Filter.prod_principal_principal, ←inf_assoc, Filter.eventually_inf_principal, Set.mem_prod, Set.mem_Ioi, Set.mem_Iio]
    filter_upwards with ⟨a, c⟩
    rintro ⟨ha : a < 1, hc : 1 < c⟩
    simp
    sorry

[Colin Jones ⚛️]

I'm somewhat familiar with Filters, though not as knowledgeable as I would like. Sorry as well for forgetting to include that all the real numbers in the derivation were positive real numbers (thus a cannot be negative, this is important in the next thing I will say).

Initially, when approaching the "<<" operator I was thinking it could be done with limits (a special kind of filter). For example,

$$\begin{equation} \lim_{a\to0} \lim_{c\to\infty} \frac{ab}{(1 - a)(1 + (c - 1)a)} = \frac{ab}{1 + ca} \end{equation}$$

However, this mathematical statement makes no sense. Again the logic would be flawed as the a*b term would have to go away. And c goes to infinity which is just makes no sense.

Thank you Eric and Ira for sharing your takes on it. I'm not that great of a mathematician (just an undergraduate and an engineering major) so I'm not sure what an asymptotic filter is, but I'll look into it.

Could someone provide an informal proof of the statement with their definition of the "<<" operator? I doubt the original statement is true rigorously but would be happy for someone to prove me wrong.

[Eric Wieser]

I'm not that great of a mathematician (just an undergraduate and an engineering major)

I too am an engineering major, which also means that this is out of my comfort zone. The code I posted above is probably close to the right thing, but almost certainly not it

[Frédéric Dupuis]

I think Eric's formulation is basically right, but aFilter should be 𝓝[>] 0 and cFilter should be atTop.

[Eric Wieser]

My claim is that the changes you're suggesting are part of solving the problem

[Eric Wieser]

That is, you're saying a << 1 is stronger than necessary, and a << 0 is fine? (did you mean 𝓝[<] 0?) hmm, that sounds backwards

[Frédéric Dupuis]

I'm saying "<<1" doesn't actually involve the number 1, it's just a limit towards zero.

[Eric Wieser]

In which case you're also saying that the problem as originally stated is false if a is allowed to be negative?

[Frédéric Dupuis]

Well, as Colin says above a is understood to be nonnegative.

[Eric Wieser]

Thanks, somehow I missed that

[Eric Wieser]

Edited above, I think now my version is accurate (but as you say, the 1 is irrelevant)

[Ira Fesefeldt]

Colin Jones ⚛️ said:

Could someone provide an informal proof of the statement with their definition of the "<<" operator? I doubt the original statement is true rigorously but would be happy for someone to prove me wrong.

I am not too familiar with the formalization of asymptotics and filters in mathlib, so I can not guarantee that my informal proof matches Eric ones. But I believe one idea goes along like this:

We have two functions

$$f(a, b, c) = \frac{ab}{(1-a)(1+(c-1)a)}\qquad g(a, b, c) = \frac{ab}{1+ca}$$

and we want to prove that f and g are asymptotically equal as $a \to 0+$ and $c \to \infty$.
Asymptotically equal means something on the line that there is a positive real number $M$ such that

$$\lim_{a \to 0+} \lim_{c \to \infty} \left|\frac{f}{g}\right| = \dots = 1 = M$$

which is the case.

[Mauricio Collares]

Note that $f \ll g$ in this context is the same as $f = o(g)$ if I understand correctly. Mathlib already has notation for the latter: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Asymptotics/Asymptotics.html#Asymptotics.%C2%ABterm_=o[_]_%C2%BB

[Robert Maxton]

When I see that sort of simplification, I'm usually thinking about first order v.s. higher order terms, where the assumption is that we can detect one order of a small number when added to a 'normal' number, but not two. So the numerator would stay even if it were a^612 b, because it's not being added with (and thus implicitly compared with) anything; whereas the denominator has removed all terms of order a^2, because it starts with 1+ and so there's a reference number to say it's "very small" in comparison to.

[Robert Maxton]

The relevant concept in strict mathematics is usually handled by dual numbers, which already exist in Lean as docs#DualNumber, but that would incorrectly remove e.g. an a^2 in the numerator. So that's not a perfect solution, but it might be a good approximation for a number of use cases.

[Robert Maxton]

In general, I'd probably imagine this best implemented as a tactic that recurses into the expression tree to some specified level, then reduces everything it finds there to the form α ε^n (1 + β ε), where ε is "small" and all other constants are "normal", throwing away higher order terms as needed. Perhaps it could in fact just attempt to factor out as many copies of ε as possible, and then try to series-expand and/or substitute in a dual?

[Wrenna Robson]

Related to this: do we have notation (I assume we do?) for neglibility? https://en.wikipedia.org/wiki/Negligible_function

[Frédéric Dupuis]

I don't think we do. And it would be more than just notation: it's little-o of every inverse polynomial.