I would like to prove this in real analysis, but I’m finding it difficult to do it in Coq. Can someone help me, please.

If $f(x_j)$ is non-linear

$x_j \geq 0$, and

$f(x_j) \geq 0$, and

$f(0) = 0$, and

$f'(x_j)<0$ (negative derivative) and

$f'(x_j) = f'(x_i)$, such that $j$ and $i$ are different, and

$f'(x_1)+f'(x_2)+\dots+f'(x_J) = G(x_1+x_2+\dots+x_J) = G(X)$

Than $f(x_j)$ should be some thing like tins:

$f(x_j) = -ax_j^2 + bx_j$ such that $a$ and $b$ are positive constants and $x_j ≤ b/a$.

This is what I have so far.

Require Import Reals.
Open Scope R_scope.

(*f(xj) is non-linear*)
(*/\ represent 'and'*)
Definition additive (f : R -> R) := forall x y : R, f (x + y) = f x + f y.
Definition homogeneous_deg_one (f : R -> R) := forall x a : R, f (a * x) = a * f x.
Definition linear (f : R -> R) := additive f /\ homogeneous_deg_one f.
Definition non_linear (f : R -> R) := ~ linear f.
Definition positive_for_all (f : R -> R) := forall xj : R, f xj > 0.

Definition derivative (f : R -> R) (x : R) := (f (x + 1/1000) - f x) / 1/1000.                              
Definition decreasing_at (f f' : R -> R) (xj : R) := f' xj < 0.
(*f′(xj)=f′(xi), such that j and i are different*) 
Definition equal_derivatives_at_different_points (f : R -> R) (xi xj : R) := xi <> xj         /\ derivative f xi = derivative f xj.
(*exist G(X)=f′(x1)+f′(x2)+⋯+f′(xJ) and X=x1+x2+⋯+xJ *)
Require Import List.
Import ListNotations.
Fixpoint sum_list (l : list R) : R :=
  match l with
  | [] => 0
  | x :: xs => x + sum_list xs
Definition sum_derivatives (f' : R -> R) (l : list R) := sum_list (map f' l).
Definition exists_G (f' : R -> R) :=
  exists G : R -> R, forall l : list R, G (sum_list l) = sum_derivatives f' l.                                      

Parameter my_f : R -> R.
Lemma my_function_is_0 : non_linear my_f.
Lemma my_function_is_1 : positive_for_all my_f.
Lemma my_function_is_2 : decreasing_at my_f.
Lemma my_function_is_3 : equal_derivatives_at_different_points my_f. 
Parameter a : R.
Parameter L : R -> R.
(*Hypothesis L_is_linear : exists m b : R, forall x : R, L x = m * x + b.*)
Lemma L_function_is_linear : linear L.
Definition ff (x : R) := a * x^2 + L x.

Hypothesis my_f_equals_f : forall x : R, my_f x = f x.
  • $\begingroup$ It is dificult to answer the question because we do not know what your level of experience with Coq is. If you are a complete beginner, you might want to try some simpler exercises before you dive into real analysis. Also, you should explain a bit more about what you have tried or where specifically you get stuck. Just saying "it is difficult, please help me" does not give us much to go with. $\endgroup$ May 11, 2023 at 20:47
  • $\begingroup$ My function (f) has too many constraints. So I think it must have a specific shape. I'd just like to prove this using coq, but this is the first time I'm using this. I'll try some more. Thanks. $\endgroup$ May 11, 2023 at 22:39
  • $\begingroup$ Do you know how to write the proof in pen and paper? $\endgroup$
    – Trebor
    May 12, 2023 at 3:35
  • $\begingroup$ @FelipeMorelli: If you've never used a proof assistant, it's going to be quite a challenge to prove your theorem in Coq. Good luck! $\endgroup$ May 12, 2023 at 5:49
  • $\begingroup$ Thant guys.I will try some easy proofs an than I come back to try this one. Like Brazilian and Portuguese say: "Don't put the cart in front of the oxen". $\endgroup$ May 14, 2023 at 12:55


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.